Sciweavers

DLOG
2010

Optimizing Algebraic Tableau Reasoning for SHOQ: First Experimental Results

13 years 1 months ago
Optimizing Algebraic Tableau Reasoning for SHOQ: First Experimental Results
In this paper we outline an algebraic tableau algorithm for the DL SHOQ, which supports more informed reasoning due to the use of semantic partitioning and integer programming. We introduce novel and adapt known optimization techniques and show their effectiveness on the basis of a prototype reasoner implementing the optimization techniques for the algebraic approach. Our first set of benchmarks clearly indicates the effectiveness of our approach and a comparison with the DL reasoners Pellet and HermiT demonstrates a runtime improvement of several orders of magnitude. 1 Motivation Nominals play an important role in Description Logics (DLs) as they allow one to express the notion of identity and enumeration; nominals must be interpreted as singleton sets. An example for the use of nominals in SHOQ would be Eye Color Green Blue Brown Black Hazel where each color is represented as a nominal. The cardinality of Eye Color is restricted to have at most 5 instances, i.e., the abovemention...
Jocelyne Faddoul, Volker Haarslev
Added 10 Feb 2011
Updated 10 Feb 2011
Type Journal
Year 2010
Where DLOG
Authors Jocelyne Faddoul, Volker Haarslev
Comments (0)