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

• Type: Journal
• Year: 2010
• Where: DLOG
• Authors: Jocelyne Faddoul, Volker Haarslev
• Keywords: Automated Reasoning, Cardinality, DLOG 2010, Eye Color, Optimization Techniques