Hybrid tableaux for the difference modality

DOI10.1016/J.ENTCS.2009.02.039MaRDI QIDQ4982124zbMATH OpenOpenAlexFDO

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

zbMATH Keywords

decision proceduresdifference modalityhybrid logicmodal logicterminating tableaux

Mathematics Subject Classification ID

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

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

Cites work

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

Cited in

(11)

• Terminating tableau systems for hybrid logic with difference and converse
• A prover dealing with nominals, binders, transitivity and relation hierarchies
• Minimal structures for modal tableaux: Some examples
• Modal tableau systems with blocking and congruence closure
• Terminating Tableaux for Hybrid Logic with the Difference Modality and Converse
• Clausal graph tableaux for hybrid logic with eventualities and difference
• Decision procedures for some strong hybrid logics
• Termination for Hybrid Tableaus
• Lightweight hybrid tableaux
• Hybrid logic with the difference modality for generalisations of graphs
• Symmetric blocking

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)