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

147 Downloads (Pure)

Abstract

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
http://www21.in.tum.de/~nipkow/Isabelle2016/

Workshop

WorkshopIsabelle Workshop 2016
Country/TerritoryFrance
CityNancy
Period25/08/201626/08/2016
OtherAssociated with ITP 2016: Interactive Theorem Proving
Internet address

Keywords

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

Fingerprint

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

Cite this