Abstract | ||
---|---|---|
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. |
Year | Venue | Field |
---|---|---|
2015 | CoRR | Algorithm,Mathematical proof,Confluence,Rewriting,Soundness,Certification,Mathematics |
DocType | Volume | Citations |
Journal | abs/1505.01337 | 3 |
PageRank | References | Authors |
0.39 | 5 | 2 |
Name | Order | Citations | PageRank |
---|---|---|---|
Julian Nagele | 1 | 21 | 6.95 |
René Thiemann | 2 | 984 | 69.38 |