Certification of Confluence Proofs using CeTA

Julian Nagele and René Thiemann

Proceedings of the 3rd International Workshop on Confluence (IWC 2014), pp. 19 – 23, 2014.


CeTA was originally developed as a tool for certifying termination proofs which have to be provided as certificates in the CPF-format. Its soundness is proven as part of IsaFoR, the Isabelle Formalization of Rewriting. By now, CeTA can also be used for certifying confluence and non-confluence proofs. In this system description, we give a short overview on what kind of proofs are supported, and what information has to be given in the certificates. As we will see, only a small amount of information is required and so we hope that CSI will not stay the only confluence tool which can produce certificates.




author = "Julian Nagele and Ren{\'e} Thiemann",
title = "Certification of Confluence Proofs using {CeTA}",
booktitle = "Proceedings of the 3rd International Workshop on Confluence",
editor = "Takahito Aoto and Delia Kesner",
pages = "19--23",
year = 2014
Nach oben scrollen