Formalizing Almost Development Closed Critical Pairs
Christina Kohl, Aart MiddeldorpProceedings of the 14th International Conference on Interactive Theorem Proving, 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
@inproceedings{CKAM-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"
}