Constructive and mechanised meta-theory of intuitionistic epistemic logic

DOI10.1007/978-3-030-93100-1_7OpenAlexW4200520344MaRDI QIDQ2151399

Dominik Kirst, Christian Hagemeier

Publication date: 1 July 2022

Full work available at URL: https://doi.org/10.1007/978-3-030-93100-1_7

zbMATH Keywords

completenessepistemic logicconstructivisation

Mathematics Subject Classification ID

Logic in computer science (03B70)

Uses Software

• Coq

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Completeness and decidability results for CTL in constructive type theory
• Does the deduction theorem fail for modal logic?
• The calculus of constructions
• Formalized meta-theory of sequent calculi for substructural logics
• Cut-elimination for provability logic by terminating proof-search: formalised and deconstructed using Coq
• Completeness theorems for first-order logic analysed in constructive type theory
• First-order intuitionistic epistemic logic
• A henkin-style completeness proof for the modal logic S5
• Constructive Completeness for Modal Logic with Transitive Closure
• Categorical and algebraic aspects of the intuitionistic modal logic IEL― and its predicate extensions
• Cut elimination and complexity bounds for intuitionistic epistemic logic
• An Arithmetical Interpretation of Verification and Intuitionistic Knowledge
• The Independence of Markov's Principle in Type Theory.
• INTUITIONISTIC EPISTEMIC LOGIC

This page was built for publication: Constructive and mechanised meta-theory of intuitionistic epistemic logic