A tableau decision procedure for \(\mathcal{SHOIQ}\)
From MaRDI portal
Publication:2462647
DOI10.1007/s10817-007-9079-9zbMath1132.68734OpenAlexW1978912716WikidataQ56988749 ScholiaQ56988749MaRDI QIDQ2462647
Publication date: 3 December 2007
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-007-9079-9
Related Items
An efficient approach to nominal equalities in hybrid logic tableaux ⋮ The two‐variable fragment with counting and equivalence ⋮ Coalition Description Logic with Individuals ⋮ Expressive probabilistic description logics ⋮ A family of dynamic description logics for representing and reasoning about actions ⋮ Algebraic tableau reasoning for the description logic \(\mathcal{SHOQ}\) ⋮ A short introduction to SHACL for logicians ⋮ Extending Description Logics with Uncertainty Reasoning in Possibilistic Logic ⋮ Query Answering in the Description Logic Horn- $\mathcal{SHIQ}$ ⋮ A resolution-based decision procedure for \({\mathcal{SHOIQ}}\). ⋮ Terminating Tableaux for Hybrid Logic with the Difference Modality and Converse ⋮ Optimizing terminological reasoning for expressive description logics ⋮ Data complexity of query answering in expressive description logics via tableaux ⋮ Algorithms for reasoning in very expressive description logics under infinitely valued Gödel semantics ⋮ Answering regular path queries in expressive description logics via alternating tree-automata ⋮ Terminating Tableaux for Hybrid Logic with Eventualities ⋮ Extending soft sets with description logics ⋮ Probabilistic DL Reasoning with Pinpointing Formulas: A Prolog-based Approach ⋮ Reasoning with rough description logics: An approximate concepts approach ⋮ Reasoning over Vague Concepts ⋮ Extracting Modules from Ontologies: A Logic-Based Approach ⋮ Ontology Integration Using ε-Connections ⋮ Composing Modular Ontologies with Distributed Description Logics ⋮ Package-Based Description Logics ⋮ Plans, actions and dialogues using linear logic ⋮ ExpTime tableaux with global caching for hybrid PDL ⋮ A prover dealing with nominals, binders, transitivity and relation hierarchies ⋮ Blocking and other enhancements for bottom-up model generation methods ⋮ Ontologies and Databases: The DL-Lite Approach ⋮ Query Answering with DBoxes is Hard ⋮ A Tableau Decision Procedure for <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" altimg="si1.gif" overflow="scroll"><mml:mi mathvariant="script">ALC</mml:mi></mml:math> With Monotonic Modal Operators and Constant Domains ⋮ Combining Description Logics, Description Graphs, and Rules ⋮ Terminating tableau systems for hybrid logic with difference and converse ⋮ Hybrid Logics and Ontology Languages ⋮ A goal-directed decision procedure for hybrid PDL ⋮ HermiT: an OWL 2 reasoner ⋮ Extended decision procedure for a fragment of HL with binders ⋮ Reasoning with nominal schemas through absorption
Uses Software
Cites Work
- Propositional dynamic logic of regular programs
- Hybrid languages
- PSPACE Reasoning for Graded Modal Logics
- Optimizing description logic subsumption
- Complexity Results for First-Order Two-Variable Logic with Counting
- An overview of tableau algorithms for description logics
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
