Constructive Completeness for Modal Logic with Transitive Closure

DOI10.1007/978-3-642-35308-6_18zbMath1383.68074OpenAlexW101180772MaRDI QIDQ4916063

Christian Doczkal, Gert Smolka

Publication date: 19 April 2013

Published in: Certified Programs and Proofs (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-35308-6_18

zbMATH Keywords

modal logiccompletenessGentzen systemsdecision proceduresCoqconstructive proofsSsreflectHilbert systems

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Mechanization of proofs and logical operations (03B35)

Related Items (3)

Cyclic hypersequent calculi for some modal logics with the master modality ⋮ Constructive and mechanised meta-theory of intuitionistic epistemic logic ⋮ A henkin-style completeness proof for the modal logic S5

Uses Software

• Coq
• Coq/SSReflect

This page was built for publication: Constructive Completeness for Modal Logic with Transitive Closure