Programming and Verifying a Declarative First-Order Prover in Isabelle/HOL

Alexander Birch Jensen, John Bruntse Larsen, Anders Schlichtkrull, Jørgen Villadsen*

*Corresponding author for this work

Research output: Contribution to journalJournal articleResearchpeer-review

664 Downloads (Pure)

Abstract

We certify in the proof assistant Isabelle/HOL the soundness of a declarative first-order prover with equality. The LCF-style prover is a translation we have made, to Standard ML, of a prover in John Harrison’s Handbook of Practical Logic and Automated Reasoning. We certify it by replacing its kernel with a certified version that we program, certify and generate code from; all in Isabelle/HOL. In a declarative proof each step of the proof is declared, similar to the sentences in a thorough paper proof. The prover allows proofs to mix the declarative style with automatic theorem proving by using a tableau prover. Our motivation is teaching how automated and declarative provers work and how they are used. The prover allows studying concrete code and a formal verification of correctness. We show examples of proofs and how they are made in the prover. The entire development runs in Isabelle’s ML environment as an interactive application or can be used standalone in OCaml or Standard ML (or in other functional programming languages like Haskell and Scala with some additional work).
Original languageEnglish
JournalAI Communications
Volume31
Issue number3
Pages (from-to)281-299
ISSN0921-7126
DOIs
Publication statusPublished - 2018

Keywords

  • Isabelle
  • Verification
  • Declarative proofs for first-order logic with equality
  • Soundness
  • LCF-style prover

Fingerprint Dive into the research topics of 'Programming and Verifying a Declarative First-Order Prover in Isabelle/HOL'. Together they form a unique fingerprint.

Cite this