An Isabelle/HOL Formalization of Narrowing and Multiset Narrowing for E-Unifiability, Reachability and Infeasibility
Dohan Kim15th International Conference on Interactive Theorem Proving (ITP 2024), 2024.
Abstract
We present an Isabelle/HOL formalization of narrowing for E-unifiability, reachability, and infeasibility. Given a semi-complete rewrite system R and two terms s and t, we show a formalized proof that if narrowing terminates, then it provides a decision procedure for R-unifiability for s and t, where R 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.
BibTeX
@inproceedings{DBLP:conf/itp/000124,
author = {Dohan Kim},
editor = {Yves Bertot and
Temur Kutsia and
Michael Norrish},
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, September 9-14, 2024, Tbilisi, Georgia},
series = {LIPIcs},
volume = {309},
pages = {24:1—24:19},
publisher = {Schloss Dagstuhl – Leibniz-Zentrum f{\”{u}}r Informatik},
year = {2024},
url = {https://doi.org/10.4230/LIPIcs.ITP.2024.24},
doi = {10.4230/LIPICS.ITP.2024.24},
timestamp = {Mon, 03 Mar 2025 21:16:06 +0100},
biburl = {https://dblp.org/rec/conf/itp/000124.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}