### Abstract

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. https://content.iospress.com/articles/ai-communications/aic764

See also: Students' Proof Assistant (SPA). https://github.com/logic-tools/spa

### License

BSD License

### History

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

### Topics

- Logic/General logic/Mechanization of proofs

### Session FOL_Harrison

- FOL_Harrison

## Cite

×

FOL_Harrison-AFP

    @article{FOL_Harrison-AFP,
      author  = {Alexander Birch Jensen and Anders Schlichtkrull and Jørgen Villadsen},
      title   = {First-Order Logic According to Harrison},
      journal = {Archive of Formal Proofs},
      month   = {January},
      year    = {2017},
      note    = {\url{https://isa-afp.org/entries/FOL_Harrison.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Jan 4, 2017 : Isabelle2016-1