Verification of an LCF-Style First-Order Prover with Equality

Alexander Birch Jensen, Anders Schlichtkrull, Jørgen Villadsen

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

189 Downloads (Pure)


We formalize in Isabelle/HOL the kernel of an LCF-style prover for first-order logic with equality from John Harrison’s Handbook of Practical Logic and Automated Reasoning. We prove the kernel sound and generate Standard ML code from the formalization. The generated code can then serve as a verified kernel. By doing this we also obtain verified components such as derived rules, a tableau prover, tactics, and a small declarative interactive theorem prover. We test that the kernel and the components give the same results as Harrison’s original on all the examples from his book. The formalization is 600 lines and is available online.
Original languageEnglish
Title of host publicationProceedings of the Isabelle Workshop 2016
Number of pages15
Publication date2016
Publication statusPublished - 2016
EventIsabelle Workshop 2016 - Nancy, France
Duration: 25 Aug 201626 Aug 2016


WorkshopIsabelle Workshop 2016
OtherAssociated with ITP 2016: Interactive Theorem Proving
Internet address


  • Isabelle/HOL
  • Verification
  • First-order logic
  • Equality
  • Soundness
  • LCF-style prover
  • OCaml
  • Code generation
  • Standard ML (SML)
  • Isabelle/ML


Dive into the research topics of 'Verification of an LCF-Style First-Order Prover with Equality'. Together they form a unique fingerprint.

Cite this