Logic Programming Techniques for Reasoning with Probabilistic Ontologies Riccardo Zese, Elena Bellodi, Evelina Lamma Fabrizio Riguzzi Dipartimento di Ingegneria Dipartimento di Matematica e Informatica University of Ferrara University of Ferrara Via Saragat 1, I-44122, Ferrara, Italy Via Saragat 1, I-44122, Ferrara, Italy [riccardo.zese,elena.bellodi,evelina.lamma]@unife.it fabrizio.riguzzi@unife.it Abstract exploits some non-deterministic expansion rules. This re- quires the developers to implement a search strategy in an The increasing popularity of the Semantic Web drove to a widespread adoption of Description Logics (DLs) for mod- or-branching search space. Moreover, if we want to com- eling real world domains. To help the diffusion of DLs, a pute the probability of a query, the algorithm has to compute large number of reasoning algorithms have been developed. all the explanations for the query, thus it has to explore all Usually these algorithms are implemented in procedural lan- the non-deterministic choices taken during the execution. guages such as Java or C++. Most of the reasoners exploit the In this paper, we present the systems TRILL for “Tableau tableau algorithm which has to manage non-determinism, a Reasoner for descrIption Logics in proLog” and TRILLP feature that is not easy to handle using such languages. Rea- for “TRILL powered by Pinpointing formulas”. They are soning on real world domains also requires the capability of tableau reasoners for the SHOIN DL and for the ALC managing probabilistic and uncertain information. We thus DL respectively, both implemented in Prolog. Prolog search present TRILL, for “Tableau Reasoner for descrIption Log- ics in proLog”, that implements a tableau algorithm and is strategy is exploited for taking into account the non- able to return explanations for queries and their correspond- determinism of the tableau rules. They use the Thea2 li- ing probability, and TRILLP , for “TRILL powered by Pin- brary (Vassiliadis, Wielemaker, and Mungall 2009) for pars- pointing formulas”, which is able to compute a Boolean for- ing OWL in its various dialects. Thea2 translates OWL files mula representing the set of explanations for a query. This into a Prolog representation in which each axiom is mapped approach can speed up the process of computing the proba- into a fact. TRILL and TRILLP can check the consistency of bility. Prolog non-determinism allows us to easily handle the a concept and the entailment of an axiom from an ontology, tableau’s non-deterministic expansion rules. and can compute the probability of the entailment follow- ing DISPONTE (Riguzzi et al. 2012), a semantics for prob- Introduction abilistic ontologies. The availability of a Prolog implementa- The Semantic Web aims at making information regarding tion of a DL reasoner will also facilitate the development of real world domains available in a form that is understand- probabilistic reasoners that can integrate probabilistic logic able by machines (Hitzler, Krötzsch, and Rudolph 2009). programming with probabilistic DLs. In probabilistic logic The World Wide Web Consortium is working for realizing programming one of the most widespread approaches is the this vision by supporting the development of the Web On- Distribution Semantics (Sato 1995), on which DISPONTE is tology Language (OWL), a family of knowledge representa- based. Since our systems follow DISPONTE, they are easily tion formalisms for defining ontologies. OWL is based on extensible to take into account this integration. Description Logics (DLs), a set of languages that are re- strictions of first order logic (FOL) with decidability and, Description Logics in some cases, low complexity. For example, the OWL DL DLs are knowledge representation formalisms that are at the sublanguage is based on the expressive SHOIN (D) DL basis of the Semantic Web (Baader et al. 2003; Baader, Hor- while OWL 2 corresponds to the SROIQ(D) DL (Hitzler, rocks, and Sattler 2008) and are used for modeling ontolo- Krötzsch, and Rudolph 2009). Moreover, uncertain informa- gies. They possess nice computational properties such as de- tion is intrinsic to real world domains, thus the combination cidability and/or low complexity. of probability and logic theories becomes of foremost im- Usually, DLs’ syntax is based on concepts and roles portance. which correspond respectively to sets of individuals and sets In order to fully support the development of the Seman- of pairs of individuals of the domain. We first briefly de- tic Web, efficient DL reasoners, such us Pellet, RacerPro, scribe ALC and then SHOIN (D). FaCT++ and HermiT, are able to extract implicit informa- Let C, R and I be sets of atomic concepts, atomic roles tion from the modeled ontologies. Despite the large number and individuals, respectively. Concepts are defined by induc- of available reasoners, only few of them are able to man- tion as follows. Each C ∈ C is a concept, ⊥ and > are age probabilistic information as well. One of the most com- concepts. If C, C1 and C2 are concepts and R ∈ R, then mon approaches for reasoning is the tableau algorithm that (C1 u C2 ), (C1 t C2 ) and ¬C are concepts, as well as ∃R.C and ∀R.C. A TBox T is a finite set of concept inclusion ax- Example 1 The following KB is inspired by the ontology ioms C v D, where C and D are concepts. We use C ≡ D people+pets (Patel-Schneider, Horrocks, and Bechhofer to abbreviate the conjunction of C v D and D v C. An 2003): ABox A is a finite set of concept membership axioms a : C, ∃hasAnimal.P et v N atureLover role membership axioms (a, b) : R, equality axioms a = b fluffy : Cat and inequality axioms a 6= b, where C ∈ C, R ∈ R and tom : Cat a, b ∈ I. A knowledge base (KB) K = (T , A) consists of a Cat v P et TBox T and an ABox A and is usually assigned a seman- (kevin, fluffy) : hasAnimal tics in terms of interpretations I = (∆I , ·I ), where ∆I is a (kevin, tom) : hasAnimal non-empty domain and ·I is the interpretation function that assigns an element in ∆I to each a ∈ I, a subset of ∆I to It states that individuals that own an animal which is a pet each C ∈ A and a subset of ∆I × ∆I to each R ∈ R. are nature lovers and that kevin owns the animals fluffy The mapping ·I is extended to all concepts (where and tom, which are cats. Moreover, cats are pets. The KB RI (x) = {y|(x, y) ∈ RI }) as: entails the query Q = kevin : N atureLover. Querying KBs: The Tableau Algorithm >I = ∆I In order to answer queries to DL KBs, a tableau algorithm ⊥I = ∅ can be used. A tableau is an ABox represented as a graph (C1 u C2 )I = C1I ∩ C2I G where each node corresponds to an individual a and is (C1 t C2 )I = C1I ∪ C2I labeled with the set of concepts L(a) to which a belongs. (¬C)I = ∆I \ C I Each edge ha, bi in the graph is labeled with the set of roles (∀R.C)I = {x ∈ ∆I |RI (x) ⊆ C I } L(ha, bi) to which the couple (a, b) belongs. A tableau algo- (∃R.C)I = {x ∈ ∆I |RI (x) ∩ C I 6= ∅} rithm proves an axiom by refutation, starting from a tableau that contains the negation of the axiom. For example, the ax- In the following we describe SHOIN (D) showing what it iom C v D can be proved by showing that C u¬D is empty, adds to ALC. A role is either an atomic role R ∈ R or the while, if the query is a class assertion, C(a), we add ¬C to inverse R− of an atomic role R ∈ R. We use R− to denote the label of a. For testing the inconsistency of a concept C the set of all inverses of roles in R. An RBox R consists of we have to test the emptiness of C by adding a new anony- a finite set of transitivity axioms T rans(R), where R ∈ R, mous node a to the tableau whose label contains C. Then, and role inclusion axioms R v S, where R, S ∈ R ∪ R− . the tableau algorithm repeatedly applies a set of consistency If a ∈ I, then {a} is a concept called nominal, and if C, preserving tableau expansion rules until a clash (i.e., a con- C1 and C2 are concepts and R ∈ R∪R− , then ≥ nR and ≤ tradiction, for example, a concept C and a node a where C nR for an integer n ≥ 0 are also concepts. A SHOIN (D) and ¬C are present in the label of a) is detected or a clash- KB K = (T , R, A) consists of a TBox T , an RBox R and free graph is found to which no more rules are applicable. If an ABox A. no clashes are found, the tableau represents a model for the The mapping ·I is extended to all new concepts (where negation of the query, which is thus not entailed. #X denotes the cardinality of the set X) as: Each expansion rule updates as well a tracing function τ , which associates labels of nodes and edges with a subset (R− )I = {(y, x)|(x, y) ∈ RI } of the axioms of the KB. τ is initialized as the empty set {a}I = {aI } for all the elements of its domain except for τ (C, a) and (≥ nR)I = {x ∈ ∆I |#RI (x) ≥ n} τ (R, ha, bi) to which the values {a : C} and {(a, b) : R} are (≤ nR)I = {x ∈ ∆I |#RI (x) ≤ n} assigned if a : C and (a, b) : R are in the ABox respectively. The tableau expansion rules for SHOIN (D) are shown in SHOIN (D) allows for the definition of datatype roles, Figure 1, where the rules for the ALC DL are marked by i.e., roles that map an individual to an element of a datatype (∗). such as integers, floats, etc. Then new concept definitions in- For ensuring the termination of the algorithm, a special volving datatype roles are added that mirror those involving condition known as blocking (Kalyanpur 2006) is used. In roles introduced above. We also assume that we have predi- a tableau a node x can be a nominal node if its label L(x) cates over the datatypes. contains a nominal or a blockable node. If there is an edge SHOIN (D) is decidable iff there are no number restric- e = hx, yi then y is a successor of x and x is a predecessor tions on roles which are transitive or have transitive subroles. of y. Ancestor is the transitive closure of predecessor while A query Q over a KB K is usually an axiom for which we descendant is the transitive closure of successor. A node y want to test the entailment from the KB, written K |= Q. The is called an R-neighbour of a node x if y is a successor of x entailment test may be reduced to checking the unsatisfia- and R ∈ L(hx, yi), where R ∈ R. bility of a concept in the knowledge base, i.e., the emptiness An R-neighbour y of x is safe if (i) x is blockable or if of the concept. For example, the entailment of the axiom (ii) x is a nominal node and y is not blocked. Finally, a node C v D may be tested by checking the unsatisfiability of the x is blocked if it has ancestors x0 , y and y0 such that all the concept C u ¬D while the entailment of the axiom a : C following conditions are true: (1) x is a successor of x0 and may be tested by checking the unsatisfiability of a : ¬C. y is a successor of y0 , (2) y, x and all nodes on the path from y to x are blockable, (3) L(x) = L(y) and L(x0 ) = nectives. It compactly encodes the set of all MinAs. Let as- L(y0 ), (4) L(hx0 , xi) = L(hy0 , yi). In this case, we say that sume that each axiom E of a KB K is associated with a y blocks x. A node is blocked also if it is blockable and all its propositional variable, indicated with var(E). The set of all predecessors are blocked; if the predecessor of a safe node propositional variables is indicated with var(K). A valua- x is blocked, then we say that x is indirectly blocked. tion ν of a monotone Boolean formula is the set of proposi- tional variables that are true. For a valuation ν ⊆ var(K), Finding Explanations let Kν := {t ∈ K|var(t) ∈ ν}. The problem of finding explanations for a query has been in- Definition 2 (Pinpointing formula) Given a query Q and vestigated by various authors (Schlobach and Cornet 2003; a KB K, a monotone Boolean formula φ over var(K) is Kalyanpur 2006; Halaschek-Wiener, Kalyanpur, and Parsia called a pinpointing formula for Q if for every valuation 2006; Kalyanpur et al. 2007). It was called axiom pinpoint- ν ⊆ var(K) it holds that Kν |= Q iff ν satisfies φ. ing in (Schlobach and Cornet 2003) and considered as a non- In Lemma 2.4 of (Baader and Peñaloza 2010b) the authors standard reasoning service useful for tracing derivations and proved that the set of all MinAs can be obtained by trans- debugging ontologies. In particular, minimal axiom sets or forming the pinpoiting formula into DNF and removing dis- MinAs for short, also called explanations, are introduced in juncts implying other disjuncts. The example below illus- (Schlobach and Cornet 2003). trates axiom pinpointing and the pinpointing formula. Definition 1 (MinA) Let K be a knowledge base and Q an Example 2 (Pinpointing formula) Consider the KB of Ex- axiom that follows from it, i.e., K |= Q. We call a set M ⊆ K ample 1. We associate Boolean variables to axioms as fol- a minimal axiom set or MinA for Q in K if M |= Q and it lows: is minimal w.r.t. set inclusion. F1 = ∃hasAnimal.P et v N atureLover The problem of enumerating all MinAs is called MIN - A - F2 = (kevin, fluffy) : hasAnimal ENUM in (Schlobach and Cornet 2003). A LL -M INA S (Q, K) F3 = (kevin, tom) : hasAnimal is the set of all MinAs for query Q in the knowledge base K. F4 = fluffy : Cat The tableau algorithm returns a single MinA using the F5 = tom : Cat tracing function. To solve MIN - A - ENUM, reasoners written F6 = Cat v P et. in imperative languages, like Pellet (Sirin et al. 2007), have Let Q = kevin : N atureLover be the query, then A LL - to implement a search strategy in order to explore the entire M INA S (Q, K) = {{F2 , F4 , F6 , F1 }, {F3 , F5 , F6 , F1 }}, search space of the possible explanations. In particular, Pel- while the pinpointing formula is ((F2 ∧ F4 ) ∨ (F3 ∧ F5 )) ∧ let, that is written entirely in Java, uses Reiter’s hitting set F6 ∧ F1 . algorithm (Reiter 1987). The algorithm, described in detail In the following, we briefly define how a tableau algorithm in (Kalyanpur 2006), starts from a MinA S and initializes can be modified to find the pinpointing formula. For more a labeled tree called Hitting Set Tree (HST) with S as the details and formal definitions see (Baader and Peñaloza label of its root v. Then it selects an arbitrary axiom E in 2010b). S, it removes it from K, generating a new knowledge base Given a KB K, the modified algorithm associates a label K0 = K − {E}, and tests the unsatisfiability of C w.r.t. K0 . lab(a) that is a monotone Boolean formula over var(K) to If C is still unsatisfiable, we obtain a new explanation. The every assertion a. For deciding whether a rule is applicable algorithm adds a new node w and a new edge hv, wi to the we have to control the insertability of the new assertion. Let tree, then it assigns this new explanation to the label of w and A be a set of labeled assertions and ψ a monotone Boolean the axiom E to the label of the edge. The algorithm repeats formula, the assertion a is ψ−insertable into A if either a ∈/ this process until the unsatisfiability test returns negative: in A, or a ∈ A but ψ 2 lab(a). Given a set B of assertions that case the algorithm labels the new node with OK, makes and a set A of labeled assertions, the set of ψ−insertable it a leaf, backtracks to a previous node, selects a different ax- elements of B into A is defined as insψ (B, A) := {b ∈ iom to be removed from the KB and repeats these operations B|b is ψ−insertable into A}. For deciding the applicability until the HST is fully built. The algorithm also eliminates ex- of a rule we need also to give the definition of substitution. traneous unsatisfiability tests based on previous results: once A substitution is a mapping ρ : V → D, where V is a finite a path leading to a node labeled OK is found, any super- set of variables and D is a countably infinite set of constants set of that path is guaranteed to be a path leading to a node that contains all the individuals in the KB and all the fresh where C is satisfiable, and thus no additional unsatisfiability individuals created by the application of the rules. Variables test is needed for that path, as indicated by an X in the node are seen as placeholder for individuals in the assertions. For label. When the HST is fully built, all leaves of the tree are example, an assertion can be C(x) or R(x, y) where C is a labeled with OK or X. The distinct non leaf nodes of the concept, R is a role and x and y are variables. In this case, tree collectively represent the set A LL -M INA S(C, K). let C(x) be an assertion with the variable x and ρ : x → a In (Baader and Peñaloza 2010a; 2010b) the authors con- a substitution, then C(x)ρ denotes the assertion obtained by sider the problem of finding a pinpointing formula instead replacing the variable with its ρ−image, i.e. C(a). A rule of A LL -M INA S (Q, K). The pinpointing formula is a mono- is of the form (B0 , S) → {B1 , ..., Bm } where Bi are finite tone Boolean formula in which each Boolean variable cor- set of assertions and S is a finite set of axioms. A rule is responds to an axiom of the KB. This formula is built us- applicable with a substitution ρ on the variable occurring in ing the variables and the conjunction and disjunction con- B0 if S ⊆ K, B0 ρ ⊆ A, where A is the set of assertions Deterministic rules: → unfold (∗): if A ∈ L(a), A atomic and (A v D) ∈ K, then if D ∈/ L(a), then Add(D, L(a)) τ (D, a) := (τ (A, a) ∪ {A v D}) → CE (∗): if (C v D) ∈ K, with C not atomic, a not blocked, then if (¬C t D) ∈ / L(a), then Add((¬C t D), a) τ ((¬C t D), a) := {C v D} → u (∗): if (C1 u C2 ) ∈ L(a), a is not indirectly blocked, then if {C1 , C2 } 6⊆ L(a), then Add({C1 , C2 }, a) τ (Ci , a) := τ ((C1 u C2 ), a) → ∃ (∗): if ∃S.C ∈ L(a), a is not blocked, then if a has no S-neighbor b with C ∈ L(b), then create new node b, Add(S, ha, bi), Add(C, b) τ (C, b) := τ ((∃S.C), a) τ (S, ha, bi) := τ ((∃S.C), a) → ∀ (∗): if ∀(S.C) ∈ L(a), a is not indirectly blocked and there is an S-neighbor b of a, then if C ∈/ L(b), then Add(C, b) τ (C, b) := τ ((∀S.C), a) ∪ τ (S, ha, bi) → ∀+ : if ∀(S.C) ∈ L(a), a is not indirectly blocked and there is an R-neighbor b of a, T rans(R) and R v S, then if ∀R.C ∈ / L(b), then Add(∀R.C, b) τ ((∀R.C), b) := τ ((∀S.C), a) ∪ τ (R, ha, bi) ∪ {T rans(R)} ∪ {R v S} →≥: if (≥ nS) ∈ L(a), a is not blocked, then if there are no n safe S-neighbors b1 , ..., bn of a with bi 6= bj , then create n new nodes b1 , ..., bn ; Add(S, ha, bi i); 6=(bi , bj ) τ (S, ha, bi i) := τ ((≥ nS), a) τ (6=(bi , bj )) := τ ((≥ nS), a) → O: if, {o} ∈ L(a) ∩ L(b) and not a6=b, then M erge(a, b) τ (M erge(a, b)) := τ ({o}, a) ∪ τ ({o}, b) For each concept Ci in L(a), τ (Add(Ci , L(b))) := τ (Add(Ci , L(a))) ∪ τ (M erge(a, b)) (similarly for roles merged, and correspondingly for concepts in L(b)) Non-deterministic rules: → t (∗): if (C1 t C2 ) ∈ L(a), a is not indirectly blocked, then if {C1 , C2 } ∩ L(a) = ∅, then Generate graphs Gi := G for each i ∈ {1, 2} Add(Ci , a) in Gi for each i ∈ {1, 2} τ (Ci , a) := τ ((C1 t C2 ), a) →≤: if (≤ nS) ∈ L(a), a is not indirectly blocked, and there are m S-neighbors b1 , ..., bm of a with m > n, then For each possible pair bi , bj , 1 ≤ i, j ≤ m; i 6= j then Generate a graph G0 τ (M erge(bi , bj )) := τ ((≤ nS), a) ∪ τ (S, ha, b1 i)... ∪ τ (S, ha, bm i) if bj is a nominal node, then M erge(bi , bj ) in G0 , else if bi is a nominal node or ancestor of bj , then M erge(bj , bi ) else M erge(bi , bj ) in G0 if bi is merged into bj , then for each concept Ci in L(bi ), τ (Ci , bj ) := τ (Ci , bi ) ∪ τ (M erge(bi , bj )) (similarly for roles merged, and correspondingly for concepts in bj if merged into bi ) Figure 1: TRILL tableau expansion rules; the subset of rules marked by (∗) is employed by TRILLP . contained in the ABox and found during inference, and, for apply_all_rules(Tab,Tab2):- apply_nondet_rules([...],Tab,Tab1), every 1 ≤ i ≤ m and every substitution ρ0 on the variables (Tab=Tab1 -> Tab2=Tab1 ; 0 W in B0 ∪ Bi , we occurring W have insψ (Bi ρ , A) 6= ∅, where apply_all_rules(Tab1,Tab2)). ψ := b∈B0 lab(bρ) ∧ s∈S lab(s). Moreover, except for the unfold rule, the node N to which the rule is applicable is apply_nondet_rules([],Tab,Tab1):- not (indirectly) blocked. When the tableau is fully built, the apply_det_rules([...],Tab,Tab1). algorithm conjoins the labels of each clash for building the final pinpointing formula. apply_nondet_rules([H|T],Tab,Tab1):- C=..[H,Tab,L], TRILL and TRILLP call(C),! member(Tab1,L), Both TRILL and TRILLP implement a tableau algorithm, Tab \= Tab1. the first solves MIN - A - ENUM while the second computes the pinpointing formula representing the set of MinAs. They can apply_nondet_rules([_|T],Tab,Tab1):- answer concept and role membership queries, subsumption apply_nondet_rules(T,Tab,Tab1). queries and can test the unsatifiability of a concept of the KB or the inconsistency of the entire KB. TRILL and TRILLP apply_det_rules([],Tab,Tab). are implemented in Prolog, so the management of the non- determinism of the rules is delegated to the language. apply_det_rules([H|T],Tab,Tab1):- C=..[H,Tab,Tab1], We use the Thea2 library (Vassiliadis, Wielemaker, call(C),!. and Mungall 2009) for converting OWL DL KBs into Prolog. Thea2 performs a direct translation of the apply_det_rules([_|T],Tab,Tab1):- OWL axioms into Prolog facts. For example, a sim- apply_det_rules(T,Tab,Tab1). ple subclass axiom between two named classes Cat v P et is written using the subClassOf/2 predicate as subClassOf(‘Cat’,‘Pet’). For more complex ax- Figure 2: Definition of the non-deterministic expansion ioms, Thea2 exploits the list construct of Prolog, so the rules by means of the predicates apply all rules/2, axiom N atureLover ≡ P etOwner t GardenOwner apply nondet rules/3 and apply det rules/3. becomes equivalentClasses([‘NatureLover’, The list [...] contains the available rules and is different unionOf([‘PetOwner’,‘GardenOwner’])]). in TRILL and TRILLP . In order to represent the tableau, TRILL and TRILLP use a pair T ableau = (A, T ), where A is a list containing infor- mation about individuals and class assertions with the cor- T ab, returns the tableau T ab1 obtained by the application responding value of the tracing function. The tracing func- of the rule to T ab. Expansion rules are applied in order tion stores a fragment of the knowledge base in TRILL and by apply all rules/2, first the non-deterministic the pinpointing formula in TRILLP . T is a triple (G, RBN , ones and then the deterministic ones. The predicate RBR) in which G is a directed graph that contains the struc- apply nondet rules/3 takes as input the ture of the tableau, RBN is a red-black tree (a key-value list of non-deterministic rules and the current dictionary), where a key is a couple of individuals and its tableau and returns a tableau obtained by the value is the set of the labels of the edge between the two application of one of the rules. It is called as individuals, and RBR is a red-black tree, where a key is a apply nondet rules(RuleList,Tab,Tab1) and role and its value is the set of couples of individuals that are is shown in Figure 2. linked by the role. This representation allows to quickly find If a non-deterministic rule is applicable, the list of the information needed during the execution of the tableau tableaux obtained by its application is returned by the algorithm. For managing the blocking system we use a predi- predicate corresponding to the applied rule, a cut is per- cate for each blocking state: nominal/2, blockable/2, formed to avoid backtracking to other rule choices and a blocked/2, indirectly blocked/2 and safe/3. tableau from the list is non-deterministically chosen with Each predicate takes as arguments the individual Ind and the member/2 predicate. If no non-deterministic rule is ap- the tableau (A, T ); safe/3 takes as input also the role plicable, deterministic rules are tried sequentially with the R. For each individual Ind in the ABox, we add the atom predicate apply det rules/3, shown in Figure 2, that is nominal(Ind) to A, then every time we have to check the called as apply det rules(RuleList,Tab,Tab1). blocking status of an individual we call the corresponding It takes as input the list of deterministic rules and the current predicate that returns the status by checking the tableau. tableau and returns a tableau obtained with the application Deterministic and non-deterministic tableau expansion of one of the rules. After the application of a determinis- rules are treated differently. Non-deterministic rules are tic rule, a cut avoids backtracking to other possible choices implemented by a predicate rule name(T ab, T abList) for the deterministic rules. If no rule is applicable, the input that, given the current tableau T ab, returns the list of tableau is returned and rule application stops, otherwise a tableaux T abList created by the application of the rule to new round of rule application is performed. T ab. Deterministic rules are implemented by a predicate In Figure 1, the symbol (∗) denotes the rules shared by rule name(T ab, T ab1) that, given the current tableau TRILL and TRILLP . In these rules, the operator ∪ for τ means union between two sets in TRILL, while in TRILLP We can now assign probabilities to queries. Given a world it joins two Boolean formulas with the OR Boolean operator. w, the probability of a query Q is defined as P (Q|w) = 1 if Moreover, when a concept is already present in a node label, w |= Q and 0 otherwise. The probability of a query can be TRILL checks whether to update the tracing function by ver- defined by marginalizing the joint probability of the query ifying that the corresponding set of axioms is not a subset of and the worlds. τ , while TRILLP performs a ψ−insertability test. X In case the assertion a to be inserted is already associ- P (Q) = P (Q, w) (2) ated with the corresponding individual, TRILLP tests its w∈WK X ψ−insertability by means of a satisfiability solver. In par- = P (Q|w)P (w) (3) ticular, it conjoins the negation of lab(a) with the Boolean w∈WK formula associated to the individual in the tableau, and tests X the satisfiability of such formula. If the test returns true, the = P (w) (4) two Boolean formulas are combined with the OR Boolean w∈WK :w|=Q operator. The following example illustrates inference under DISPONTE semantics. Computing the Probability The aim of our work is to implement algorithms which Example 3 Consider the following KB, a probabilistic ver- can compute the probability of queries to KBs following sion of that proposed in Example 1. DISPONTE (Riguzzi et al. 2012). DISPONTE applies the (1) 0.5 :: ∃hasAnimal.P et v N atureLover distribution semantics (Sato 1995) of probabilistic logic pro- fluffy : Cat gramming to DLs. A program following this semantics de- tom : Cat fines a probability distribution over normal logic programs (2) 0.6 :: Cat v P et called worlds. Then the distribution is extended to a joint (kevin, fluffy) : hasAnimal distribution over worlds and queries from which the proba- (kevin, tom) : hasAnimal bility of a query is obtained by marginalization. In DISPONTE, a probabilistic knowledge base K con- It indicates that the individuals that own an animal which tains a set of probabilistic axioms which take the form is a pet are nature lovers with a 50% probability and cats p :: E (1) are pets with a 60% probability. The KB has four possible worlds: where p is a real number in [0, 1] and E is a DL axiom. The probability p can be interpreted as an epistemic prob- {(1), (2)}, {(1)}, {(2)}, {} ability, i.e., as the degree of our belief in the truth of ax- and the query axiom Q = kevin : N atureLover is true in iom E. For example, a probabilistic concept membership the first of them, while in the remaining ones it is false. The axiom p :: a : C means that we have degree of belief p in probability of the query is P (Q) = 0.5 · 0.6 = 0.3. C(a). A probabilistic concept inclusion axiom of the form When a probabilistic KB is given as input, all the axioms p :: C v D represents the fact that we believe in the truth of are translated by means of the Thea2 library. Then, for each C v D with probability p. probabilistic axiom of the form P rob :: Axiom, a fact The idea of DISPONTE is to associate independent p(Axiom,Prob) is asserted in the Prolog KB. Boolean random variables to the axioms. To obtain a world To compute the probability of queries to KBs following w we decide whether to include each axiom or not in w. the DISPONTE semantics, we can first perform MIN - A - A world therefore is a non probabilistic KB that can be as- ENUM . Then the explanations must be made mutually ex- signed a semantics in the usual way. A query is entailed by clusive, so that the probabilities of individual explanations a world if it is true in every model of the world. are computed and summed. This can be done by exploit- Formally, an atomic choice is a pair (Ei , k) where Ei ing a splitting algorithm as shown in (Poole 2000). Alter- is the ith probabilistic axiom and k ∈ {0, 1} indicates natively, we can assign independent Boolean random vari- whether Ei is chosen to be included in a world (k = 1) ables to the axioms contained in the explanations and define or not (k = 0). If a set of atomic choices κ is consistent, the DNF Boolean formula fK WwhichV models theVset of ex- i.e., (Ei , k) ∈ κ, (Ei , m) ∈ κ implies k = m (only planations K. Thus fK (X) = κ∈K (Ei ,1) Xi (Ei ,0) Xi one decision is taken for each axiom), it is called a com- where X = {Xi |(Ei , k) ∈ κ, κ ∈ K} is the set of Boolean Q The probability posite choice. Q of a composite choice κ is random variables. P (κ) = (Ei ,1)∈κ pi (Ei ,0)∈κ (1 − pi ), where pi is the TRILLP , instead, computes directly a pinpointing for- probability associated with axiom Ei . A selection σ is a mula which is a monotone Boolean formula that represents composite choice which contains an atomic choice (Ei , k) the set of all MinAs. for every axiom of the theory. A selection σ identifies a the- Irrespective of which representation of the explanations ory wσ called a world in this way: wσ = {Ei |(Ei , 1) ∈ we choose, a DNF or a general pinpointing formula, we can σ}. Q The probabilityQ of a world wσ is P (wσ ) = P (σ) = apply knowledge compilation and transform it into a Binary (Ei ,1)∈σ p i (Ei ,0)∈σ (1 − Pi p ). P (wσ ) is a probability dis- Decision Diagram (BDD), from which we can compute the tribution over worlds, i.e., w∈WK P (w) = 1, where WK probability of the query with a dynamic programming algo- is the set of all worlds. rithm that is linear in the size of the BDD. X1 n1 various complexity to which we added 50 probabilistic ax- ioms: X2 n2 • BRCA1 , which models the risk factor of breast cancer; • an extract of the DBPedia2 ontology obtained from X3 n3 Wikipedia; • Biopax level 33 , which models metabolic pathways; 1 0 • Vicodi4 , which contains information on European history. Figure 3: BDD representing the function f (X) = (X1 ∧ For the tests, we used a version of the DBPedia and Biopax X3 ) ∨ (X2 ∧ X3 ). KBs without the ABox and a version of BRCA and of Vicodi with an ABox containing 1 individual and 19 individuals re- spectively. We added 50 probabilistic axioms to each KB. A BDD for a function of Boolean variables is a rooted In this experimentation, the probabilistic parameter values graph that has one level for each Boolean variable. A node n were learned using EDGE (Riguzzi et al. 2013b), a system in a BDD has two children: one corresponding to the 1 value that computes the probability value associated with axioms of the variable associated with the level of n, indicated with starting from a set of positive and negative examples in the child1 (n), and one corresponding to the 0 value of the vari- form of class assertion axioms that we regard as true (false), able, indicated with child0 (n). When drawing BDDs, the 0- and for which we would like to get an high (low) probability -branch - the one going to child0 (n) - is distinguished from respectively. the 1-branch by drawing it with a dashed line. The leaves For each dataset, we randomly created 100 different store either 0 or 1. Figure 3 shows a BDD for the func- queries. In particular, for the DBPedia and Biopax datasets, tion f (X) = (X1 ∧ X3 ) ∨ (X2 ∧ X3 ), where the variables we created 100 subclass-of queries, while for the other KBs X = {X1 , X2 , X3 } are independent Boolean random vari- we created 80 subclass-of and 20 instance-of queries. For ables. generating the subclass-of queries, we randomly selected A BDD performs a Shannon expansion of the Boolean two classes that are connected in the hierarchy of classes, formula f (X), so that, if X is the variable associated with so that each query had at least one explanation. For the the root level of a BDD, the formula f (X) can be rep- instance-of queries, we randomly selected an individual a and a class to which a belongs by following the hierarchy resented as f (X) = X ∧ f X (X) ∨ X ∧ f X (X) where of the classes, starting from the classes to which a explicitly f X (X) (f X (X)) is the formula obtained by f (X) by set- belongs in the KB. ting X to 1 (0). Now the two disjuncts are pairwise exclusive Table 1 shows, for each ontology, the average number of and the probability of f (X) being true can be computed as different MinAs computed and the average time in seconds P (f (X)) = P (X)P (f X (X)) + (1 − P (X))P (f X (X)) by that TRILL, TRILLP and BUNDLE took for computing the knowing the probabilities of the Boolean variables of being probability of the queries. In particular, the BRCA and the true. version of DBPedia that we used contain a large number of subclass axioms between complex concepts. These pre- TRILL-on-SWISH liminary tests show that both TRILL and TRILLP perfor- mances can sometimes be better than BUNDLE, even if they In order to popularize DISPONTE, we developed a Web lack all the optimizations that BUNDLE inherits from Pel- application called “TRILL-on-SWISH” and available at let. This represents evidence that a Prolog implementation http://trill.lamping.unife.it. We exploited of a Semantic Web tableau reasoner is feasible and that may SWISH (Lager and Wielemaker 2014), a recently proposed lead to practical systems. Moreover, TRILLP provides an Web framework for logic programming that is based on var- improvement of the execution time with respect to TRILL ious features and packages of SWI-Prolog. SWISH allows when more MinAs are present. the user to write Prolog programs and ask queries in the browser without installing SWI-Prolog on his machine. We modified it in order to manage OWL KBs. SWISH also al- Related Work lows users to collaborate on code development. TRILL-on- Usually, DL reasoners implement a tableau algorithm using SWISH allows users to write a KB in the RDF/XML format a procedural language. Since some tableau expansion rules directly in the web page or load it from a URL, and specify are non-deterministic, the developers have to implement a queries that are answered by TRILL running on the server. search strategy from scratch. Moreover, in order to solve Once the computation ends, the results are sent to the client MIN - A - ENUM , all different ways of entailing an axiom must browser and visualized in the Web page. be found. For example, Pellet (Sirin et al. 2007) is a tableau 1 http://www2.cs.man.ac.uk/˜klinovp/pronto/ Experiments brc/cancer_cc.owl In order to evaluate TRILL and TRILLP performances, we 2 http://dbpedia.org/ 3 compared them with BUNDLE, a reasoner for DISPONTE http://www.biopax.org/ 4 based on Pellet. We used four different knowledge bases of http://www.vicodi.org/ Table 1: Average number of MinAs and average time (in seconds) for computing the probability of queries with the reasoners TRILL, TRILLP and BUNDLE. DATASET AVG . N . MINA S TRILL TIME ( S ) TRILLP TIME ( S ) BUNDLE TIME ( S ) BRCA 6.49 27.87 4.74 6.96 DBPedia 16.32 51.56 4.67 3.79 Biopax level 3 3.92 0.12 0.12 1.85 Vicodi 1.02 0.19 0.19 1.12 reasoner for OWL written in Java and able to solve MIN - ability of queries. FOProblog is a reasoner for FOL that is A - ENUM . It computes A LL -M INA S (Q, K) by finding a sin- not tailored to DLs, so the algorithm could be suboptimal for gle MinA using the tableau algorithm and then applying the them. hitting set algorithm to find all the other MinAs. Recently, Calı̀ et al. (2009) combine DLs and logic programs in or- BUNDLE (Riguzzi et al. 2013a) was proposed for reasoning der to integrate ontologies and rules. They use a tightly cou- over DISPONTE KBs. BUNDLE exploits Pellet for solving pled approach to (probabilistic) disjunctive description logic MIN - A - ENUM and computes the probability of queries. programs. They define a description logic program as a pair Reasoners written in Prolog can exploit its backtracking (L, P ), where L is a DL KB and P is a disjunctive logic facilities for performing the search. This has been observed program which contains rules on concepts and roles of L. in various works. Beckert and Posegga (1995) proposed a P may contain probabilistic alternatives in the style of ICL tableau reasoner in Prolog for FOL based on free-variable (Poole 1997). Interpretations assign a probability to ground semantic tableaux. However, the reasoner is not tailored to atoms, in the style of Nilsson probabilistic logic (Nilsson DLs. Meissner (2004) presented the implementation of a 1986). Queries can be answered by finding all answer sets. Prolog reasoner for the DL ALCN . This work was the ba- Differently from (Calı̀ et al. 2009), in DISPONTE interpre- sis of (Herchenröder 2006), that considered ALC and im- tations are not probabilistic and they are assigned a probabil- proved (Meissner 2004) by implementing heuristic search ity, instead of being a mapping from atoms to probabilities. techniques to reduce the running time. Faizi (2011) added In (Gavanelli et al. 2015a) and (Gavanelli et al. 2015b), to (Herchenröder 2006) the possibility of returning explana- we addressed representation and reasoning for Datalog± tions for queries but still handled only ALC. ontologies in an Abductive Logic Programming frame- Hustadt, Motik, and Sattler (2008) presented the KAON2 work, with existential and universal variables, and Con- algorithm that exploits basic superposition, a refutational straint Logic Programming constraints in rule heads. The un- theorem proving method for FOL with equality, and a new derlying abductive proof procedure can be directly exploited inference rule, called decomposition, to reduce a SHIQ KB as an ontological reasoner for query answering and consis- to a disjunctive datalog program. tency check. DLog (Lukácsy and Szeredi 2009) is an ABox reasoning algorithm for the SHIQ language that permits storing the Conclusions content of the ABox externally in a database and answers In this paper we have presented the algorithm TRILL for instance check and instance retrieval queries by transform- reasoning on SHOIN KBs and the algorithm TRILLP for ing the KB into a Prolog program. TRILL differs from these reasoning on ALC KBs. The experiments performed show works for the considered DL and from DLog for the capa- that Prolog is a viable language for implementing DL rea- bility of answering general queries. soning algorithms and that their performances are compara- A different approach is shown in (Ricca et al. 2009), who ble with those of a state-of-art reasoner such as BUNDLE. introduced a system for reasoning on a logic-based ontology In the future we plan to apply various optimizations to representation language, called OntoDLP, which is an exten- our systems in order to better manage the expansion of the sion of (disjunctive) ASP and can interoperate with OWL. tableau. In particular, we plan to carefully choose the rule This system, called OntoDLV, rewrites the OWL KB into the and node application order. We are also studying an exten- OntoDLP language, can retrieve information directly from sion of our systems for managing KBs integrating rules and external OWL ontologies and answers queries by using ASP. DL axioms. Moreover, we plan to exploit TRILL for im- OntoDLV cannot find the set of explanations thus it is not ap- plementing algorithms for learning the parameters of prob- plicable to DISPONTE KBs. All the presented systems are abilistic DISPONTE KBs, along the lines of (Bellodi and not able to compute the probability of queries. Riguzzi 2012; 2013; Riguzzi et al. 2014). Bruynooghe et al. (2010) presented FOProbLog, an ex- tension of ProbLog where a program contains a set of prob- References abilistic facts, i.e. facts annotated with probabilities, and a set of general clauses which can have positive and negative Baader, F., and Peñaloza, R. 2010a. Automata-based axiom probabilistic facts in their body. Each fact is assumed to be pinpointing. J. Autom. Reasoning 45(2):91–129. probabilistically independent. FOProbLog follows the dis- Baader, F., and Peñaloza, R. 2010b. Axiom pinpointing in tribution semantics and exploits BDDs to compute the prob- general tableaux. J. Log. Comput. 20(1):5–34. Baader, F.; Calvanese, D.; McGuinness, D. L.; Nardi, D.; K., and et al., eds., ISWC/ASWC 2007, volume 4825 of and Patel-Schneider, P. F., eds. 2003. The Description LNCS, 267–280. Springer. Logic Handbook: Theory, Implementation, and Applica- Kalyanpur, A. 2006. Debugging and Repair of OWL On- tions. Cambridge University Press. tologies. Ph.D. Dissertation, The Graduate School of the Baader, F.; Horrocks, I.; and Sattler, U. 2008. Description University of Maryland. logics. In Handbook of knowledge representation. Elsevier. Lager, T., and Wielemaker, J. 2014. Pengines: Web logic chapter 3, 135–179. programming made easy. TPLP 14(4-5):539–552. Beckert, B., and Posegga, J. 1995. leantap: Lean tableau- Lukácsy, G., and Szeredi, P. 2009. Efficient description logic based deduction. J. Autom. Reasoning 15(3):339–358. reasoning in prolog: The dlog system. TPLP 9(3):343–414. Bellodi, E., and Riguzzi, F. 2012. Learning the struc- Meissner, A. 2004. An automated deduction system for ture of probabilistic logic programs. In Muggleton, S. H.; description logic with alcn language. Studia z Automatyki i Tamaddoni-Nezhad, A.; and Lisi, F. A., eds., ILP 2011, vol- Informatyki 28-29:91–110. ume 7207 of LNCS, 61–75. Springer. Nilsson, N. J. 1986. Probabilistic logic. Artif. Intell. Bellodi, E., and Riguzzi, F. 2013. Expectation Maximiza- 28(1):71–87. tion over binary decision diagrams for probabilistic logic programs. Intel. Data Anal. 17(2):343–363. Patel-Schneider, P, F.; Horrocks, I.; and Bechhofer, S. 2003. Tutorial on OWL. Bruynooghe, M.; Mantadelis, T.; Kimmig, A.; Gutmann, B.; Vennekens, J.; Janssens, G.; and Raedt, L. D. 2010. Problog Poole, D. 1997. The Independent Choice Logic for mod- technology for inference in a probabilistic first order logic. elling multiple agents under uncertainty. Artif. Intell. 94(1- In ECAI 2010 - 19th European Conference on Artificial In- 2):7–56. telligence, Lisbon, Portugal, August 16-20, 2010, Proceed- Poole, D. 2000. Abducing through negation as failure: sta- ings, volume 215 of Frontiers in Artificial Intelligence and ble models within the independent choice logic. J. Log. Pro- Applications, 719–724. IOS Press. gram. 44(1-3):5–35. Calı̀, A.; Lukasiewicz, T.; Predoiu, L.; and Stuckenschmidt, Reiter, R. 1987. A theory of diagnosis from first principles. H. 2009. Tightly coupled probabilistic description logic pro- Artif. Intell. 32(1):57–95. grams for the semantic web. In Journal on Data Semantics Ricca, F.; Gallucci, L.; Schindlauer, R.; Dell’Armi, T.; XII. Springer. 95–130. Grasso, G.; and Leone, N. 2009. OntoDLV: An ASP- Faizi, I. 2011. A Description Logic Prover in Prolog, Bache- based system for enterprise ontologies. J. Log. Comput. lor’s thesis, Informatics Mathematical Modelling, Technical 19(4):643–670. University of Denmark. Riguzzi, F.; Bellodi, E.; Lamma, E.; and Zese, R. 2012. Gavanelli, M.; Lamma, E.; Riguzzi, F.; Bellodi, E.; Zese, Epistemic and statistical probabilistic ontologies. In Bobillo, R.; and Cota, G. 2015a. Abductive logic programming for F., and et al., eds., URSW 2012, volume 900 of CEUR Work- datalog± ontologies. In Proceedings of the 30th Italian Con- shop Proceedings, 3–14. Sun SITE Central Europe. ference on Computational Logic (CILC2015). Accepted for Riguzzi, F.; Bellodi, E.; Lamma, E.; and Zese, R. 2013a. publication, CEUR Workshop Proceedings. Sun SITE Cen- BUNDLE: A reasoner for probabilistic ontologies. In RR tral Europe. 2013, volume 7994 of LNCS, 183–197. Springer. Gavanelli, M.; Lamma, E.; Riguzzi, F.; Bellodi, E.; Zese, Riguzzi, F.; Bellodi, E.; Lamma, E.; and Zese, R. 2013b. R.; and Cota, G. 2015b. Abductive logic programming for Parameter learning for probabilistic ontologies. In Datalog± ontologies and deductive rule integration. In Tech- Faber, W., and Lembo, D., eds., RR 2013, volume nical Communications of the 31st International Conference 7994 of LNCS, 265–270. Springer. http://www. on Logic Programming (ICLP15). Accepted for publication. ing.unife.it/docenti/FabrizioRiguzzi/ Halaschek-Wiener, C.; Kalyanpur, A.; and Parsia, B. 2006. Papers/RigBelLam-RR13a.pdf. Extending tableau tracing for ABox updates. Technical re- Riguzzi, F.; Bellodi, E.; Lamma, E.; Zese, R.; and Cota, G. port, University of Maryland. 2014. Learning probabilistic description logics. In URSW Herchenröder, T. 2006. Lightweight semantic web oriented III, volume 8816 of LNCS, 63–78. Springer. reasoning in Prolog: Tableaux inference for description log- Sato, T. 1995. A statistical learning method for logic pro- ics. Master’s thesis, School of Informatics, University of grams with distribution semantics. In ICLP 1995, 715–729. Edinburgh. MIT Press. Hitzler, P.; Krötzsch, M.; and Rudolph, S. 2009. Founda- Schlobach, S., and Cornet, R. 2003. Non-standard reason- tions of Semantic Web Technologies. CRCPress. ing services for the debugging of description logic termi- Hustadt, U.; Motik, B.; and Sattler, U. 2008. Deciding ex- nologies. In Gottlob, G., and Walsh, T., eds., IJCAI 2003, pressive description logics in the framework of resolution. 355–362. Morgan Kaufmann. Inf. Comput. 206(5):579–601. Sirin, E.; Parsia, B.; Cuenca-Grau, B.; Kalyanpur, A.; and Kalyanpur, A.; Parsia, B.; Horridge, M.; and Sirin, E. 2007. Katz, Y. 2007. Pellet: A practical OWL-DL reasoner. J. Finding all justifications of OWL DL entailments. In Aberer, Web Sem. 5(2):51–53. Vassiliadis, V.; Wielemaker, J.; and Mungall, C. 2009. Processing OWL2 ontologies using thea: An application of logic programming. In OWLED 2009, volume 529 of CEUR Workshop Proceedings. CEUR-WS.org.