Termination for Hybrid Tableaus

DOI10.1093/logcom/exm014zbMath1140.03005OpenAlexW2067803913WikidataQ57813480 ScholiaQ57813480MaRDI QIDQ5431611

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

modal logichybrid logictableau systemsdecision proceduresloop-checks

Mathematics Subject Classification ID

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

Related Items (27)

An efficient approach to nominal equalities in hybrid logic tableaux ⋮ Modal Tableau Systems with Blocking and Congruence Closure ⋮ Terminating Tableaux for Dynamic Epistemic Logics ⋮ Reflecting on social influence in networks ⋮ 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? ⋮ Terminating Tableaux for Hybrid Logic with the Difference Modality and Converse ⋮ 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 ⋮ Global Caching for Coalgebraic Description Logics ⋮ Terminating Tableaux for Hybrid Logic with Eventualities ⋮ Herod and Pilate: Two Tableau Provers for Basic Hybrid Logic ⋮ A logic for diffusion in social networks ⋮ Coalgebraic Hybrid Logic ⋮ ExpTime tableaux with global caching for hybrid PDL ⋮ A prover dealing with nominals, binders, transitivity and relation hierarchies ⋮ 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 ⋮ Sequent calculi and decidability for intuitionistic hybrid logic ⋮ Terminating tableau systems for hybrid logic with difference and converse ⋮ Formalizing a Seligman-style tableau system for hybrid logic (short paper) ⋮ Modal Satisfiability via SMT Solving ⋮ 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

Uses Software

• Herod
• Pilate

This page was built for publication: Termination for Hybrid Tableaus