Programming and verifying a declarative first-order prover in Isabelle/HOL

被引：8

作者：

Jensen, Alexander Birch ^{[1
]}

Larsen, John Bruntse ^{[1
]}

Schlichtkrull, Anders ^{[1
]}

Villadsen, Jorgen ^{[1
]}

机构：

[1] Tech Univ Denmark, DTU Compute, DK-2800 Lyngby, Denmark

来源：

AI COMMUNICATIONS | 2018年 / 31卷 / 03期

关键词：

Isabelle; verification; declarative proofs for first-order logic with equality; soundness; LCF-style prover; PROOF; FORMALIZATION; THEOREM; SOUNDNESS; CALCULUS;

D O I：

10.3233/AIC-180764

中图分类号：

TP18 [人工智能理论];

学科分类号：

081104 ; 0812 ; 0835 ; 1405 ;

摘要：

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).

引用

页码：281 / 299

页数：19