Hybrid tableaux for the difference modality

DOI10.1016/J.ENTCS.2009.02.039zbMATH Open1347.03044OpenAlexW2002949351MaRDI QIDQ4982124FDOQ4982124

Authors: Mark Kaminski, Gert Smolka 

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

Recommendations

• Terminating tableau systems for hybrid logic with difference and converse
• Lightweight hybrid tableaux
• Termination for Hybrid Tableaus
• Terminating Tableaux for Hybrid Logic with the Difference Modality and Converse
• Decision procedures for some strong hybrid logics

zbMATH Keywords

modal logicdecision procedureshybrid logicdifference modalityterminating tableaux

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Mechanization of proofs and logical operations (03B35) Logic in computer science (03B70)

Cites Work

• Modal logic
• Title not available (Why is that?)
• The modal logic of inequality
• EXPtime tableaux for ALC
• Handbook of modal logic
• Title not available (Why is that?)
• The Taming of the Cut. Classical Refutations with Analytic Cut
• Title not available (Why is that?)
• Title not available (Why is that?)
• Strongly analytic tableaux for normal modal logics
• Are tableaux an improvement on truth-tables? Cut-free proofs and bivalence
• Higher-order syntax and saturation algorithms for hybrid logic
• Modal logic with names
• The computational complexity of hybrid temporal logics
• Modal definability in enriched languages
• Derivation rules as anti-axioms in modal logic
• Tableau-based Decision Procedures for Hybrid Logic
• Building decision procedures for modal logics from propositional decision procedures -- the case study of modal K
• Termination for Hybrid Tableaus
• Display Calculi for Nominal Tense Logics
• A simple tableau system for the logic of elsewhere

Cited In (11)

• Hybrid logic with the difference modality for generalisations of graphs
• Minimal structures for modal tableaux: Some examples
• Terminating Tableaux for Hybrid Logic with the Difference Modality and Converse
• Decision procedures for some strong hybrid logics
• Clausal graph tableaux for hybrid logic with eventualities and difference
• Symmetric blocking
• Termination for Hybrid Tableaus
• Lightweight hybrid tableaux
• 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

This page was built for publication: Hybrid tableaux for the difference modality

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