Formalizing Almost Development Closed Critical Pairs
Christina Kohl and Aart Middeldorp
Proceedings of the 14th International Conference on Interactive Theorem
Proving (ITP 2023), Leibniz International Proceedings in
Informatics 268, pp. 38:1 – 38:8, 2023.
Abstract
We report on the first formalization of the almost-development closedness criterion for confluence of left-linear term rewrite systems and illustrate a problem we encountered while trying to formalize the original paper proof by van Oostrom.BibTeX Entry
@inproceedings{KM-ITP23,
author = "Christina Kohl and Aart Middeldorp",
title = "Formalizing Almost Development Closed Critical Pairs",
booktitle = "Proceedings of the 14th International Conference on
Interactive Theorem Proving",
editor = "Adam Naumowicz and Ren\'e Thiemann",
series = "Leibniz International Proceedings in Informatics",
volume = 268,
pages = "38:1--38:8",
year = 2023,
doi = "10.4230/LIPIcs.ITP.2023.38"
}