An Ordered Theory Resolution Calculus for Hybrid Reasoning in …

Short Description
theory resolution calculus (Baumgartner 1992) that permits ….. The inference rules of the ordered narrow theory resolution calculus. …

Website: www.cs.toronto.edu | Filesize: 168kb

Content
An Ordered Theory Resolution Calculus for Hybrid Reasoning in First-order
Extensions of Description Logic
Scott Sanner and Sheila McIlraith
University of Toronto
Department of Computer Science
Toronto, ON, M5S 3H5, CANADA
fssanner, sheilag @cs.toronto.edu
Abstract
Systems for hybrid reasoning with first-order logic
(FOL) extensions of description logic (DL) date back
at least 20 years and are enjoying a renewed interest
in the context of recent FOL extensions of OWL DL
for the Semantic Web. However, current systems for
reasoning with such languages can only handle subsets
of FOL or they do not fully exploit recent advances in
both FOL theorem proving and DL inference. In response,
we present an ordered theory resolution calculus
for hybrid reasoning in unrestricted FOL extensions
of the DL SHI. This calculus permits near-seamless
integration of highly optimized FOL theorem provers
and DL reasoners while minimizing redundant reasoning
and maintaining soundness and refutational completeness.
Empirical results demonstrate the potential of
this approach in comparison to the state-of-the-art FOL
theorem provers Vampire, Otter, and SPASS.
1 Introduction
It is widely acknowledged that knowledge representation
languages based on (decidable) description logics…