Description Logics (DLs) are gaining a widespread adoption as the popularity of the Semantic Web increases. Traditionally, reasoning algorithms for DLs have been implemented in procedural languages such as Java or C++. In this paper, we present the system TRILL for “Tableau Reasoner for descrIption Logics in proLog”. TRILL answers queries to SHOIN (D) knowledge bases using a tableau algorithm. Prolog nondeterminism is used for easily handling non-deterministic expansion rules that produce more than one tableau. Moreover, given a query, TRILL is able to return instantiated explanations for the query, i.e., instantiated minimal sets of axioms that allow the entailment of the query. The Thea2 library is exploited by TRILL for parsing ontologies and for the internal Prolog representation of DL axioms.
The Semantic Web aims at making information available in a form that is
understandable by machines [
In order to fully support the development of the Semantic Web, efficient DL reasoners, such us Pellet, RacerPro, FaCT++ and HermiT, must be available to extract implicit information from the modeled ontologies. Most DL reasoners implement a tableau algorithm in a procedural language. However, some tableau expansion rules are non-deterministic, requiring the developers to implement a search strategy in an or-branching search space. Moreover, in some cases we want to compute all explanations for a query, thus requiring the exploration of all the non-deterministic choices done by the tableau algorithm.
In this paper, we present the system TRILL for “Tableau Reasoner for
descrIption Logics in proLog”, a tableau reasoner for the SHOIN (D) DL
implemented in Prolog. Prolog’s search strategy is exploited for taking into account
non-determinism of the tableau rules. TRILL uses the Thea2 library [
TRILL can check the consistency of a concept and the entailment of an
axiom from an ontology and return “instantiated explanations” for queries, a
non-standard reasoning service that is useful for debugging ontologies and for
performing probabilistic reasoning. Instantiated explanations record, besides the
axioms necessary to entail the query, also the individuals involved in the
application of the axioms. This service was used in [
Our ultimate aim is to use TRILL for performing probabilistic reasoning.
The availability of a Prolog implementation of a DL reasoner will also facilitate
the development of a probabilistic reasoner for integrations of probabilistic logic
programming [
In the following, section 2 briefly introduces SHOIN (D) and its translation into predicate logic. Section 3 defines the problem we are trying to solve while Section 4 illustrates related work. Section 5 discusses the tableau algorithm used by TRILL and Section 6 describes TRILL’s implementation. Section 7 shows preliminary experiments and Section 8 concludes the paper. 2
Description Logics (DLs) are knowledge representation formalisms that possess
nice computational properties such as decidability and/or low complexity, see
[
While DLs can be translated into FOL, they are usually represented using a syntax based on concepts and roles. A concept corresponds to a set of individuals of the domain while a role corresponds to a set of couples of individuals of the domain. We now briefly describe SHOIN (D).
Let A, R and I be sets of atomic concepts, roles and individuals, respectively. A role is either an atomic role R ∈ R or the inverse R− of an atomic role R ∈ R. We use R− to denote the set of all inverses of roles in R. An RBox R consists of a finite set of transitivity axioms T rans(R), where R ∈ R, and role inclusion axioms R v S, where R, S ∈ R ∪ R−. Concepts are defined by induction as follows. Each C ∈ A is a concept, ⊥ and > are concepts, and if a ∈ I, then {a} is a concept called nominal. If C, C1 and C2 are concepts and R ∈ R ∪ R−, then (C1 u C2), (C1 t C2), and ¬C are concepts, as well as ∃R.C, ∀R.C, ≥ nR and ≤ nR for an integer n ≥ 0. A TBox T is a finite set of concept inclusion axioms C v D, where C and D are concepts. We use C ≡ D to abbreviate the conjunction of C v D and D v C. An ABox A is a finite set of concept membership axioms a : C, role membership axioms (a, b) : R, equality axioms a = b and inequality axioms a 6= b, where C is a concept, R ∈ R and a, b ∈ I. A knowledge base (KB) K = (T , R, A) consists of a TBox T , an RBox R and an ABox A. A knowledge base K is usually assigned a semantics in terms of set-theoretic interpretations and models of the form I = (ΔI , ·I ) where ΔI is a non-empty domain and ·I is the interpretation function that assigns an element in ΔI to each a ∈ I, a subset of ΔI to each C ∈ A and a subset of ΔI × ΔI to each R ∈ R.
The semantics of DLs can be given equivalently by converting a KB into
a predicate logic theory and then using the model-theoretic semantics of the
resulting theory. A translation of SHOIN into First-Order Logic with Counting
Quantifiers is given in the following as an extension of the one given in [
πx(A) = A(x) πx(¬C) = ¬πx(C) πx({a}) = (x = a) πx(C u D) = πx(C) ∧ πx(D) πx(C t D) = πx(C) ∨ πx(D) πx(∃R.C) = ∃y.R(x, y) ∧ πy(C) πx(∃R−.C) = ∃y.R(y, x) ∧ πy(C) πx(∀R.C) = ∀y.R(x, y) → πy(C) πx(∀R−.C) = ∀y.R(y, x) → πy(C) πx(≥ nR) = ∃≥ny.R(x, y) πx(≥ nR−) = ∃≥ny.R(y, x) πx(≤ nR) = ∃≤ny.R(x, y) πx(≤ nR−) = ∃≤ny.R(y, x) and πy is obtained from πx by replacing x with y and vice-versa. Table 1 shows the translation of each axiom of SHOIN knowledge bases into predicate logic.
Axiom Translation C v D ∀x.πx(C) → πx(D)
R v S ∀x, y.R(x, y) → S(x, y) T rans(R) ∀x, y, z.R(x, y) ∧ R(y, z) → R(x, z)
a : C πa(C) (a, b) : R R(a, b) a = b a = b a 6= b a 6= b
SHOIN (D) adds to SHOIN datatype roles, i.e., roles that map an individual to an element of a datatype such as integers, floats, etc. Then new concept definitions involving datatype roles are added that mirror those involving roles introduced above. We also assume that we have predicates over the datatypes.
A query Q over a KB K is usually an axiom for which we want to test the entailment from the knowledge base, written K |= Q. The entailment test may be reduced to checking the unsatisfiability of a concept in the knowledge base, i.e., the emptiness of the concept.
SHOIN (D) is decidable if there are no number restrictions on non-simple roles. A role is non-simple iff it is transitive or has transitive subroles.
Given a predicate logic formula F , a substitution θ is a set of pairs x/a,
where x is a variable universally quantified in the outermost quantifier in F and
a ∈ I. The application of θ to F , indicated by F θ, is called an instantiation
of F and is obtained by replacing x with a in F and by removing x from the
external quantification for every pair x/a in θ. Formulas not containing variables
are called ground. A substitution θ is grounding for a formula F if F θ is ground.
Example 1. The following KB is inspired by the ontology people+pets [
Querying KBs in S HOI N (D) Traditionally, a reasoning algorithm decides whether an axiom is entailed or not by a KB by refutation: axiom E is entailed if ¬E has no model in the KB. Besides deciding whether an axiom is entailed by a KB, we want to find also instantiated explanations for the axiom.
The problem of finding explanations for a query has been investigated by
various authors [
Definition 1 (MinA). Let K be a knowledge base and Q an axiom that follows from it, i.e., K |= Q. We call a set M ⊆ K a minimal axiom set or MinA for Q in K if M |= Q and it is minimal w.r.t. set inclusion.
The problem of enumerating all MinAs is called min-a-enum in [
However, in some cases, besides All-MinAs(Q, K), we may want to know also the individuals to which the axioms were applied. We call this problem instantiated axiom pinpointing.
In instantiated axiom pinpointing we are interested in instantiated minimal sets of axioms that entail an axiom. An instantiated axiom set is a finite set F = {(F1, θ1), . . . , (Fn, θn)} where F1, . . . , Fn are axioms contained in K and θ1, . . . , θn are substitutions. Given two instantiated axiom sets F = {(F1, θ1), . . . , (Fn, θn)} and E = {(E1, δ1), . . . , (Em, δm)}, we say that F precedes E , written F E , iff, for each (Fi, θi) ∈ F , there exists an (Ej , δj ) ∈ E and a substitution η such that Fj θj = Eiδiη. Definition 2 (InstMinA). Let K be a knowledge base and Q an axiom that follows from it, i.e., K |= Q. We call F = {(F1, θ1), . . . , (Fn, θn)} an instantiated minimal axiom set or InstMinA for Q in K if {F1θ1, . . . , Fnθn} |= Q and F is minimal w.r.t. precedence.
Minimality w.r.t. precedence means that axioms in an InstMinA are as instantiated as possible. We call inst-min-a-enum the problem of enumerating all InstMinAs. All-InstMinAs(Q, K) is the set of all InstMinAs for the query Q in knowledge base K.
Example 2. The query Q = kevin : N atureLover of Example 1 has two MinAs (in predicate logic): { hasAnimal(kevin, fluffy ), Cat(fluffy ), ∀x.Cat(x) → P et(x), ∀x.∃y.hasAnimal(x, y) ∧ P et(y) → N atureLover(x)} and { hasAnimal(kevin, tom), Cat(tom), ∀x.Cat(x) → P et(x), ∀x.∃y.hasAnimal(x, y) ∧ P et(y) → N atureLover(x)}. The corresponding InstMinAs are {hasAnimal(kevin, fluffy ), Cat(fluffy ) → P et(fluffy ), Cat(fluffy ), hasAnimal(kevin, fluffy ) ∧ P et(fluffy ) → N atureLover(kevin)} and { hasAnimal(kevin, tom), Cat(tom), Cat(tom) → P et(tom), hasAnimal(kevin, tom) ∧ P et(tom) → N atureLover(kevin)}.
Instantiated axiom pinpointing is useful for a more fine-grained debugging of
the ontology: by highlighting the individuals to which axioms are applied, it
may point to parts of the ABox to be modified for repairing the KB.
inst-mina-enum is also required to support reasoning in probabilistic DLs, in particular
in those that follow the DISPONTE probabilistic semantics [
Usually, DL reasoners implement a tableau algorithm using a procedural
language. Since some tableau expansion rules are non-determinsitic, the developers
have to implement a search strategy from scratch. Moreover, in order to solve
min-a-enum, all different ways of entailing an axiom must be found. For
example, Pellet [
Reasoners written in Prolog can exploit Prolog’s backtracking facilities for
performing the search. This has been observed in various works. In [
In TRILL we use the tableau expansion rules for SHOIN (D) shown in
Figure 1 that are similar to those of Pellet [
For ensuring the termination of the algorithm, TRILL, as Pellet, uses a
special condition known as blocking [
An R-neighbour y of x is safe if (i) x is blockable or if (ii) x is a nominal node and y is not blocked. Finally, a node x is blocked if it has ancestors x0, y and y0 such that all the following conditions are true: (1) x is a successor of x0 and 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) = L(y0), (4) L(hx0, xi) = L(hy0, yi). In this case, we say that y blocks x. A node is blocked also if it is blockable and all its predecessors are blocked; if the predecessor of a safe node x is blocked, then we say that x is indirectly blocked.
Since we want to solve also the inst-min-a-enum problem, we modified the tableau expansion rules of Pellet to return a set of pairs (axiom, substitution) instead of a set of axioms. The tracing function τ now stores, together with information regarding concepts and roles, also information concerning individuals involved in the expansion rules, which will be returned at the end of the derivation process together with the axioms. In Figure 1, (A v D, a) is the abbreviation of (A v D, {x/a}), (R v S, a) of (R v S, {x/a}), (R v S, a, b) of (R v S, {x/a, y/b}), (Trans(R), a, b) of (Trans(R), {x/a, y/b}) and (Trans(R), a, b, c) of (Trans(R), {x/a, y/b, z/c}), with a, b, c individuals and x, y, z variables contained in the logical translation of the axioms (Table 1). The most important modifications of Pellet’s tableau algorithm are in the rules → ∀+ and → ∀. For rule → ∀+, we record in the explanation a transitivity axiom for the role R in which only two individuals, those connected by the super role S, are involved. For rule → ∀, we make a distinction between the case in which ∀S1.C was added to L(a1) by a chain of applications of → ∀+ or not. In the first case, we fully instantiate the transitivity and subrole axioms. In the latter case, we simply obtain τ (C, b) by combining the explanation of ∀S1.C(a1) with that of (a1, b) : S1. To clarify how the rules → ∀ and → ∀+ work we now give two examples. Example 3. Let us consider the query Q = ann : P erson for the following knowledge base: kevin : ∀kin.P erson (kevin, lara) : relative (lara, eva) : ancestor (eva, ann) : ancestor T rans(ancestor) T rans(relative) relative v kin ancestor v relative TRILL first applies the → ∀+ rule to kevin, adding ∀relative.P erson to the label of lara. The tracing function τ is (in predicate logic): τ (∀relative.P erson, lara) = { ∀y.kin(kevin, y) → P erson(y), relative(kevin, lara), relative(kevin, lara) → kin(kevin, lara), ∀z.relative(kevin, lara) ∧ relative(lara, z) → relative(kevin, z)} Note that the transitivity axiom is not fully instantiated, the variable z is still present. Then TRILL applies the → ∀+ rule to lara adding ∀ancestor.P erson to eva. The tracing function τ is (in predicate logic): Deterministic rules: → unfold: if A ∈ L(a), A atomic and (A v D) ∈ K, then if D ∈/ L(a), then
L(a) := L(a) ∪ {D} τ(D, a) := τ(A, a) ∪ {(A v D, a)} → CE: if (C v D) ∈ K, then if (¬C t D) ∈/ L(a), then
L(a) := L(a) ∪ {¬C t D} τ(¬C t D, a) := {(C v D, a)} → u: if (C1 u C2) ∈ L(a), then if {C1, C2} 6⊆ L(a), then
L(a) := L(a) ∪ {C1, C2} τ(Ci, a) := τ((C1 u C2), a) → ∃: if ∃S.C ∈ L(a), then if a has no S-neighbor b with C ∈ L(b), then create new node b, L(b) := {C}, L(ha, bi) := {S}, τ(C, b) := τ((∃S.C), a), τ(S, ha, bi) := τ((∃S.C), a) → ∀: if ∀S1.C ∈ L(a1), a1 is not indirectly blocked and there is an S1-neighbor b of a1, then if C ∈/ L(b), then L(b) := L(a) ∪ {C} if there is a chain of individuals a2, . . . , an and roles S2, . . . , Sn such that
Sn
i=2{(Trans(Si−1), ai, ai−1), (Si−1 v Si, ai, ai−1)} ⊆ τ(∀S1.C, a1) and ¬∃an+1 : {(Trans(Sn), an+1, an), (Sn v Sn+1, an+1)} ⊆ τ(∀S1.C, a1), then τ(C, b) := τ(∀S1.C, a1) \ Sn
i=2{(Trans(Si−1), ai, ai−1), (Si−1 v Si, ai, ai−1)}∪ Sn
i=2{(Trans(Si−1), ai, ai−1, b), (Si−1 v Si, ai, b)} ∪ τ(S1, ha1, bi) else
τ(C, b) := τ(∀S1.C, a1) ∪ τ(S1, ha1, 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 L(b) := L(b) ∪ {∀R.C}
τ(∀R.C, b) := τ(∀S.C, a) ∪ τ(R, ha, bi) ∪ {(Trans(R), a, b), (R v S, a, b)} →≥: 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; L(ha, bii) := {S}; add in the ABox 6= (bi, bj) τ(S, ha, bii) := τ((≥ nS), a) τ(6= (bi, bj)) := τ((≥ nS), a) → O: if, {o} ∈ L(a) ∩ L(b) and not a 6= b, then
Merge(a, b) τ(Merge(a, b)) := τ({o}, a) ∪ τ({o}, b) For each concept Ci in L(a), τ(Ci, b) := τ(Ci, a) ∪ τ(Merge(a, b)) (similarly for roles merged, and correspondingly for concepts in L(b)) Non-deterministic rules: → t: if (C1 t C2) ∈ L(a) and a is not indirectly blocked, then if {C1, C2} ∩ L(a) = ∅, then
Generate graphs Gi := G for each i ∈ {1, 2}, L(a) := L(a) ∪ {Ci} 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 Gk := G τ(Merge(bi, bj)) := (τ((≤ nS), a) ∪ τ(S, ha, b1i)... ∪ τ(S, ha, bmi)) For each concept Ci in L(bi), τ(Ci, bj) := τ(Ci, bi) ∪ τ(Merge(bi, bj)) (similarly for roles merged, and correspondingly for concepts in L(bj))
Fig. 1. TRILL tableau expansion rules for OWL DL. τ (∀ancestor.P erson, eva) = { ∀y.kin(kevin, y) → P erson(y), relative(kevin, lara), ancestor(lara, eva), ∀z.relative(kevin, lara) ∧ relative(lara, z) → relative(kevin, z), ∀z.ancestor(lara, eva) ∧ ancestor(eva, z) → ancestor(lara, z), relative(kevin, lara) → kin(kevin, lara), ancestor(lara, eva) → relative(lara, eva) } Now TRILL applies the → ∀ rule to eva adding P erson to the label of ann. The tracing function τ is (in predicate logic): τ (P erson, ann) = { ∀y.kin(kevin, y) → P erson(y), relative(kevin, lara), ancestor(lara, eva), ancestor(eva, ann), relative(kevin, lara) ∧ relative(lara, ann) → relative(kevin, ann), ancestor(lara, eva) ∧ ancestor(eva, ann) → ancestor(lara, ann), relative(kevin, ann) → kin(kevin, ann), ancestor(lara, ann) → relative(lara, ann) } Here the chain of transitivity and subrole axioms becomes ground. At this point the tableau contains a clash so the algorithm stops and returns the explanation given by τ (P erson, ann).
It is easy to see that the explanation entails the axiom represented by the arguments of τ . In general, the following theorem holds.
Theorem 1. Let Q be an axiom entailed by K and let S be the output of a reasoner with the tableau expansion rules of Figure 1, such as TRILL, with input Q and K. Then S ∈ All-InstMinAs(Q, K).
Proof. The full details of the proof are given in [
We use the Thea2 library [
In order to represent the tableau, we use a couple T ableau = (A, T ), where A is a list containing all the class assertions of the individuals with the corresponding value of τ and the information about nominal individuals, while T is a triple (G,RBN ,RBR) in which G is a directed graph that contains the structure of the tableau, RBN is a red-black tree in which each key is a couple of individuals and the value associated to it is the set of the labels of the edge between the two individuals, and RBR is a red-black tree in which each key is a role and the value associated to it is the set of couples of individuals that are linked by the role. This representation allows us to rapidly find the information needed during the execution of the tableau algorithm. For managing the blocking system we use a predicate for each blocking state, so we have the following predicates: nominal/2, blockable/2, blocked/2, indirectly blocked/2 and safe/3. Each predicate takes as arguments the individual Ind and the tableau, (A, T ). safe/3 takes as input also the role R. For each nominal individual Ind at the time of the creation of the ABox we add the atom nominal(Ind) to A, then every time we have to check the blocking status of an individual we call the corresponding predicate that returns the status by checking the tableau.
In TRILL deterministic and non-deterministic tableau expansion rules are treated differently, see Figure 1 for the list of rules. Deterministic rules are implemented by a predicate rule name(T ab, T ab1) that, given the current tableau T ab, returns the tableau T ab1 to which the rule was applied. Figure 2 shows the code of the deterministic rule → unfold. The predicate unfold rule/2 searches in T ab for an individual to which the rule can be applied and calls the predicate find sub sup class/3 in order to find the class to be added to the label of the individual. find/2 implements the search for a class assertion. Since the data structure that stores class assertions is currently a list, find/2 simply calls member/2. absent/3 checks if the class assertion axiom with the associated explanation is already present in A. Non-deterministic rules are implemented by a unfold_rule((A,T),([(classAssertion(D,Ind),[(Ax,Ind)|Expl])|A],T)):find((classAssertion(C,Ind),Expl),A), atomic(C), find_sub_sup_class(C,D,Ax), absent(classAssertion(D,Ind),[(Ax,Ind)|Expl],(A,T)). find_sub_sup_class(C,D,subClassOf(C,D)):
subClassOf(C,D). find_sub_sup_class(C,D,equivalentClasses(L)):equivalentClasses(L), member(C,L), member(D,L), C\==D. predicate rule name(T ab, T abList) that, given the current tableau T ab, returns the list of tableaux T abList obtained by applying the rule. Figure 3 shows the code of the non-deterministic rule → t. The predicate or rule/2 searches in T ab for an individual to which the rule can be applied and unifies T abList with the list of new tableaux created by scan or list/6.
Expansion rules are applied in order by apply all rules/2, first the nondeterministic ones and then the deterministic ones. The predicate apply nondet rules(RuleList,Tab,Tab1) takes as input the list of or_rule((A,T),L):find((classAssertion(unionOf(LC),Ind),Expl),A), \+ indirectly_blocked(Ind,T0), findall((A1,T),scan_or_list(LC,Ind,Expl,A,T,A1),L),
L\=[],!. scan_or_list([],_Ind,_Expl,A,T,A). scan_or_list([C|_T],Ind,Expl,A,T,[(classAssertion(C,Ind),Expl)|A]):absent(classAssertion(C,Ind),Expl,(A,T)). scan_or_list([_C|T],Ind,Expl,A0,T,A):scan_or_list(T,Ind,Expl,A0,T,A). non-deterministic rules and the current tableau and returns a tableau obtained by the application of one rule. apply nondet rules/3 is called as apply nondet rules([or rule,max rule],Tab,Tab1) and is shown in Fig. 4. If a non-deterministic rule is applicable, the list of tableaux obtained by its apply_all_rules(Tab,Tab2):apply_nondet_rules([or_rule,max_rule],Tab,Tab1), (Tab=Tab1 -> Tab2=Tab1 ; apply_all_rules(Tab1,Tab2)). apply_nondet_rules([],Tab,Tab1):apply_det_rules([o_rule,and_rule,unfold_rule,add_exists_rule, forall_rule,forall_plus_rule,exists_rule,min_rule],Tab,Tab1). apply_nondet_rules([H|T],Tab,Tab1):
C=..[H,Tab,L], call(C),!, member(Tab1,L),
Tab \= Tab1. apply_nondet_rules([_|T],Tab,Tab1):apply_nondet_rules(T,Tab,Tab1). application is returned by the rule predicate, a cut is performed to avoid backtracking to other rule choices and a tableau from the list is non-deterministically chosen with the member/2 predicate. If no non-deterministic rule is applicable, deterministic rules are tried sequentially with the predicate apply det rules/3, shown in Figure 5, that is called as apply det rules(RuleList, Tab,Tab1). It takes as input the list of deterministic rules and the current tableau and returns a tableau obtained by the application of one rule. After the application of a deterministic rule, a cut avoids backtracking to other possible choices for the deterministic rules. If no rule is applicable, the input tableau is returned and rule application stops, otherwise a new round of rule application is performed. In each rule application round, a rule is applied if its result is not already present apply_det_rules([],Tab,Tab). apply_det_rules([H|T],Tab,Tab1):
C=..[H,Tab,Tab1], call(C),!. apply_det_rules([_|T],Tab,Tab1):apply_det_rules(T,Tab,Tab1). in the tableau. This avoids both infinite loops in rule application and considering alternative rules when a rule is applicable. In fact, if a rule is applicable in a tableau, it will also be so in any tableaux obtained by its expansion, thus the choice of which expansion rule to apply introduces “don’t care” non-determinism. Differently, non-deterministic rules introduce in the algorithm also “don’t know” non-determinism, since a single tableau is expanded into a set of tableaux. We use Prolog search only to handle “don’t know” non-determinism. Example 4. Let us consider the knowledge base presented in Example 1 and the query Q = kevin : N atureLover. After the initialization of the tableau, TRILL can apply the → unfold rule to the individuals tom or fluffy. Suppose it selects tom. The tracing function τ becomes (in predicate logic):
τ (P et, tom) = { Cat(tom), Cat(tom) → P et(tom)} At this point TRILL applies the → CE rule to kevin, adding ¬(∃hasAnimal.P et) t N atureLover = ∀hasAnimal.(¬P et) t N atureLover to L(kevin) with the following tracing function: τ (∀hasAnimal.(¬P et) t N atureLover, kevin) = {
∃y.hasAnimal(kevin, y) ∧ P et(y) → N atureLover(kevin)} Then it applies the → t rule to kevin generating two tableaux. In this step we have a backtracking point because we have to choose which tableau to expand. In the first one TRILL adds ∀hasAnimal.(¬P et) to the label of kevin with the tracing function τ (∀hasAnimal.(¬P et), kevin) = {
∃y.hasAnimal(kevin, y) ∧ P et(y) → N atureLover(kevin)} Now it can apply the → ∀ rule to kevin. In this step it can use either tom or fluffy, supposing it selects tom the tracing function will be: τ (¬(P et), tom) = { hasAnimal(kevin, tom),
hasAnimal(kevin, tom) ∧ P et(tom) → N atureLover(kevin)} At this point this first tableau contains a clash for the individual tom, thus TRILL backtracks and expands the second tableau. The second tableau was created by applying the → CE rule that added N atureLover to the label of kevin, so the second tableau contains a clash, too. Now TRILL joins the tracing functions of the two clashes to find the following InstMinA: {hasAnimal(kevin, tom) ∧ P et(tom) → N atureLover(kevin), hasAnimal(kevin, tom), Cat(tom), Cat(tom) → P et(tom)}.
The tableau algorithm returns a single InstMinA. The computation of AllInstMinAs(Q, K) is performed by simply calling findall/3 over the tableau predicate.
Example 5. Let us consider Example 4. Once the first InstMinA is found, TRILL performs backtracking. Supposing it applies the → unfold rule to the individual fluffy instead of tom and following the same steps used in Example 4 it finds a new InstMinA: {hasAnimal(kevin, fluffy) ∧ P et(fluffy) → N atureLover(kevin), hasAnimal(kevin, fluffy), Cat(fluffy), Cat(fluffy) → P et(fluffy)}. 7
In this section, we evaluate TRILL performances when computing instantiated explanations by comparing it to BUNDLE that also solves the inst-min-a-enum problem. We consider four different knowledge bases of various complexity: the BRCA3 that models the risk factor of breast cancer, an extract of the DBPedia4 ontology that has been obtained from Wikipedia, the Biopax level 35 that models metabolic pathways and the Vicodi6 that contains information on European history. For the tests, we used the DBPedia and the Biopax KBs without ABox while for BRCA and Vicodi we used a little ABox contaning 1 individual for the first one and 19 individuals for the second one. We ran two different subclass-of queries w.r.t. the DBPedia and the Biopax datasets and two different instance-of queries w.r.t. the other KBs. For each KB, we ran each query 50 times for a total of 100 executions of the reasoners. Table 2 shows, for each ontology, the number of axioms, the average number of explanations and the average time in milliseconds that TRILL and BUNDLE took for answering the queries. In particular, in order to stress the algorithm, the BRCA and the version of DBPedia that we used contain a large number of subclass axioms between complex concepts.These preliminary tests show that TRILL performance can sometimes be better than BUNDLE, even if it lacks all the optimizations that BUNDLE inherits from Pellet. This represents evidence that a Prolog implementation of a Semantic Web tableau reasoner is feasible and that may lead to a practical system. 3 http://www2.cs.man.ac.uk/~klinovp/pronto/brc/cancer_cc.owl 4 http://dbpedia.org/ 5 http://www.biopax.org/ 6 http://www.vicodi.org/ In this paper we presented the algorithm TRILL for reasoning on SHOIN (D) knowledge bases and its Prolog implementation. The results we obtained show that Prolog is a viable language for implementing DL reasoning algorithms and that performances are comparable with those of a state of the art reasoner.
In the future we plan to apply various optimizations to TRILL in order to
better manage the expansion of the tableau. In particular, we plan to carefully
choose the rule and node application order. Moreover, we plan to exploit TRILL
for performing reasoning on probabilistic ontologies and on integration of
probabilistic logic programming with DLs and for implementing learning algorithms
for such integration, along the lines of [