Consequence-Driven Reasoning for Horn SHIQ Ontologies

international joint conference on artificial intelligence, 2009, Pages 2040-2045.

Cited by: 224|Bibtex|Views133|Links
EI
Keywords:
common fragmentnovel reasoning procedurehorn fragmentconsequence-driven reasoningshiq ontologyMore(9+)
Weibo:
Ontology languages based on Description Logics, such as OWL,1 are becoming increasingly popular among ontology developers thanks to the availability of ontology reasoners, which provide automated support for visualization, debugging, and querying of ontologies

Abstract:

We present a novel reasoning procedure for Horn SHIQ ontologies—SHIQ ontologies that can be translated to the Horn fragment of first-order logic. In contrast to traditional reasoning procedures for ontologies, our procedure does not build models or model representations, but works by deriving new consequent axioms. The procedure is closel...More

Code:

Data:

Introduction
  • Ontologies are formal vocabularies of terms describing specific subjects like chemical elements, genes, or animal species.
  • It can be seen that every ELH ontology is a Horn SHIQ ontology since it cannot contain concepts of the form ¬C, C D, ∀R.C, nR.C, or mR.C. In [Baader et al, 2005], a polynomial time classification procedure has been presented for the description logic EL++, which extends EL+ with the bottom concept ⊥, nominals, and “safe” concrete domains.
Highlights
  • Ontologies are formal vocabularies of terms describing specific subjects like chemical elements, genes, or animal species
  • Ontology languages based on Description Logics (DLs) [Baader et al, 2007], such as OWL,1 are becoming increasingly popular among ontology developers thanks to the availability of ontology reasoners, which provide automated support for visualization, debugging, and querying of ontologies
  • In this paper we describe a reasoning procedure, which utilizes the core reasoning technique of EL++, but works for a larger class of socalled Horn SHIQ ontologies
  • According to the definition in Section 2.2, Horn SHIQ ontologies allow for the usage of inverse roles and positive occurrences of universal restrictions
  • Lemma 2 Every Horn SHIQ ontology O can be transformed into an ontology O containing only axioms of the forms: (n1) Ai C, (n2) R1 R2, and (n3) Tra(R), where C is a simple concept
  • To evaluate the performance of our procedure, we implemented a prototype reasoner CB4 using a simplified version of the rules in Table 3 for Horn SHIF ontologies, which are sufficient for Galen
Results
  • According to the definition in Section 2.2, Horn SHIQ ontologies allow for the usage of inverse roles and positive occurrences of universal restrictions.
  • In Section 4, the authors generalize inferences (2)–(5) and present a sound and complete system of inference rules for Horn SHIQ ontologies, which derive only consequence axioms of the form
  • Lemma 2 Every Horn SHIQ ontology O can be transformed into an ontology O containing only axioms of the forms: (n1) Ai C, (n2) R1 R2, and (n3) Tra(R), where C is a simple concept.
  • By applying structural transformation to O, the authors obtain an ontology O containing only concept inclusions of the form A1 A2, A st(C+), and st(C−) A, where C+ occurs positively in O and C− occurs negatively in O.
  • The authors' procedure for Horn SHIQ ontologies works by saturating the input axioms under the rules in Table 3.
  • The authors demonstrate that the procedure is sound and complete for classification, that is, it derives all subsumptions between atomic concepts in the input ontology.
  • Theorem 4, in conjunction with Lemmas 2 and 3, implies that the procedure based on the rules in Table 3 can be used, in particular, for computing all subsumptions A B between atomic concepts implied by the input ontology.
  • Since deciding concept subsumptions in Horn SHIQ ontologies is ExpTime-complete, this implies that the procedure is computationally optimal.
Conclusion
  • The main goal for the consequence-based procedure for Horn SHIQ ontologies, was to reason efficiently with mediumsized ontologies such as Galen.3 Galen turned out to be very difficult for model-building reasoners since it contains a large number of existential dependencies between classes of the form A ∃R.B. These dependencies are used, e.g., for expressing partonomy relations between anatomical units, for example: BasilarArtery ∃isBranchOf.VertebralArtery.
  • To evaluate the performance of the procedure, the authors implemented a prototype reasoner CB4 using a simplified version of the rules in Table 3 for Horn SHIF ontologies, which are sufficient for Galen.
