Constructive Formalization of Hybrid Logic with Eventualities

DOI10.1007/978-3-642-25379-9_3MaRDI QIDQ3100197zbMATH OpenOpenAlexFDO

Authors Christian Doczkal, Gert Smolka

Publication date 22 November 2011

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

Full work available at URL https://doi.org/10.1007/978-3-642-25379-9_3

zbMATH Keywords

Coqdecision procedureseventualitieshybrid logicsmall model theoremSsreflect

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45)

Recommendations

• Terminating Tableaux for Hybrid Logic with Eventualities
• Constructive description logics hybrid-style
• scientific article; zbMATH DE number 5587277
• Hybrid formulas and elementarily generated modal logics
• Hybrid logic and its proof-theory
• scientific article; zbMATH DE number 4049019
• Sequent calculus for hybrid logic
• Proof-Based Approach to Hybrid Systems Development: Dynamic Logic and Event-B
• Axiomatizing hybrid logic using modal logic

Cites work

• A machine-checked implementation of Buchberger's algorithm
• A Modular Formalisation of Finite Group Theory
• Correctness and worst-case optimality of Pratt-style decision procedures for modal and hybrid logics
• Decision procedures and expressiveness in the temporal logic of branching time
• Handbook of modal logic
• scientific article; zbMATH DE number 1301852 (Why is no real title available?)
• Kripke models for classical logic
• Mechanised computability theory
• Packaging Mathematical Structures
• Propositional dynamic logic of regular programs
• Terminating Tableaux for Hybrid Logic with Eventualities
• Using branching time temporal logic to synthesize synchronization skeletons

Cited in

(3)

• Formalizing a Seligman-style tableau system for hybrid logic (short paper)
• Terminating Tableaux for Hybrid Logic with Eventualities
• Synthetic completeness for a terminating Seligman-style tableau system

Describes a project that uses

Uses Software

• Coq
• Coq/SSReflect

This page was built for publication: Constructive Formalization of Hybrid Logic with Eventualities

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