2026-07-21T19:38:28Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:3119 2024-03-06T10:33:49Z ddc:004 open_access

Automated Certified Proofs with CiME3 Contejean, Évelyne Courtieu, Pierre Forest, Julien Pons, Olivier Urbain, Xavier Rewriting Formal Proof Proof Automation Proof Assistant We present the rewriting toolkit CiME3. Amongst other original features, this version enjoys two kinds of engines: to handle and discover proofs of various properties of rewriting systems, and to generate Coq scripts from proof traces given in certification problem format in order to certify them with a skeptical proof assistant like Coq. Thus, these features open the way for using CiME3 to add automation to proofs of termination or confluence in a formal development in the Coq proof assistant. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Évelyne Contejean and Pierre Courtieu and Julien Forest and Olivier Pons and Xavier Urbain 2011 Is Part Of LIPIcs, Volume 10, 22nd International Conference on Rewriting Techniques and Applications (RTA'11) (2011) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.RTA.2011.21 urn:nbn:de:0030-drops-31192 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2011.21 eng https://creativecommons.org/licenses/by-nc-nd/3.0/legalcode