Abstract
We formalize in Isabelle/HOL the kernel of an LCF-style prover for first-order logic with equality from John Harrison’s Handbook of Practical Logic and Automated Reasoning. We prove the kernel sound and generate Standard ML code from the formalization. The generated code can then serve as a verified kernel. By doing this we also obtain verified components such as derived rules, a tableau prover, tactics, and a small declarative interactive theorem prover. We test that the kernel and the components give the same results as Harrison’s original on all the examples from his book. The formalization is 600 lines and is available online.
| Original language | English |
|---|---|
| Title of host publication | Proceedings of the Isabelle Workshop 2016 |
| Number of pages | 15 |
| Publication date | 2016 |
| Publication status | Published - 2016 |
| Event | Isabelle Workshop 2016 - Nancy, France Duration: 25 Aug 2016 → 26 Aug 2016 http://www21.in.tum.de/~nipkow/Isabelle2016/ |
Workshop
| Workshop | Isabelle Workshop 2016 |
|---|---|
| Country/Territory | France |
| City | Nancy |
| Period | 25/08/2016 → 26/08/2016 |
| Other | Associated with ITP 2016: Interactive Theorem Proving |
| Internet address |
Keywords
- Isabelle/HOL
- Verification
- First-order logic
- Equality
- Soundness
- LCF-style prover
- OCaml
- Code generation
- Standard ML (SML)
- Isabelle/ML