Verified Prover (Q40509)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
AFP entry Verified-Prover
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | Verified Prover |
AFP entry Verified-Prover |
Statements
Tom Ridge
0 references
Soundness and completeness for a system of first order logic are formally proved, building on James Margetson's formalization of work by Wainer and Wallen. The completeness proofs naturally suggest an algorithm to derive proofs. This algorithm, which can be implemented tail recursively, is formalized in Isabelle/HOL. The algorithm can be executed via the rewriting tactics of Isabelle. Alternatively, the definitions can be exported to OCaml, yielding a directly executable program.
0 references
28 September 2004
0 references
A Mechanically Verified, Efficient, Sound and Complete Theorem Prover For First Order Logic (English)
0 references
