Correctness and Worst-Case Optimality of Pratt-Style Decision Procedures for Modal and Hybrid Logics

DOI10.1007/978-3-642-22119-4_16zbMath1333.03008OpenAlexW134846372MaRDI QIDQ3010369

Gert Smolka, Mark Kaminski, Thomas Schneider

Publication date: 1 July 2011

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-22119-4_16

Mathematics Subject Classification ID

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

Related Items (6)

Completeness and decidability results for CTL in constructive type theory ⋮ Mechanising Gödel-Löb provability logic in HOL light ⋮ Verified Decision Procedures for Modal Logics. ⋮ Correctness and Worst-Case Optimality of Pratt-Style Decision Procedures for Modal and Hybrid Logics ⋮ Constructive Formalization of Hybrid Logic with Eventualities ⋮ A goal-directed decision procedure for hybrid PDL

Uses Software

• Racer

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Attributive concept descriptions with complements
• An essay in combinatory dynamic logic
• Automata-theoretic techniques for modal logics of programs
• An automata theoretic decision procedure for the propositional mu- calculus
• A near-optimal method for reasoning about action
• Propositional dynamic logic of regular programs
• Modal logic with names
• EXPtime tableaux for ALC
• Combining deduction and model checking into tableaux and algorithms for converse-PDL.
• Decision procedures and expressiveness in the temporal logic of branching time
• Optimizing terminological reasoning for expressive description logics
• Correctness and Worst-Case Optimality of Pratt-Style Decision Procedures for Modal and Hybrid Logics
• The computational complexity of hybrid temporal logics
• Clausal Graph Tableaux for Hybrid Logic with Eventualities and Difference
• An Optimal On-the-Fly Tableau-Based Decision Procedure for PDL-Satisfiability
• Termination for Hybrid Tableaus
• EXPTIME Tableaux with Global Caching for Description Logics with Transitive Roles, Inverse Roles and Role Hierarchies
• Optimal and Cut-Free Tableaux for Propositional Dynamic Logic with Converse
• Terminating Tableaux for Hybrid Logic with Eventualities

This page was built for publication: Correctness and Worst-Case Optimality of Pratt-Style Decision Procedures for Modal and Hybrid Logics