Terminating Tableaux for Hybrid Logic with Eventualities

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

Gert Smolka, Mark Kaminski

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

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

Related Items (6)

Completeness and decidability results for CTL in constructive type theory ⋮ 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 ⋮ Clausal Tableaux for Hybrid PDL ⋮ Constructive Formalization of Hybrid Logic with Eventualities ⋮ A goal-directed decision procedure for hybrid PDL

Uses Software

• Spartacus

Cites Work

• 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
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Terminating Tableaux for Hybrid Logic with Eventualities