Reflecting Proofs in First-Order Logic with Equality

Our general goal is to provide better automation in interactive proof assistants such as Coq. We present an interpreter of proof traces in first-order multi-sorted logic with equality. Thanks to the reflection ability of Coq, this interpreter is both implemented and formally proved sound -- with respect to a reflective interpretation of formulae as Coq properties -- inside Coq's type theory. Our generic framework allows to interpret proofs traces computed by any automated theorem prover, as long as they are precise enough: we illustrate that on traces produced by the CiME tool when solving unifiability problems by ordered completion. We discuss some benchmark results obtained on the TPTP library. The aim of this paper is twofold: first we want to validate a reflective approach for proofs in interactive proof assistants, and second show how to provide a better automation for such assistants. Both aspects can be achieved by using external provers designed to automatically solve some...

• Type: Conference
• Year: 2005
• Where: CADE
• Authors: Evelyne Contejean, Pierre Corbineau
• Keywords: Automated Reasoning, CADE 2005, Fine Grained Proof, Interactive Proof Assistants, Proof Traces