Optimizing Tableau Reasoning: a Prolog-based Framework

Tracking #: 2202-3415

This paper is currently under review
Riccardo Zese
Giuseppe Cota

Responsible editor: 
Thomas Lukasiewicz

Submission type: 
Full Paper
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. Each one of them uses different approaches for probabilistic inference and handles different DLs flavours. Our previous work showed that they can achieve sometimes 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. In the first one, the reasoners build the hierarchy of the concepts contained in a knowledge base in order to quickly find connections among them during the expansion of the tableau. The second one modifies the order of application of tableau rules in order to reduce the number of operations. Experimental results show the effectiveness of the introduced optimizations. All systems can be tried online in the TRILL on SWISH web application at \url{http://trill-sw.eu/}.
Full PDF Version: 
Under Review