Development Closed Critical Pairs: Towards a Formalized Proof

Christina Kohl, Aart Middeldorp
Proceedings of the 11th International Workshop on Confluence (IWC 2022), pp. 2-6, 2022.

 pdf

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
}