Formalizing axiomatic systems for propositional logic in Isabelle/HOL

DOI10.1007/978-3-030-81097-9_3zbMath1485.68292OpenAlexW3186360832MaRDI 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

completenesspropositional logicsoundnessIsabelle/HOLaxiomatic systems

Mathematics Subject Classification ID

Classical propositional logic (03B05) Subsystems of classical logic (including intuitionistic logic) (03B20) Formalization of mathematics in connection with theorem provers (68V20)

Uses Software

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

Cites Work

• Isabelle/HOL. A proof assistant for higher-order logic
• Extending Sledgehammer with SMT solvers
• Formalizing Bachmair and Ganzinger's ordered resolution prover
• Finding missing proofs with automated reasoning
• Epistemic Logic
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Formalizing axiomatic systems for propositional logic in Isabelle/HOL