Probabilistic DL Reasoning with Pinpointing Formulas: A Prolog-based
  Approach
  When modeling real world domains we have to deal with information that is
incomplete or that comes from sources with different trust levels. This
motivates the need for managing uncertainty in the Semantic Web. To this
purpose, we introduced a probabilistic semantics, named DISPONTE, in order to
combine description logics with probability theory. The probability of a query
can be then computed from the set of its explanations by building a Binary
Decision Diagram (BDD). The set of explanations can be found using the tableau
algorithm, which has to handle non-determinism. Prolog, with its efficient
handling of non-determinism, is suitable for implementing the tableau
algorithm. TRILL and TRILLP are systems offering a Prolog implementation of the
tableau algorithm. TRILLP builds a pinpointing formula, that compactly
represents the set of explanations and can be directly translated into a BDD.
Both reasoners were shown to outperform state-of-the-art DL reasoners. In this
paper, we present an improvement of TRILLP, named TORNADO, in which the BDD is
directly built during the construction of the tableau, further speeding up the
overall inference process. An experimental comparison shows the effectiveness
of TORNADO. All systems can be tried online in the TRILL on SWISH web
application at http://trill.ml.unife.it/.
