Automated Certified Proofs with CiME3

. Contejean, P. Courtieu, J. Forest, O. Pons and X. Urbain

Abstract: 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 sceptical 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.

Full Paper

This document was translated from LATEX by HEVEA.