Constructive Formalization of Hybrid Logic with Eventualities

DOI10.1007/978-3-642-25379-9_3zbMath1350.68230OpenAlexW2200608472MaRDI QIDQ3100197

Gert Smolka, Christian Doczkal

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

hybrid logiceventualitiesdecision proceduresCoqSsreflectsmall model theorem

Mathematics Subject Classification ID

Related Items (1)

Formalizing a Seligman-style tableau system for hybrid logic (short paper)

Uses Software

• Coq
• Coq/SSReflect

Cites Work

• Unnamed Item
• Unnamed Item
• Kripke models for classical logic
• Using branching time temporal logic to synthesize synchronization skeletons
• Propositional dynamic logic of regular programs
• A machine-checked implementation of Buchberger's algorithm
• Decision procedures and expressiveness in the temporal logic of branching time
• Correctness and Worst-Case Optimality of Pratt-Style Decision Procedures for Modal and Hybrid Logics
• Mechanised Computability Theory
• Packaging Mathematical Structures
• A Modular Formalisation of Finite Group Theory
• Terminating Tableaux for Hybrid Logic with Eventualities

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