Optimizing Algebraic Tableau Reasoning for SHOQ: First Experimental Results.
Jocelyne Faddoul, Volker Haarslev · 2010
Abstract. 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