swMATH ID: 32220
Software Authors: Alexander Birch Jensen, Anders Schlichtkrull, Jørgen Villadsen
Description: First-Order Logic According to Harrison. 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
Homepage: https://www.isa-afp.org/entries/FOL_Harrison.html
Dependencies: Isabelle
Related Software: Verified Prover; Archive Formal Proofs; FOL Fitting; Superposition Calculus; Completeness theorem; GitHub; Sledgehammer; Isar; Isabelle/HOL; Isabelle; Metamath; Isabelle/jEdit; HOL; Isabelle/Isar; Propositional Resolution; Incredible Proof Machine; Abstract Soundness; Lambda Free RPOs; Incompleteness Theorems; Abstract Completeness
Referenced in: 2 Publications

Referencing Publications by Year