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

Research output: Contribution to journalJournal article – Annual report year: 2018Researchpeer-review

Documents

DOI

View graph of relations

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
CitationsWeb of Science® Times Cited: No match on DOI

    Research areas

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

Download statistics

No data available

ID: 149476666