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