Code Generation for a Simple First-Order Prover

Jørgen Villadsen, Anders Schlichtkrull, Andreas Halkjær From

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

266 Downloads (Pure)


We present Standard ML code generation in Isabelle/HOL of a sound and complete prover for first-order logic, taking formalizations by Tom Ridge and others as the starting point. We also define a set of so-called unfolding rules and show how to use these as a simple prover, with the aim of using the approach for teaching logic and verification to computer science students at the bachelor level.
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
  • First-order logic
  • Soundness
  • Completeness
  • Code generation
  • Unfolding rules
  • Standard ML
  • Isabelle/ML


Dive into the research topics of 'Code Generation for a Simple First-Order Prover'. Together they form a unique fingerprint.

Cite this