Summary
  • Ontologies are formal vocabularies of terms describing specific subjects like chemical elements, genes, or animal species.
  • It can be seen that every ELH ontology is a Horn SHIQ ontology since it cannot contain concepts of the form ¬C, C D, ∀R.C, nR.C, or mR.C. In [Baader et al, 2005], a polynomial time classification procedure has been presented for the description logic EL++, which extends EL+ with the bottom concept ⊥, nominals, and “safe” concrete domains.
  • According to the definition in Section 2.2, Horn SHIQ ontologies allow for the usage of inverse roles and positive occurrences of universal restrictions.
  • In Section 4, the authors generalize inferences (2)–(5) and present a sound and complete system of inference rules for Horn SHIQ ontologies, which derive only consequence axioms of the form
  • Lemma 2 Every Horn SHIQ ontology O can be transformed into an ontology O containing only axioms of the forms: (n1) Ai C, (n2) R1 R2, and (n3) Tra(R), where C is a simple concept.
  • By applying structural transformation to O, the authors obtain an ontology O containing only concept inclusions of the form A1 A2, A st(C+), and st(C−) A, where C+ occurs positively in O and C− occurs negatively in O.
  • The authors' procedure for Horn SHIQ ontologies works by saturating the input axioms under the rules in Table 3.
  • The authors demonstrate that the procedure is sound and complete for classification, that is, it derives all subsumptions between atomic concepts in the input ontology.
  • Theorem 4, in conjunction with Lemmas 2 and 3, implies that the procedure based on the rules in Table 3 can be used, in particular, for computing all subsumptions A B between atomic concepts implied by the input ontology.
  • Since deciding concept subsumptions in Horn SHIQ ontologies is ExpTime-complete, this implies that the procedure is computationally optimal.
  • The main goal for the consequence-based procedure for Horn SHIQ ontologies, was to reason efficiently with mediumsized ontologies such as Galen.3 Galen turned out to be very difficult for model-building reasoners since it contains a large number of existential dependencies between classes of the form A ∃R.B. These dependencies are used, e.g., for expressing partonomy relations between anatomical units, for example: BasilarArtery ∃isBranchOf.VertebralArtery.
  • To evaluate the performance of the procedure, the authors implemented a prototype reasoner CB4 using a simplified version of the rules in Table 3 for Horn SHIF ontologies, which are sufficient for Galen.
Tables
  • Table1: The syntax and semantics of SHIQ terminologies the constructors given in the upper part of Table 1, where A ∈ NC, C, D are concepts, R, S roles, and n, m positive integers. A terminology or ontology is a set O of axioms specified in the lower part of Table 1. A role R is transitive (in O) if Tra(R) ∈ O or Tra(R−) ∈ O. Given an ontology O, let R1 O R2 be the smallest transitive reflexive relation between roles such that R1 R2 ∈ O implies R1 O R2 and R1− O R2−. It is required that for every concept of the form nS.C and mS.C in O the role S is simple, that is, R O S holds for no transitive role R
  • Table2: The Completion Rules for ELH
  • Table3: Saturation Rules for Horn SHIQ Ontologies
  • Table4: A comparison of classification times (in seconds): “—” means that the reasoner failed to return the result; “n/a” means that the test could not be performed
Download tables as Excel
Reference
  • [Baader et al., 2005] Franz Baader, Sebastian Brandt, and Carsten Lutz. Pushing the EL envelope. In IJCAI, pages 364–369. Professional Book Center, 2005.
    Google ScholarLocate open access versionFindings
  • [Baader et al., 2007] Franz Baader, Diego Calvanese, Deborah L. McGuinness, Daniele Nardi, and Peter F. PatelSchneider, editors. The Description Logic Handbook. Cambridge University Press, 2007. 2nd edition.
    Google ScholarFindings
  • [Baader et al., 2008] Franz Baader, Sebastian Brandt, and Carsten Lutz. Pushing the EL envelope further. In Proc. of OWLED 2008, 2008.
    Google ScholarLocate open access versionFindings
  • [Horrocks et al., 2000] Ian Horrocks, Ulrike Sattler, and Stephan Tobies. Practical reasoning for very expressive description logics. Logic Journal of the IGPL, 8(3), 2000.
    Google ScholarLocate open access versionFindings
  • [Hustadt et al., 2007] Ullrich Hustadt, Boris Motik, and Ulrike Sattler. Reasoning in description logics by a reduction to disjunctive datalog. J. Autom. Reasoning, 39(3):351–384, 2007.
    Google ScholarLocate open access versionFindings
  • [Motik et al., 2007] Boris Motik, Rob Shearer, and Ian Horrocks. Optimized reasoning in description logics using hypertableaux. In CADE, volume 4603 of Lecture Notes in Computer Science, pages 67–83.
    Google ScholarLocate open access versionFindings
Your rating :
0

 

Best Paper
Best Paper of IJCAI, 2009
Tags
Comments