Formalizing axiomatic systems for propositional logic in Isabelle/HOL

DOI10.1007/978-3-030-81097-9_3zbMath1485.68292MaRDI QIDQ2128791

Jørgen Villadsen, Asta Halkjær From, Agnes Moesgård Eschen

Publication date: 22 April 2022

Full work available at URL: https://orbit.dtu.dk/en/publications/a8f3ad6e-d47f-450f-a889-5af864770732

zbMATH Keywords

completeness; propositional logic; soundness; Isabelle/HOL; axiomatic systems

Mathematics Subject Classification ID

03B05: Classical propositional logic

03B20: Subsystems of classical logic (including intuitionistic logic)

68V20: Formalization of mathematics in connection with theorem provers

Uses Software

• Isabelle
• Isabelle/HOL
• HOL
• Sledgehammer
• Archive Formal Proofs
• Epistemic Logic

Cites Work

• Epistemic Logic