We present an Isabelle/HOL formalization of narrowing for E-unifiability, reachability, and infeasibility. Given a semi-complete rewrite system ℛ and two terms s and t, we show a formalized proof that if narrowing terminates, then it provides a decision procedure for ℛ-unifiability for s and t, where ℛ is viewed as a set of equations. Furthermore, we present multiset narrowing and its formalization for multiset reachability and reachability analysis, providing decision procedures using certain restricted conditions on multiset reachability and reachability problems. Our multiset narrowing also provides a complete method for E-unifiability problems consisting of multiple goals if E can be represented by a complete rewrite system.
@InProceedings{kim:LIPIcs.ITP.2024.24, author = {Kim, Dohan}, title = {{An Isabelle/HOL Formalization of Narrowing and Multiset Narrowing for E-Unifiability, Reachability and Infeasibility}}, booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)}, pages = {24:1--24:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-337-9}, ISSN = {1868-8969}, year = {2024}, volume = {309}, editor = {Bertot, Yves and Kutsia, Temur and Norrish, Michael}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.24}, URN = {urn:nbn:de:0030-drops-207525}, doi = {10.4230/LIPIcs.ITP.2024.24}, annote = {Keywords: Narrowing, Multiset Narrowing, Unifiability, Reachability} }
Feedback for Dagstuhl Publishing