Conference paper
Certified Soundness of Simplest Known Formulation of First-Order Logic
In
Proceedings of the Esslli 2017 Student Session
—
2017, pp. 25-36
Abstract
In 1965, Donald Monk published a paper about an axiomatic system for first-order predicate logic that he described as “the simplest known formulation of ordinary logic”. In this paper we show work in progress on certifying soundness of this system in the interactive proof assistant Isabelle. Through this work we demonstrate the usefulness of using proof assistants for validating mathematical results.
This work also establishes an outline for future work such as a certified completeness proof of the axiomatic system in Isabelle.
| Language: | English |
|---|---|
| Year: | 2017 |
| Pages: | 25-36 |
| Proceedings: | 29th European Summer School in Logic, Language & Information |
| Types: | Conference paper |
| ORCIDs: | Larsen, John Bruntse |
