Optimizing Tableau Reasoning: a Prolog-based Framework

Tracking #: 2415-3629

This paper is currently under review
Riccardo Zese
Giuseppe Cota

Responsible editor: 
Bernardo Cuenca Grau

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. 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 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 the 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 http://trill-sw.eu/.
Full PDF Version: 
Under Review