A Verified Simple Prover for First-Order Logic

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

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

369 Downloads (Pure)


We present a simple prover for first-order logic with certified soundness and completeness in Isabelle/HOL, taking formalizations by Tom Ridge and others as the starting point, but with the aim of using the approach for teaching logic and verification to computer science students at the bachelor level. The prover is simple in the following sense: It is purely functional and can be executed with rewriting rules or as code generation to a number of functional programming languages. The prover uses no higher-order functions, that is, no function takes a function as argument or returns a function as its result. This is advantageous when students perform rewriting steps by hand. The prover uses the logic of first-order logic on negation normal form with a term language consisting of only variables. This subset of the full syntax of first-order logic allows for a simple proof system without resorting to the much weaker propositional logic.
Original languageEnglish
Title of host publicationProceedings of the 6th Workshop on Practical Aspects of Automated Reasoning (PAAR)
EditorsBoris Konev, Josef Urban, Philipp Rümmer
Publication date2018
Publication statusPublished - 2018
Event6th Workshop on Practical Aspects of Automated Reasoning (PAAR) - Oxford, United Kingdom
Duration: 19 Jul 201819 Jul 2018


Workshop6th Workshop on Practical Aspects of Automated Reasoning (PAAR)
Country/TerritoryUnited Kingdom
SeriesCEUR Workshop Proceedings


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

Cite this