Christine Golbreich,
Matthew Horridge,
Ian Horrocks,
Boris Motik, and
Rob Shearer. OBO and OWL: Leveraging Semantic Web Technologies for the Life Sciences. In Karl Aberer, Key-Sun Choi, Natasha Fridman Noy, Dean Allemang, Kyung-Il Lee, Lyndon J. B. Nixon, Jennifer Golbeck, Peter Mika, Diana Maynard, Riichiro Mizoguchi, Guus Schreiber, and Philippe Cudré-Mauroux, editors,
Proc. of the 6th Int. Semantic Web Conference (ISWC 2007), volume 4825 of LNCS, pages 169–182, Busan, Korea, November 11-15 2007. Springer.
@InProceedings{ghhms07obo-and-owl,
author = "Christine Golbreich and Matthew Horridge and Ian Horrocks and Boris Motik and Rob Shearer",
title = "{OBO and OWL: Leveraging Semantic Web Technologies for the Life Sciences}",
booktitle = "Proc. of the 6th Int. Semantic Web Conference (ISWC 2007)",
editor = "Karl Aberer and Key-Sun Choi and Natasha Fridman Noy and Dean Allemang and Kyung-Il Lee and Lyndon J. B. Nixon and Jennifer Golbeck and Peter Mika and Diana Maynard and Riichiro Mizoguchi and Guus Schreiber and Philippe Cudr{\'e}-Mauroux",
address = "Busan, Korea",
month = "November 11-15",
year = "2007",
publisher = "Springer",
series = "LNCS",
volume = "4825",
pages = "169--182",
}
OBO is an ontology language that has often been used for modeling
ontologies in the life sciences. Its definition is relatively
informal, so, in this paper, we provide a clear specification for
OBO syntax and semantics via a mapping to OWL. This mapping also
allows us to apply existing Semantic Web tools and techniques to
OBO. We show that Semantic Web reasoners can be used to efficiently
reason with OBO ontologies. Furthermore, we show that grounding the
OBO language in formal semantics is useful for the ontology
development process: using an OWL reasoner, we detected a likely
modeling error in one OBO ontology.
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,
Ian Horrocks, and
Boris Motik. Exploiting Partial Information in Taxonomy Construction. In Bernardo Guenca Grau,
Ian Horrocks,
Boris Motik, and
Ulrike Sattler, editors,
Proc. of the 22nd Int. Workshop on Description Logics (DL 2009), volume 477 of CEUR Workshop Proceedings, Oxford, UK, July 27–30 2009.
@InProceedings{shm09rewriting,
author = "Rob Shearer and Ian Horrocks and Boris Motik",
title = "{Exploiting Partial Information in Taxonomy Construction}",
booktitle = "Proc. of the 22nd Int. Workshop on Description Logics (DL 2009)",
editor = "Bernardo Guenca Grau and Ian Horrocks and Boris Motik and Ulrike Sattler",
address = "Oxford, UK",
month = "July 27--30",
year = "2009",
series = "CEUR Workshop Proceedings",
volume = "477",
}
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,
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.
@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.