Automated Certified Proofs with CiME3

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.

This document was translated from L^AT_EX by H^EV^EA.