Abstract
We describe novel axiomatic systems for classical propositional logic: one based on the K and S combinators and elimination rules and one on transitivity of implication, explosion and rules for disjunction. We show how Isabelle/HOL helps investigate such systems.
| Original language | English |
|---|---|
| Title of host publication | Proceedings of 27th International Conference on Types for Proofs and Programs |
| Number of pages | 3 |
| Publication date | 2021 |
| Publication status | Published - 2021 |
| Event | 27th International Conference on Types for Proofs and Programs - Virtual Event Duration: 14 Jun 2021 → 18 Jun 2021 Conference number: 27 https://types21.liacs.nl/ |
Conference
| Conference | 27th International Conference on Types for Proofs and Programs |
|---|---|
| Number | 27 |
| Location | Virtual Event |
| Period | 14/06/2021 → 18/06/2021 |
| Internet address |