Data and Knowledge Group

― Knowledge Representation and Reasoning

HermiT Publications

Updated 2009-08-02

Boris Motik, Bernardo Cuenca Grau, and Ulrike Sattler. Structured Objects in OWL: Representation and Reasoning. In Jinpeng Huai, Robin Chen, Hsiao-Wuen Hon, Yunhao Liu, Wei-Ying Ma, Andrew Tomkins, and Xiaodong Zhang, editors, Proc. of the 17th Int. World Wide Web Conference (WWW 2008), pages 555–564, Beijing, China, April 21–25 2008. ACM Press.
@InProceedings{mgs08structured-objects,
    author = "Boris Motik and Bernardo Cuenca Grau and Ulrike Sattler",
    title = "{Structured Objects in OWL: Representation and Reasoning}",
    booktitle = "Proc. of the 17th Int. World Wide Web Conference (WWW 2008)",
    editor = "Jinpeng Huai and Robin Chen and Hsiao-Wuen Hon and Yunhao Liu and Wei-Ying Ma and Andrew Tomkins and Xiaodong Zhang",
    address = "Beijing, China",
    month = "April 21--25",
    year = "2008",
    publisher = "ACM Press",
    pages = "555--564",
}
Applications of semantic technologies often require the representation of and reasoning with structured objects—that is, objects composed of parts connected in complex ways. Although OWL is a general and powerful language, its class descriptions and axioms cannot be used to describe arbitrarily connected structures. An OWL representation of structured objects can thus be underconstrained, which reduces the inferences that can be drawn and causes performance problems in reasoning. To address these problems, we extend OWL with description graphs, which allow for the description of structured objects in a simple and precise way. To represent conditional aspects of the domain, we also allow for SWRL-like rules over description graphs. Based on an observation about the nature of structured objects, we ensure decidability of our formalism. We also present a hypertableau-based decision procedure, which we implemented in the HermiT reasoner. To evaluate its performance, we have extracted description graphs from the GALEN and FMA ontologies, classified them successfully, and even detected a modeling error in GALEN.
Boris Motik, Rob Shearer, and Ian Horrocks. Optimized Reasoning in Description Logics using Hypertableaux. In Frank Pfenning, editor, Proc. of the 21st Conference on Automated Deduction (CADE-21), volume 4603 of LNAI, pages 67–83, Bremen, Germany, July 17–20 2007. Springer.
@InProceedings{msh07optimizing,
    author = "Boris Motik and Rob Shearer and Ian Horrocks",
    title = "{Optimized Reasoning in Description Logics using Hypertableaux}",
    booktitle = "Proc. of the 21st Conference on Automated Deduction (CADE-21)",
    editor = "Frank Pfenning",
    address = "Bremen, Germany",
    month = "July 17--20",
    year = "2007",
    publisher = "Springer",
    series = "LNAI",
    volume = "4603",
    pages = "67--83",
}
We present a novel reasoning calculus for Description Logics (DLs)—knowledge representation formalisms with applications in areas such as the Semantic Web. In order to reduce the nondeterminism due to general inclusion axioms, we base our calculus on hypertableau and hyperresolution calculi, which we extend with a blocking condition to ensure termination. To prevent the calculus from generating large models, we introduce "anywhere" pairwise blocking. Our preliminary implementation shows significant performance improvements on several well-known ontologies. To the best of our knowledge, our reasoner is currently the only one that can classify the original version of the GALEN terminology.
Rob Shearer, Boris Motik, and Ian Horrocks. HermiT: A Highly-Efficient OWL Reasoner. In Alan Ruttenberg, Ulrile Sattler, and Cathy Dolbear, editors, Proc. of the 5th Int. Workshop on OWL: Experiences and Directions (OWLED 2008 EU), Karlsruhe, Germany, October 26–27 2008.
@InProceedings{smh08HermiT,
    author = "Rob Shearer and Boris Motik and Ian Horrocks",
    title = "{HermiT: A Highly-Efficient OWL Reasoner}",
    booktitle = "Proc. of the 5th Int. Workshop on OWL: Experiences and Directions (OWLED 2008 EU)",
    editor = "Alan Ruttenberg and Ulrile Sattler and Cathy Dolbear",
    address = "Karlsruhe, Germany",
    month = "October 26--27",
    year = "2008",
}
%!TEX root = paper.tex HermiT is a new OWL reasoner based on a novel "hypertableau'' calculus. The new calculus addresses performance problems due to nondeterminism and model size—the primary sources of complexity in state-of-the-art OWL reasoners. The latter is particularly important in practice, and it is achieved in HermiT with an improved blocking strategy and and an optimization that tries to reuse existing individuals rather than generating new ones. HermiT also incorporates a number of other novel optimizations, such as a more efficient approach to handling nominals, and various techniques for optimizing ontology classification. Our tests show that HermiT is usually much faster than other reasoners when classifying complex ontologies, and it is already able to classify a number of ontologies which no other reasoner has been able to handle.
Boris Motik, Rob Shearer, and Ian Horrocks. Optimizing the Nominal Introduction Rule in (Hyper)Tableau Calculi. In Franz Baader, Carsten Lutz, and Boris Motik, editors, Proc. of the 21st Int. Workshop on Description Logics (DL 2008), volume 353 of CEUR Workshop Proceedings, Dresden, Germany, May 13–16 2008.
@InProceedings{msh08rewriting,
    author = "Boris Motik and Rob Shearer and Ian Horrocks",
    title = "{Optimizing the Nominal Introduction Rule in (Hyper)Tableau Calculi}",
    booktitle = "Proc. of the 21st Int. Workshop on Description Logics (DL 2008)",
    editor = "Franz Baader and Carsten Lutz and Boris Motik",
    address = "Dresden, Germany",
    month = "May 13--16",
    year = "2008",
    series = "CEUR Workshop Proceedings",
    volume = "353",
}
%!TEX root = paper.tex Interactions between nominals, inverse roles, and number restrictions provide challenges to description logic reasoners, as they can make models of a knowledge base non-forest-like. The solution to this problem used by the standard tableau calculus can incur a high degree of nondeterminism and can lead to the generation of unnecessarily large models. We present a more efficient approach to handling this combination of constructs. We use this approach to extend our hypertableau calculus to SHOIQ. This approach, however, is equally applicable to traditional tableau calculi.
Boris Motik, Bernardo Cuenca Grau, and Ulrike Sattler. The Representation of Structured Objects in DLs using Description Graphs. In Franz Baader, Carsten Lutz, and Boris Motik, editors, Proc. of the 21st Int. Workshop on Description Logics (DL 2008), volume 353 of CEUR Workshop Proceedings, Dresden, Germany, May 13–16 2008.
@InProceedings{mgs08description-graphs,
    author = "Boris Motik and Bernardo Cuenca Grau and Ulrike Sattler",
    title = "{The Representation of Structured Objects in DLs using Description Graphs}",
    booktitle = "Proc. of the 21st Int. Workshop on Description Logics (DL 2008)",
    editor = "Franz Baader and Carsten Lutz and Boris Motik",
    address = "Dresden, Germany",
    month = "May 13--16",
    year = "2008",
    series = "CEUR Workshop Proceedings",
    volume = "353",
}
Boris Motik, Rob Shearer, and Ian Horrocks. A Hypertableau Calculus for SHIQ. In Diego Calvanese, Enriso Franconi, Volker Haarslev, Domenico Lembo, Boris Motik, Sergio Tessaris, and Anny-Yasmin Turhan, editors, Proc. of the 20th Int. Workshop on Description Logics (DL 2007), pages 419–426, Brixen/Bressanone, Italy, June 8–10 2007. Bozen/Bolzano University Press.
@InProceedings{msh07hypertableau,
    author = "Boris Motik and Rob Shearer and Ian Horrocks",
    title = "{A Hypertableau Calculus for SHIQ}",
    booktitle = "Proc. of the 20th Int. Workshop on Description Logics (DL 2007)",
    editor = "Diego Calvanese and Enriso Franconi and Volker Haarslev and Domenico Lembo and Boris Motik and Sergio Tessaris and Anny-Yasmin Turhan",
    address = "Brixen/Bressanone, Italy",
    month = "June 8--10",
    year = "2007",
    publisher = "Bozen/Bolzano University Press",
    pages = "419--426",
}
We present a novel reasoning calculus for the Description Logic SHIQ. In order to reduce the nondeterminism due to general inclusion axioms, we base our calculus on hypertableau and hyperresolution calculi, which we extend with a blocking condition to ensure termination. To prevent the calculus from generating large models, we introduce "anywhere'' pairwise blocking. Our preliminary implementation shows significant performance improvements on several well-known ontologies. To the best of our knowledge, our reasoner is currently the only one that can classify the original version of the GALEN terminology.
Boris Motik, Bernardo Cuenca Grau, and Ulrike Sattler. Structured Objects in OWL: Representation and Reasoning. Technical Report, University of Oxford, UK, 2007.
@TechReport{mgs07structured-objects-report,
    author = "Boris Motik and Bernardo Cuenca Grau and Ulrike Sattler",
    title = "{Structured Objects in OWL: Representation and Reasoning}",
    institution = "University of Oxford",
    address = "UK",
    year = "2007",
}
Applications of semantic technologies often require the representation of and reasoning with structured objects—that is, objects composed of parts connected in complex ways. Although OWL is a general and powerful language, its class descriptions and axioms cannot be used to describe arbitrarily connected structures. An OWL representation of structured objects can thus be underconstrained, which reduces the inferences that can be drawn and causes performance problems in reasoning. To address these problems, we extend OWL with description graphs, which allow for the description of structured objects in a simple and precise way. To represent conditional aspects of the domain, we also allow for SWRL-like rules over description graphs. Based on an observation about the nature of structured objects, we ensure decidability of our formalism. We also present a hypertableau-based decision procedure, which we implemented in the HermiT reasoner. To evaluate its performance, we have extracted description graphs from the GALEN and FMA ontologies, classified them successfully, and even detected a modeling error in GALEN.
Boris Motik, Rob Shearer, and Ian Horrocks. Hypertableau Reasoning for Description Logics. 2009. Submitted to a journal.
@Misc{msh09hypertableau-journal,
    author = "Boris Motik and Rob Shearer and Ian Horrocks",
    title = "{Hypertableau Reasoning for Description Logics}",
    year = "2009",
    note = "Submitted to a journal",
}
%!TEX root = paper.tex We present a novel reasoning calculus for the description logic SHOIQplus—a knowledge representation formalism with applications in areas such as the Semantic Web. 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 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 preliminary implementation shows significant performance improvements over state-of-the-art reasoners on several well-known ontologies.

Project Summary

Duration

August 2008 to May 2011

Researchers

Ian Horrocks, Boris Motik, Birte Glimm, and Rob Shearer

Sponsors

UK Engineering and Physical Sciences Research Council

Links

The HermiT OWL Reasoner