Abstract
We consider a plethora of well-known axiomatic systems, and some less well-known variants, for classical propositional logic all with soundness and completeness theorems formalized in the proof assistant Isabelle/HOL. We have previously only formalized systems based on either implication and falsity or on disjunction and negation. We have now formalized 12 additional systems based on implication and negation. Each of them has three or more axioms. We have also formalized single-axiom systems, by Lukasiewicz and Tarski as well as by Meredith, and we describe the formalization of the former in detail. A few systems with two axioms are described too.
| Original language | English |
|---|---|
| Title of host publication | Proceedings of Logic & Artificial Intelligence |
| Publisher | Vladimir Andrunachievici Institute of Mathematics and Computer Science |
| Publication date | 2023 |
| Pages | 7-22 |
| ISBN (Print) | 978-9975-68-484-2 |
| Publication status | Published - 2023 |
| Event | Logic and Artificial Intelligence 2022 - Virtual Duration: 12 Jan 2022 → 16 Jan 2022 |
Conference
| Conference | Logic and Artificial Intelligence 2022 |
|---|---|
| City | Virtual |
| Period | 12/01/2022 → 16/01/2022 |