We propose a generalization of Newman’s lemma which gives a criterion of confluence for a wide class of not-necessarily-terminating abstract rewriting systems. We show that ordinary Newman’s lemma for terminating systems can be considered as a corollary of this criterion. We describe a formalization of the proposed generalized Newman’s lemma in Isabelle proof assistant using HOL logic.
@InProceedings{ivanov:LIPIcs.FSCD.2023.9, author = {Ivanov, Ievgen}, title = {{Generalized Newman’s Lemma for Discrete and Continuous Systems}}, booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)}, pages = {9:1--9:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-277-8}, ISSN = {1868-8969}, year = {2023}, volume = {260}, editor = {Gaboardi, Marco and van Raamsdonk, Femke}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.9}, URN = {urn:nbn:de:0030-drops-179936}, doi = {10.4230/LIPIcs.FSCD.2023.9}, annote = {Keywords: abstract rewriting system, confluence, discrete-continuous systems, proof assistant, formal proof} }
Feedback for Dagstuhl Publishing