Reflecting Proofs in First-Order Logic with Equality

12 years 5 months ago
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...
Evelyne Contejean, Pierre Corbineau
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2005
Where CADE
Authors Evelyne Contejean, Pierre Corbineau
Comments (0)