An Isabelle/HOL Formalization of Semi-Thue and Conditional Semi-Thue Systems
Dohan KimInternational Conference on Interactive Theorem Proving, Leibniz International Proceedings in Informatics 352, pp. 10:1—10:20, 2025.
Abstract
We present a formalized framework for semi-Thue and conditional semi-Thue systems for studying monoids and their word problem using the Isabelle/HOL proof assistant. We provide a formalized decision procedure for the word problem of monoids if they are finitely presented by complete semi-Thue systems. In particular, we present a new formalized method for checking confluence using (conditional) critical pairs for certain conditional semi-Thue systems. We propose and formalize an inference system for generating conditional equational theories and Thue congruences using conditional semi-Thue systems. Then we provide a new formalized decision procedure for the word problem of monoids which have finite complete (reductive) conditional presentations.
BibTeX
@InProceedings{kim:LIPIcs.ITP.2025.10,
author = {Kim, Dohan},
title = {An Isabelle/HOL Formalization of Semi-{T}hue and Conditional Semi-{T}hue Systems},
booktitle = {16th International Conference on Interactive Theorem Proving (ITP 2025)},
pages = {10:1--10:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-396-6},
ISSN = {1868-8969},
year = {2025},
volume = {352},
editor = {Forster, Yannick and Keller, Chantal},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.10},
URN = {urn:nbn:de:0030-drops-246081},
doi = {10.4230/LIPIcs.ITP.2025.10}
}