Terminating tableau systems for hybrid logic with difference and converse
From MaRDI portal
Publication:1047795
The paper presents a tableau-based decision procedure for hybrid logic with global, difference, and converse modalities, considering also reflexive and transitive relations. The main contributions are a new model existence theorem, a terminating control that does not rely on the usual chain-based blocking scheme, a new treatment of the equational constraints that come with nominals and difference, and a terminating tableau for difference modalities.
Recommendations
- Terminating Tableaux for Hybrid Logic with the Difference Modality and Converse
- Terminating Tableaux for Hybrid Logic with Eventualities
- Terminating Tableau Calculi for Hybrid Logics Extending K
- HTab: a terminating tableaux system for hybrid logic
- A tableau system for quasi-hybrid logic
- scientific article; zbMATH DE number 1341482
- Terminating tableaux for graded hybrid logic with global modalities and role hierarchies
- Terminating tableaux for graded hybrid logic with global modalities and role hierarchies
- scientific article; zbMATH DE number 1950252
- Termination proofs for logic programs with tabling
Cites work
- A description logic with transitive and inverse roles and role hierarchies
- A guide to completeness and complexity for modal logics of knowledge and belief
- A tableau decision procedure for \(\mathcal{SHOIQ}\)
- scientific article; zbMATH DE number 4148058 (Why is no real title available?)
- scientific article; zbMATH DE number 3325547 (Why is no real title available?)
- Hybrid tableaux for the difference modality
- Modal logic
- Modal logic with names
- Semantical Analysis of Modal Logic I Normal Modal Propositional Calculi
- Tableau-based Decision Procedures for Hybrid Logic
- Terminating Tableaux for Hybrid Logic with the Difference Modality and Converse
- Termination for Hybrid Tableaus
- The modal logic of inequality
- The seven virtues of simple type theory
Cited in
(24)- Quantified multimodal logics in simple type theory
- A prover dealing with nominals, binders, transitivity and relation hierarchies
- Blocking and other enhancements for bottom-up model generation methods
- A tableaux calculus for default intuitionistic logic
- 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
- Extended decision procedure for a fragment of HL with binders
- An efficient approach to nominal equalities in hybrid logic tableaux
- A Tableaux Based Decision Procedure for a Broad Class of Hybrid Formulae with Binders
- Verifying the modal logic cube is an easy task (for higher-order automated reasoners)
- Terminating Tableaux for Hybrid Logic with the Difference Modality and Converse
- Completeness in hybrid type theory
- Clausal graph tableaux for hybrid logic with eventualities and difference
- HTab: a terminating tableaux system for hybrid logic
- Terminating Tableau Calculi for Hybrid Logics Extending K
- Hybrid tableaux for the difference modality
- Decision procedures for some strong hybrid logics
- Termination for Hybrid Tableaus
- Terminating Tableaux for Hybrid Logic with Eventualities
- Terminating tableaux for graded hybrid logic with global modalities and role hierarchies
- Terminating tableaux for graded hybrid logic with global modalities and role hierarchies
- Lightweight hybrid tableaux
- Hybrid logic with the difference modality for generalisations of graphs
- Combining and automating classical and non-classical logics in classical higher-order logics
This page was built for publication: Terminating tableau systems for hybrid logic with difference and converse
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1047795)
