Termination for Hybrid Tableaus

DOI10.1093/LOGCOM/EXM014MaRDI QIDQ5431611zbMATH OpenOpenAlexWikidataFDO

Authors Thomas Bolander, Patrick Blackburn

Publication date 12 December 2007

Published in Journal Of Logic And Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1093/logcom/exm014

zbMATH Keywords

decision procedureshybrid logicloop-checksmodal logictableau systems

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35) Modal logic (including the logic of norms) (03B45)

Recommendations

• Terminating Tableaux for Hybrid Logic with Eventualities
• Hybrid tableaux for the difference modality
• Terminating tableau systems for hybrid logic with difference and converse
• Terminating Tableaux for Hybrid Logic with the Difference Modality and Converse
• Terminating Tableau Calculi for Hybrid Logics Extending K
• Hyper tableaux
• HTab: a terminating tableaux system for hybrid logic
• Tableau-based Decision Procedures for Hybrid Logic
• Alternation for termination
• Clausal tableaux for hybrid PDL

Cited in

(38)

• Terminating tableau systems for hybrid logic with difference and converse
• Reflecting on social influence in networks
• A logic for diffusion in social networks
• Formalizing a Seligman-style tableau system for hybrid logic (short paper)
• ExpTime tableaux with global caching for hybrid PDL
• A prover dealing with nominals, binders, transitivity and relation hierarchies
• A goal-directed decision procedure for hybrid PDL
• A tableau based decision procedure for an expressive fragment of hybrid logic with binders, converse and global modalities
• Internalization: The case of hybrid logics
• An efficient approach to nominal equalities in hybrid logic tableaux
• Completeness and termination for a Seligman-style tableau system
• A Tableaux Based Decision Procedure for a Broad Class of Hybrid Formulae with Binders
• Correctness and worst-case optimality of Pratt-style decision procedures for modal and hybrid logics
• Terminating tableaux for dynamic epistemic logics
• Modal tableau systems with blocking and congruence closure
• Terminating Tableaux for Hybrid Logic with the Difference Modality and Converse
• Coalgebraic Hybrid Logic
• scientific article; zbMATH DE number 1341482 (Why is no real title available?)
• HTab: a terminating tableaux system for hybrid logic
• Terminating Tableau Calculi for Hybrid Logics Extending K
• Hybrid tableaux for the difference modality
• Experiments in theorem proving for topological hybrid logic
• Modal Satisfiability via SMT Solving
• Global caching for coalgebraic description logics
• Terminating Tableaux for Hybrid Logic with Eventualities
• Herod and Pilate: two tableau provers for basic hybrid logic
• Terminating tableaux for graded hybrid logic with global modalities and role hierarchies
• Terminating tableaux for graded hybrid logic with global modalities and role hierarchies
• Lightweight hybrid tableaux
• Hybrid logic with the difference modality for generalisations of graphs
• Axiomatizing hybrid products. How can we reason many-dimensionally in hybrid logic?
• Data-aware hybrid tableaux
• Completeness of tableau calculi for two-dimensional hybrid logics
• Agent-knowledge logic for alternative epistemic logic
• Agent-knowledge logic for alternative epistemic logic
• Synthetic completeness for a terminating Seligman-style tableau system
• Terminating hybrid tableaus for ordered models
• Sequent calculi and decidability for intuitionistic hybrid logic

Describes a project that uses

Uses Software

• Herod
• Pilate

This page was built for publication: Termination for Hybrid Tableaus

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