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.
@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.
@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.