TY - GEN

T1 - A Verified Simple Prover for First-Order Logic

AU - Villadsen, Jørgen

AU - Schlichtkrull, Anders

AU - From, Andreas Halkjær

PY - 2018

Y1 - 2018

N2 - 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.

AB - 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.

UR - https://easychair.org/smart-slide/slide/M6k3#

M3 - Article in proceedings

T3 - CEUR Workshop Proceedings

SP - 88—104

BT - Proceedings of the 6th Workshop on Practical Aspects of Automated Reasoning (PAAR)

A2 - Konev, Boris

A2 - Urban, Josef

A2 - Rümmer, Philipp

PB - CEUR-WS

T2 - 6th Workshop on Practical Aspects of Automated Reasoning (PAAR)

Y2 - 19 July 2018 through 19 July 2018

ER -