Terminating Tableaux for Hybrid Logic with Eventualities

DOI10.1007/978-3-642-14203-1_21zbMath1291.03019MaRDI QIDQ5747764

Mark Kaminski, Gert Smolka

Publication date: 14 September 2010

Published in: Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-14203-1_21

Mathematics Subject Classification ID

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

03B35: Mechanization of proofs and logical operations

Related Items

A goal-directed decision procedure for hybrid PDL, The expressibility of fragments of hybrid graph logic on finite digraphs, Correctness and Worst-Case Optimality of Pratt-Style Decision Procedures for Modal and Hybrid Logics, Constructive Formalization of Hybrid Logic with Eventualities

Uses Software

• Spartacus

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Terminating tableau systems for hybrid logic with difference and converse
• Using branching time temporal logic to synthesize synchronization skeletons
• A near-optimal method for reasoning about action
• Propositional dynamic logic of regular programs
• Combining deduction and model checking into tableaux and algorithms for converse-PDL.
• A tableau decision procedure for \(\mathcal{SHOIQ}\)
• Tableau-based Decision Procedures for Hybrid Logic
• Terminating Tableaux for Hybrid Logic with the Difference Modality and Converse
• “Sometimes” and “not never” revisited
• An On-the-fly Tableau-based Decision Procedure for PDL-satisfiability
• An Optimal On-the-Fly Tableau-Based Decision Procedure for PDL-Satisfiability
• Termination for Hybrid Tableaus