First-Order Logic According to Harrison

Alexander Birch Jensen 🌐, Anders Schlichtkrull 🌐 and Jørgen Villadsen 🌐

January 1, 2017

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


We present a certified declarative first-order prover with equality based on John Harrison's Handbook of Practical Logic and Automated Reasoning, Cambridge University Press, 2009. ML code reflection is used such that the entire prover can be executed within Isabelle as a very simple interactive proof assistant. As examples we consider Pelletier's problems 1-46.

Reference: Programming and Verifying a Declarative First-Order Prover in Isabelle/HOL. Alexander Birch Jensen, John Bruntse Larsen, Anders Schlichtkrull & Jørgen Villadsen. AI Communications 31:281-299 2018.

See also: Students' Proof Assistant (SPA).


BSD License


July 21, 2018
Proof of Pelletier's problem 34 (Andrews's Challenge) thanks to Asta Halkjær From.


Session FOL_Harrison