A henkin-style completeness proof for the modal logic S5

DOI10.1007/978-3-030-89391-0_25OpenAlexW3208200734MaRDI QIDQ2695534

Bruno Bentzen

Publication date: 31 March 2023

Full work available at URL: https://arxiv.org/abs/1910.01697

zbMATH Keywords

modal logiccompletenessformal methodslean

Mathematics Subject Classification ID

Logic in artificial intelligence (68T27) Logic in computer science (03B70)

Related Items (2)

Constructive and mechanised meta-theory of intuitionistic epistemic logic ⋮ Mechanising Gödel-Löb provability logic in HOL light

Uses Software

• Coq
• Agda
• Lean
• Archive Formal Proofs

Cites Work

• Unnamed Item
• Unnamed Item
• The calculus of constructions
• A formalised proof of the soundness and completeness of a simply typed lambda-calculus with explicit substitutions
• Formalizing Cut Elimination of Coalgebraic Logics in Coq
• Completeness and Decidability Results for CTL in Coq
• Forcing-Based Cut-Elimination for Gentzen-Style Intuitionistic Sequent Calculus
• Dependently Typed Programming in Agda
• Constructive Completeness for Modal Logic with Transitive Closure
• Verified Decision Procedures for Modal Logics.
• Inductively defined types in the Calculus of Constructions

This page was built for publication: A henkin-style completeness proof for the modal logic S5