Hypertableau Reasoning for Description Logics
By Boris Motik, Rob Shearer, Ian Horrocks. Journal of Artificial Intelligence Research, 2009
465 citations recorded by the source corpus.
We present a novel reasoning calculus for the description logic SHOIQ+--a knowledge representation formalism with applications in areas such as the SemanticWeb. Unnecessary nondeterminism and the construction of large models are two primary sources of inefficiency in the tableau-based reasoning calculi used in state-of-the-art reasoners. In order to reduce nondeterminism, we base our calculus on hypertableau and hyperresolution calculi, which we extend with a blocking condition to ensure termination. In order to reduce the size of the constructed models, we introduce anywhere pairwise blocking. We also present an improved nominal introduction rule that ensures termination in the presence of nominals, inverse roles, and number restrictions--a combination of DL constructs that has proven notoriously difficult to handle. Our implementation shows significant performance improvements over state-of-the-art reasoners on several well-known ontologies.
Subfields: Artificial Intelligence, Molecular Biology
View Paper: https://www.semanticscholar.org/paper/d761b538ce7ed881b071fff5f0c3c9a7eae72473
How researchers see this paper
The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.
In Artificial Intelligence
- Pavel Shvaiko
- Jérôme Euzenat
- Bernardo Cuenca Grau
- Boris Motik
- Ian Horrocks
- Birte Glimm
- Ernesto Jiménez-Ruiz
- Giorgos Stoilos
In Molecular Biology
- Jérôme Euzenat
- Pavel Shvaiko
- Isabelle Bloch
- Jamal Atif
- Céline Hudelot
- Bernardo Cuenca Grau
- Ernesto Jiménez-Ruiz
- Ian Horrocks
Citations in the corpus
- HermiT: An OWL 2 Reasoner (2014, methodology): “C , and it also implements the required pruning operation [30].”
- Knowledge Graphs (2020, unknown): “, [363]).”
- Results of the Ontology Alignment Evaluation Initiative 2014 (2014, methodology): “We have used the OWL 2 reasoner HermiT [25] to compute the number of unsatisfiable classes.”
- Explanatory Reasoning for Image Understanding Using Formal Concept Analysis and Description Logics (2014, methodology): “, Hermit system [50] based on semantic-tableaux reasoning can be used to generate such counter-examples in the FCA-based processes described in [28] and [47].”
- LogMap: Logic-Based and Scalable Ontology Matching (2011, methodology): “LogMap bundles HermiT [17] and Condor [22], which are highly optimised for classification.”