An Isabelle/HOL Formalization of Narrowing and Multiset Narrowing for E-Unifiability, Reachability and Infeasibility.

Dohan Kim

Browse the full ITP paper archive.