Information Systems Group

― Knowledge Representation and Reasoning

Hermit OWL Reasoner

The New Kid on the OWL Block

Publications

Birte Glimm, Ian Horrocks, Boris Motik, and Giorgos Stoilos . Optimising Ontology Classification. In Peter F. Patel-Schneider, Yue Pan, Pascal Hitzler, Peter Mika, Lei Zhang, Jeff Z. Pan, Ian Horrocks, and Birte Glimm, editors, Proc. of the 9th Int. Semantic Web Conf. (ISWC 2010), volume 6496 of LNCS, pages 225--240, Shanghai, China, November 7-11 2010. Springer.
@InProceedings{ghms10classification,
    author = "Optimising Ontology Classification",
    title = "{Birte Glimm and Ian Horrocks and Boris Motik and Giorgos Stoilos}",
    booktitle = "Proc. of the 9th Int. Semantic Web Conf. (ISWC 2010)",
    editor = "Peter F. Patel-Schneider and Yue Pan and Pascal Hitzler and Peter Mika and Lei Zhang and Jeff Z. Pan and Ian Horrocks and Birte Glimm",
    address = "Shanghai, China",
    month = "November 7--11",
    year = "2010",
    publisher = "Springer",
    series = "LNCS",
    volume = "6496",
    pages = "225--240",
}
Ontology classification-the computation of subsumption hierarchies for classes and properties-is one of the most important tasks for OWL reasoners. Based on the algorithm by Shearer and Horrocks, we present a new classification procedure that addresses several open issues of the original algorithm, and that uses several novel optimisations in order to achieve superior performance. We also consider the classification of (object and data) properties. We show that algorithms commonly used to implement that task are incomplete even for relatively weak ontology languages. Furthermore, we show how to reduce the property classification problem into a standard (class) classification problem, which allows reasoners to classify properties using our optimised procedure. We have implemented our algorithms in the OWL HermiT reasoner, and we present the results of a performance evaluation.

Birte Glimm, Ian Horrocks, and Boris Motik. Optimized Description Logic Reasoning via Core Blocking. In Jürgen Giesl and Reiner Hähnle, editors, Proc. of the 5th Int. Joint Conf. on Automated Reasoning (IJCAR 2010), volume 6173 of LNCS, pages 457-471, Edinburgh, UK, July 16-19 2010. Springer.
@InProceedings{ghm10core-blocking,
    author = "Birte Glimm and Ian Horrocks and Boris Motik",
    title = "{Optimized Description Logic Reasoning via Core Blocking}",
    booktitle = "Proc. of the 5th Int. Joint Conf. on Automated Reasoning (IJCAR 2010)",
    editor = "J{\"u}rgen Giesl and Reiner H{\"a}hnle",
    address = "Edinburgh, UK",
    month = "July 16--19",
    year = "2010",
    publisher = "Springer",
    series = "LNCS",
    volume = "6173",
    pages = "457--471",
}
State of the art reasoners for expressive description logics, such as those that underpin the OWL ontology language, are typically based on highly optimized implementations of (hyper)tableau algorithms. Despite numerous optimizations, certain ontologies encountered in practice still pose significant challenges to such reasoners, mainly because of the size of the model abstractions that they construct. To address this problem, we propose a new blocking technique that tries to identify and halt redundant construction at a much earlier stage than standard blocking techniques. An evaluation of a prototypical implementation in the HermiT reasoner shows that our technique can dramatically reduce the size of constructed model abstractions and reduce reasoning time.

Boris Motik, Rob Shearer, and Ian Horrocks. Hypertableau Reasoning for Description Logics. Journal of Artificial Intelligence Research, 36:165-228, 2009.
@Article{msh09hypertableau,
    author = "Boris Motik and Rob Shearer and Ian Horrocks",
    title = "{Hypertableau Reasoning for Description Logics}",
    journal = "Journal of Artificial Intelligence Research",
    year = "2009",
    volume = "36",
    pages = "165--228",
}
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 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.

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.

Boris Motik, Rob Shearer, and Ian Horrocks. Optimizing the Nominal Introduction Rule in (Hyper)Tableau Calculi. In Proc. of the 21st Int. Workshop on Description Logics (DL 2008), Dresden, Germany, May 13-16 2008. To appear.
@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)",
    xeditor = "Franz Baader and Carsten Lutz and Boris Motik",
    address = "Dresden, Germany",
    month = "May 13--16",
    year = "2008",
    xpages = "xx--xx",
    note = "To appear",
}
%!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, 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, 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.