A Small Framework for Proof Checking

We describe a framework with which first order theorem provers can be used for checking formal proofs. The main aim of the framework is to take as much advantage as possible from the strength of first order theorem provers in the formalization of realistic formal proofs. In order to obtain this, we restricted the use of higher order constructs to a minimum. In particular, we refrained from notation in formulas and from currying. The first order prover can be freely chosen. All communication with the theorem prover uses TPTP syntax. The system is intended for teaching, for checking mathematical proofs or correctness proofs of algorithms and also for improving the effectiveness of theorem provers. In its current set up, the system is not intended for building large libraries of checked mathematics.

• Type: Conference
• Year: 2008
• Where: CADE
• Authors: Hans de Nivelle, Piotr Witkowski
• Keywords: Automated Reasoning, CADE 2008, Order Theorem Provers, Prover Uses Tptp, Realistic Formal Proofs