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 proofs traces input in certification proof format (CPF) (an XML format widely accepted by the certified rewriting community) in order to certify them with a skeptical proof assistant like COQ. CiME3 may thus be used 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.