A Small Framework for Proof Checking

9 years 2 months ago
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.
Hans de Nivelle, Piotr Witkowski
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2008
Where CADE
Authors Hans de Nivelle, Piotr Witkowski
Comments (0)