Termination for Hybrid Tableaus
From MaRDI portal
Publication:5431611
DOI10.1093/logcom/exm014zbMath1140.03005WikidataQ57813480 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
03B45: Modal logic (including the logic of norms)
03B25: Decidability of theories and sets of sentences
03B35: Mechanization of proofs and logical operations
Related Items
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, 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?, Sequent calculi and decidability for intuitionistic hybrid logic, 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, An efficient approach to nominal equalities in hybrid logic tableaux, 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
Uses Software
