Hybrid Tableaux for the Difference Modality

DOI10.1016/j.entcs.2009.02.039zbMath1347.03044MaRDI QIDQ4982124

Gert Smolka, Mark Kaminski

Publication date: 23 March 2015

Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.entcs.2009.02.039

zbMATH Keywords

modal logic; hybrid logic; decision procedures; difference modality; terminating tableaux

Mathematics Subject Classification ID

03B45: Modal logic (including the logic of norms)

03B70: Logic in computer science

03B35: Mechanization of proofs and logical operations

Related Items

Lightweight hybrid tableaux, Symmetric blocking, Terminating tableau systems for hybrid logic with difference and converse, A prover dealing with nominals, binders, transitivity and relation hierarchies, Modal Tableau Systems with Blocking and Congruence Closure, Terminating Tableaux for Hybrid Logic with the Difference Modality and Converse

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Modal definability in enriched languages
• Modal logic with names
• Are tableaux an improvement on truth-tables? Cut-free proofs and bivalence
• EXPtime tableaux for ALC
• Higher-Order Syntax and Saturation Algorithms for Hybrid Logic
• Tableau-based Decision Procedures for Hybrid Logic
• The modal logic of inequality
• Derivation rules as anti-axioms in modal logic
• The Taming of the Cut. Classical Refutations with Analytic Cut
• The computational complexity of hybrid temporal logics
• A simple tableau system for the logic of elsewhere
• Building decision procedures for modal logics from propositional decision procedures — The case study of modal K
• Display Calculi for Nominal Tense Logics
• Strongly analytic tableaux for normal modal logics
• Termination for Hybrid Tableaus