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.
| Original language | English |
|---|---|
| Title of host publication | Proceedings of the ESSLLI 2017 Student Session |
| Publication date | 2017 |
| Pages | 25-36 |
| Publication status | Published - 2017 |
| Event | 29th European Summer School in Logic, Language & Information
- Toulouse, France Duration: 17 Jul 2017 → 28 Jul 2017 Conference number: 29 |
Conference
| Conference | 29th European Summer School in Logic, Language & Information |
|---|---|
| Number | 29 |
| Country/Territory | France |
| City | Toulouse |
| Period | 17/07/2017 → 28/07/2017 |