Formalizing axiomatic systems for propositional logic in Isabelle/HOL

DOI10.1007/978-3-030-81097-9_3MaRDI QIDQ2128791zbMATH OpenOpenAlexFDO

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

Publication date 22 April 2022

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

zbMATH Keywords

axiomatic systemscompletenessIsabelle/HOLpropositional logicsoundness

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)

Recommendations

• Formalized proof systems for propositional logic
• scientific article; zbMATH DE number 2110621
• Formalizing Hilbert's Grundlagen in Isabelle/Isar
• Isabelle/HOL. A proof assistant for higher-order logic
• Isabelle/HOL/GST: a formal proof environment for generalized set theories
• scientific article; zbMATH DE number 1301858
• Programming and verifying a declarative first-order prover in Isabelle/HOL
• scientific article; zbMATH DE number 2003161
• Higher-order separation logic in Isabelle/HOLCF
• A sequent calculus for first-order logic formalized in Isabelle/HOL

Cites work

• Epistemic Logic
• Extending Sledgehammer with SMT solvers
• Finding missing proofs with automated reasoning
• Formalized proof systems for propositional logic
• Formalizing Bachmair and Ganzinger's ordered resolution prover
• scientific article; zbMATH DE number 3122413 (Why is no real title available?)
• scientific article; zbMATH DE number 1865568 (Why is no real title available?)
• scientific article; zbMATH DE number 3045411 (Why is no real title available?)
• Isabelle/HOL. A proof assistant for higher-order logic

Cited in

(4)

• Isabelle/HOL. A proof assistant for higher-order logic
• An Axiomatic Value Model for Isabelle/UTP
• scientific article; zbMATH DE number 4191139 (Why is no real title available?)
• scientific article; zbMATH DE number 2110621 (Why is no real title available?)

Describes a project that uses

Uses Software

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

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2128791)