Journal article
First-Order Logic According to Harrison
In
Archive of Formal Proofs
—
2017, pp. 1-66
Abstract
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.
| Language: | English |
|---|---|
| Year: | 2017 |
| Pages: | 1-66 |
| ISSN: | 2150914x |
| Types: | Journal article |
| ORCIDs: | Jensen, Alexander Birch , Schlichtkrull, Anders and Villadsen, Jørgen |
