Development Closed Critical Pairs: Towards a Formalized Proof
Christina Kohl, Aart MiddeldorpProceedings of the 11th International Workshop on Confluence (IWC 2022), pp. 2-6, 2022.
Abstract
Having development closed critical pairs is a well-known sufficient condition for confluence of left-linear term rewrite systems. We present formalized results involving proof terms and unification that play an important role in the proof.
BibTeX
@inproceedings{CKAM-IWC22,
author = "Christina Kohl and Aart Middeldorp",
title = "Development Closed Critical Pairs: Towards a Formalized
Proof",
booktitle = "Proceedings of the 11th International Workshop on Confluence",
pages = "2--6",
year = 2022
}