A Tableaux Decision Procedure for SHOIQ

By Ian Horrocks, U. Sattler. International Joint Conference on Artificial Intelligence, 2005

458 citations recorded by the source corpus.

View Paper: https://www.semanticscholar.org/paper/ced0910c91ea679ec385ef0969fdca63ca46bf2e

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

Citations in the corpus

Pellet: A practical OWL-DL reasoner (2007, methodology): “This strategy is based on the recently developed decision procedure for SHOIQ 3 [13].”
Ontologies and the semantic web (2006, methodology): “OWL is based on a very expressive DL called SHOIN (D)—a sort of acronym derived from the various features of the language [11].”
The Even More Irresistible SROIQ (2006, background): “details and refer the reader to Horrocks & Sattler (2005) .”
Conjunctive Query Answering for the Description Logic SHIQ (2007, methodology): “In the presence of transitive roles, a TBoxT can be internalised using an “approximation” of a universal role u [ 8 , 11].”
OWL 2: The next step for OWL (2008, background): “OWL 1 DL Semantics The description logic SHOIN (D) has been extensively investigated in the literature, and its expressivity and computational properties are wellknown [36,19].”
FaCT++ Description Logic Reasoner: System Description (2006, methodology): “Many systems now implement the SHIQ or SHOIQ DLs, tableaux algorithms for which were presented in [7, 6]; these logics are very expressive, and correspond closely to the OWL ontology language.”
Modular Reuse of Ontologies: Theory and Practice (2008, background): “In this case, importing the module will have the Cuenca Grau, Horrocks, Kazakov, & Sattler DLs Constructors Axioms [ Ax ] Here r ∈ AR, A ∈ AC, a, b ∈ Ind, R (i) ∈ Rol, C (i) ∈ Con, n ≥ 1 and S ∈ Rol is a simple role (see (Horrocks & Sattler, 2005)).”
Managing uncertainty and vagueness in description logics for the Semantic Web (2008, background): “More specifically, ontology entailment in OWL Lite and OWL DL reduces to knowledge base (un)satisfiability in the expressive description logics SHIF(D) and SHOIN(D) [55,57], respectively.”
HermiT: An OWL 2 Reasoner (2014, methodology): “Prior to HermiT, this requirement was satisfied using ancestor blocking [17]: an individual s ′ could directly block an individual s only if, in addition to the usual requirements on single or pairwise blocking, it is the case that s ′ is an ancestor of s.”