Terminating Tableaux for Hybrid Logic with Eventualities

DOI10.1007/978-3-642-14203-1_21MaRDI QIDQ5747764zbMATH OpenOpenAlexFDO

Authors 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

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

Recommendations

• Terminating Tableaux for Hybrid Logic with the Difference Modality and Converse
• Terminating Tableau Calculi for Hybrid Logics Extending K
• HTab: a terminating tableaux system for hybrid logic
• Terminating tableau systems for hybrid logic with difference and converse
• Terminating tableaux for graded hybrid logic with global modalities and role hierarchies
• Terminating tableaux for graded hybrid logic with global modalities and role hierarchies
• Terminating tableaux for dynamic epistemic logics
• scientific article; zbMATH DE number 1341482
• scientific article; zbMATH DE number 1950252
• Constructive Formalization of Hybrid Logic with Eventualities

Cites work

• A near-optimal method for reasoning about action
• A tableau decision procedure for \(\mathcal{SHOIQ}\)
• An on-the-fly tableau-based decision procedure for PDL-satisfiability
• An Optimal On-the-Fly Tableau-Based Decision Procedure for PDL-Satisfiability
• Combining deduction and model checking into tableaux and algorithms for converse-PDL.
• Handbook of modal logic
• scientific article; zbMATH DE number 67500 (Why is no real title available?)
• scientific article; zbMATH DE number 1556014 (Why is no real title available?)
• scientific article; zbMATH DE number 1765663 (Why is no real title available?)
• Modal logic
• Propositional dynamic logic of regular programs
• Tableau-based Decision Procedures for Hybrid Logic
• Terminating tableau systems for hybrid logic with difference and converse
• Terminating Tableaux for Hybrid Logic with the Difference Modality and Converse
• Termination for Hybrid Tableaus
• Using branching time temporal logic to synthesize synchronization skeletons
• “Sometimes” and “not never” revisited

Cited in

(12)

• Terminating tableau systems for hybrid logic with difference and converse
• A goal-directed decision procedure for hybrid PDL
• The expressibility of fragments of hybrid graph logic on finite digraphs
• Clausal tableaux for hybrid PDL
• Completeness and decidability results for CTL in constructive type theory
• Correctness and worst-case optimality of Pratt-style decision procedures for modal and hybrid logics
• Constructive Formalization of Hybrid Logic with Eventualities
• Clausal graph tableaux for hybrid logic with eventualities and difference
• HTab: a terminating tableaux system for hybrid logic
• Terminating Tableau Calculi for Hybrid Logics Extending K
• Termination for Hybrid Tableaus
• On temporal references via definite descriptions in first-order monadic logic of order

Describes a project that uses

Uses Software

• Spartacus

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

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