Conference paper
On the Use of Isabelle/HOL for Formalizing New Concise Axiomatic Systems for Classical Propositional Logic
In
Proceedings of 27<sup>th</sup> International Conference on Types for Proofs and Programs
—
2021
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.
| Language: | English |
|---|---|
| Year: | 2021 |
| Proceedings: | 27<sup>th</sup> International Conference on Types for Proofs and Programs |
| Types: | Conference paper |
| ORCIDs: | From, Asta Halkjær and Villadsen, Jørgen |
