A Mechanically Verified, Efficient, Sound and Complete Theorem Prover For First Order Logic

Title:	A Mechanically Verified, Efficient, Sound and Complete Theorem Prover For First Order Logic
Author:	Tom Ridge
Submission date:	2004-09-28
Abstract:	Soundness and completeness for a system of first order logic are formally proved, building on James Margetson's formalization of work by Wainer and Wallen. The completeness proofs naturally suggest an algorithm to derive proofs. This algorithm, which can be implemented tail recursively, is formalized in Isabelle/HOL. The algorithm can be executed via the rewriting tactics of Isabelle. Alternatively, the definitions can be exported to OCaml, yielding a directly executable program.
BibTeX:	@article{Verified-Prover-AFP, author = {Tom Ridge}, title = {A Mechanically Verified, Efficient, Sound and Complete Theorem Prover For First Order Logic}, journal = {Archive of Formal Proofs}, month = sep, year = 2004, note = {\url{https://isa-afp.org/entries/Verified-Prover.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.