Certification of Confluence Proofs using CeTA
René ThiemannProceedings of the 1st International Workshop on Confluence (IWC 2012), pp. 45, 2012.
Abstract
We shortly report on the possibilities to certify confluence and non-confluence proofs via CeTA. Here,
proofs may use Newman’s lemma, critical pairs, weak orthogonality and non-joinable forks.
BibTeX
@inproceedings{RT-IWC12, author = "Ren{\'e} Thiemann", title = "Certification of Confluence Proofs using {CeTA}", booktitle = "Proceedings of the 1st International Workshop on Confluence", editor = "Nao Hirokawa and Aart Middeldorp", pages = "45", year = 2012, note = "\url{http://cl-informatik.uibk.ac.at/events/iwc-2012/}" }