Abstract: 

Narrowing is a generalization of rewriting, where matching used in rewriting is replaced by unification. In this talk, I will first give an overview of narrowing, E-unifiability, and reachability. Then I will talk about equational narrowing and describe how it is applied to reachability analysis and E-unifiability problems. In particular, I will discuss an Isabelle/HOL formalization of equational narrowing and its applications to reachability analysis and E-unifiability problems.

Next, I will introduce the proposed multiset rewriting and multiset narrowing and describe the difference between (ordinary) narrowing and multiset narrowing.  I will explore how multiset narrowing is applied to multiset reachability analysis, reachability analysis, and E-unifiability problems consisting of multiple goals. Furthermore, I will present an Isabelle/HOL formalization of multiset narrowing and its related results on multiset reachability analysis, reachability analysis, and E-unifiability problems.

Finally, I will conclude the talk by discussing potential future research directions on multiset rewriting and multiset narrowing along with their formalization in Isabelle/HOL.