Optimizing a tableau reasoner and its implementation in Prolog

One of the foremost reasoning services for knowledge bases is finding all the justifications for a query. This is useful for debugging purpose and for coping with uncertainty. Among Description Logics (DLs) reasoners, the tableau algorithm is one of the most used. However, in order to collect the justifications, the reasoners must manage the non-determinism of the tableau method. For these reasons, a Prolog implementation can facilitate the management of such non-determinism. The TRILL framework contains three probabilistic reasoners written in Prolog: TRILL, TRILLP and TORNADO. Since they are all part of the same framework, the choice about which to use can be done easily via the framework settings. Each one of them uses different approaches for probabilistic inference and handles different DLs flavors. Our previous work showed that they can sometimes achieve better results than state-of-the-art (non-)probabilistic reasoners. In this paper we present two optimizations that improve the performances of the TRILL reasoners. The first one consists into identifying the fragment of the KB that allows to perform inference without losing the completeness. The second one modifies which tableau rule to apply and their order of application, in order to reduce the number of operations. Experimental results show the effectiveness of the introduced optimizations.