Abstract
We present Standard ML code generation in Isabelle/HOL of a sound and complete prover for first-order logic, taking formalizations by Tom Ridge and others as the starting point. We also define a set of so-called unfolding rules and show how to use these as a simple prover, with the aim of using the approach for teaching logic and verification to computer science students at the bachelor level.
| 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
- First-order logic
- Soundness
- Completeness
- Code generation
- Unfolding rules
- Standard ML
- Isabelle/ML