We present a Logic Programming prototype implementation, working as proof-of-concept for a unified strategy proposed in our past research to solve several non-standard reasoning problems in Description Logics (DLs), denoted by Constructive Reasoning. In order to prove both the problem-independence and the logic-independence of the adopted approach, the prototype is focused on the solution of three different problems - namely Least Common Subsumer, Concept Abduction and Concept Difference - and two different, though simple and endowed with structural subsumption, DLs, i.e., EL and ALN . Accordingly to the implemented strategy, problems are formalized as conjunction of both subsumption and non-subsumption statements, causing the whole prototype to rely on a Prolog program solving subsumption. The program is built around a predicate, which on the one hand checks for the existence of subsumption relations between ground elements, providing boolean answers, and on the other hand, if inverted, exploits Prolog built-in unification to enumerate variable values making subsumption true between concept terms containing concept variables.
mation, through management strategies whose significance increases with the level of novelty introduced by provided results.
In past knowledge management literature, in fact, interest has been given to the
proposal of special purpose inferences allowing for exploiting as much as possible the
informative content achieved through knowledge representation effort. To this aim,
several non-standard reasoning services have been proposed and continue to be investigated
to cope with different representation or inference needs. The most relevant services we
may cite are explanation [
tractable, even though not very expressive, sub-languages, like E L [
for dealing with several different non-standard inferences. The framework, presented as independent of the DL adopted for knowledge representation, takes a constructive reasoning perspective on problem solving: most inferences are in the form “Find one or more concept(s) C such that fsentence involving C g“ and the proposed framework aims at building such C.
proach, we here present a prototype implementation in Logic Programming solving
Though still inefficient at this stage, the prototype works as proof-of-concept for the integrated solution framework. It exploits the property of our approach according to which most non-standard reasoning problems may be formalized as conjunction of both subsumption and non-subsumption statements and therefore relies on a Prolog program solving subsumption, built around a main predicate called either subs el or subs aln, depending on the adopted DL. In particular, we show how to invert the subs predicate (either subs el or subs aln ), so that not only it can check subsumption between ground elements (providing boolean answers), but it can also exploit Prolog built-in unification to enumerate variable values making subsumption true between concept terms containing concept variables. The approach takes a generate-and-test strategy.
integrated framework. Then,we describe the architecture of the prototype implementing the solving strategy in Section 3, before delving into details of subsumption program, on which the whole prototype relies, in Section 4. We show how to query the presented prototype in Section 5, and, finally, close the paper with discussions and future work. 2
The approach presented in our past research [
concept variables X0; X1; : : : ; Xn. We say that is satisfiable in DL iff there exists a substitution = X0 > E0; :::Xn > En such that ( ) is true (i.e., , each subsumption and non-subsumption statement in (1) is true). If is satisfiable in DL then
Definition 1 (OSP). An Optimal Solution Problem (OSP) P is a pair h ; i, where is a formula of the form (1) and is a preorder over SOL( ). A solution to P is a concept tuple E such that both E 2 SOL( ) and there is no E 0 2 SOL( ) with E 0 E . 2.1
Non-standard Services in DLs as OSPs
Least Common Subsumer
Definition 2. [
Common subsumers of C1; C2 satisfy the formula of the form (1):
LCS = (C1 v X) ^ (C2 v X) Then, the LCS problem can be expressed by the OSP LCS = h LCS ; @i. We note that > is always a solution of LCS which is a greatest element w.r.t. @.
tion retrieval, Concept Difference [
Definition 3. [
DIF F = (C v (D u X)) ^ ((D u X) v C)
Such a definition causes Concept Difference to be modeled as the OSP DIF F =
h DIF F ; Ai. We recall that, is spite of its name, a Concept Difference problem may
have several solutions [
duction.
Definition 4. [
ABD = (C u X 6v ?) ^ (C u X v D)
specific solutions should be preferred because they hypothesize the least. According to the proposed framework, we can model Subsumption-maximal Concept Abduction as ABD = h ABD; Ai. Note that a greatest—i.e., most specific—solution of ABD w.r.t.
[12, Prop.1]). 2.2
Optimality by Fixpoint
Definition 5 (Inflationary operators and fixpoints). Given an OSP P = h ; i, we say that the operator bP : SOL( ) ! SOL( ) (for better) is inflationary if for every E 2 SOL( ), it holds that bP(E ) E if E is not a least element of , bP(E ) = E otherwise. In the latter case, we say that E is a fixpoint of bP.
a fixpoint has been reached, and such a fixpoint is a solution to P. Being bP inflationary, a fixpoint is always reached—possibly in an infinite number of steps—by the following induction: starting from a solution E , let
E0 = E
Ei+1 = bP(Ei) for i = 0; 1; 2; : : : Then, there exists a limit ordinal such that E is a fixpoint of bP. For each of the previous non-standard reasoning services, we highlighted a greatest solution E 2 SOL( ) which this iteration can start from. Obviously, when is well-founded (in particular, when SOL( ) is finite) the fixpoint is reached in a finite number of steps, but the general conditions for well-foundedness of are not known, and out of the scope of this paper. However, also when after n iterations En is not a fixpoint, one can stop and consider En as an approximation of an optimal solution, since Ei+1 Ei for every i = 0; : : : ; n. In this sense, our method can be used as an anytime approximation.
a monotone operator are not applicable in this setting, first of all, because bP is not monotone, and secondly because there can be more than one minimal fixpoint: in fact, it is known that for ALN , both Concept Difference and Concept Abduction admit more than one solution.
can be solved by this method. For instance, deciding whether a formula of the form (1) is satisfiable is an open problem for ALN , to the best of our knowledge. In this paper we address particular cases of (1), corresponding to known non-standard inferences, for which a solution is always known to exist.
3
above mentioned approach to non-standard inference [
our approach: the generality and the independence of the adopted DL (within a given subset) of non-standard inferences solving strategy. In particular, the prototype here presented is devoted to the solution of three different reasoning services, namely Least Common Subsumer, Concept Difference and Concept Abduction, in E L and ALN .2
for the system of the OSP modeling the non-standard inference need at hand. It is easy to notice that, therefore, the whole approach relies on the logic rules formalizing structural subsumption, which is at the basis of each formula to be solved.
The crucial role of subsumption affects the system architecture in Figure 1, whose main components are described below: – Subs is the central component, which implements a recursive algorithm solving subsumption between concept descriptions; such a module is designed to provide one interface for each DL adopted to model the problem: the current prototype allows for solving subsumption in E L and ALN . – Problems is the component implementing OSP solving algorithms: the current prototype allows for solving Least Common Subsumer (lcs), Concept Difference (diff) and Concept Abduction (abd), but Problems may be extended to include further services. It is noteworthy how, depending on the DL adopted to model the problem, a different subsumption interface, either subs EL or subs ALN, is invoked. – Support Modules includes clauses supporting the performance of subsumption and inferences included in Problems, but related to sorts of information processing outside the core solving algorithms, such as ALN concept normalization in
2 See http://dl.dropbox.com/u/28260263/DL2012exe.rar for an executable version of the prototype. In order to show the prototype implementing the solving strategy detailed so far, we refer to Least Common Subsumer computation, solved by the Prolog code fragment in the following, excerpted from Problems module. 1 :-use_module(’subs_el’). 2 :-use_module(’subs_aln’). 3 :-use_module(’support_modules’). 4 :-use_module(’normalization’). 5 problem(lcs,C,D,Result,DL):- lcs(C,D,Result,DL). 6 problem(abd,C,D,Result,DL):- abd(C,D,Result,DL). 7 problem(diff,C,D,Result,DL):- diff(C,D,Result,DL). 8 lcs(C1, C2, LN, DL) :9 manage_concept(C1, C1N, DL), 10 manage_concept(C2, C2N, DL), 11 find_lcs(C1N, C2N, [top], L, DL), 12 normalization_top(L, LN). 13 find_lcs(C1, C2, L1, L3, DL) :14 decorate(L1, L2), 15 better_lcs(C1, C2, L1,L2, DL), !, 16 find_lcs(C1, C2, L2, L3, DL). 17 find_lcs(C1, C2, L1, L1, _). 18 decorate(C,C0):- list(C,CL),select(some(R,D),CL,Rest), 19 decorate(D,DL),append(Rest,[some(R, DL)], C0). 20 decorate(C,C0):- list(C,CL), append(CL,[X0],C0). 21 better_lcs(C1, C2, L1, L2, el):22 subs_el(C1, L2), 23 subs_el(C2, L2), 24 not(subs_el(L1, L2)). 25 better_lcs(C1, C2, L1, L2, aln):26 computeMaxAtLeast(C1,Max3), 27 computeMaxAtLeast(C2,Max4), 28 MaxL is max(Max3,Max4), 29 computeMaxAtMost(C1,Max1), 30 computeMaxAtMost(C2,Max2), 31 MaxM is max(Max1,Max2), 32 subs_aln(C1, L2, MaxL, MaxM), 33 subs_aln(C2, L2, MaxL, MaxM), 34 not(subs_aln(L1, L2, MaxL, MaxM)).
given preorder, by incrementally trying to find solutions which are better than the one at hand, till a best one is reached.
In order to compute the Least Common Subsumer LN of two concepts, C1 and C2 in a DL (see line 8), we need to incrementally construct a concept which subsumes both C1 and C2, and is optimal w.r.t. subsumption minimality (in fact, LN must be the most specific common subsumer of C1 and C2). To this aim, we start considering the trivial, subsumption maximal, solution, L1 = > (line 11) and recursively try to find (lines 13–16) better common subsumers L2 (line 15), by solving the system reported hereafter: fC1 v L2; C2 v L2; L1 6v L2g (lines 22–24 or 32–34, depending on the adopted DL). When no common subsumer Ln such that Ln 1 6v Ln exists, Ln 1 is returned as best (Least) Common Subsumer (line 17).
a predicate, namely decorate, which makes the common subsumer at hand L1 more specific by appending fresh variables to it at every nesting level(lines 18–20). We notice that, even though different clauses are needed to check if L2 is better than L1 in
reasons: subs aln needs two parameters more than subs el and the adoption of a logicindependent unique better lcs would force subs el to work less efficiently with such two parameters, even though instantiated to anonymous variables. By the way, the reader can notice that the solving strategy underlying better is shared by both characterizations.
excerpt belong to one of the imported modules. In particular, subs el and sub aln modules provide the related logic-dependent subsumption programs, listed in Section 4.1.
crucial for the problem solution, but outside the core solving algorithms.
Among the others, we underline the role of the logic-dependent predicate manage concept (see lines 9–10), which manipulates input concepts to make them ready for subsumption in the adopted DL: in the case of E L, simple list manipulation operations are performed, while in the case of ALN , such a predicate starts the process of normalization of input concepts: concepts are reduced in CCNF and both possible clashes and inherent subsumption relationships between number restrictions are identified. 4.1
Subsumption
tions written as conjunctions, formalized as Prolog lists. We recall that in ALN such
member of the list related to C2, at least one subsumed member in the list representing C1. In other words, the whole subsumption check mechanism reverts to a one-one comparison between list members (or, more appropriately, conjuncts).
showing check results. Nevertheless, we notice that conjuncts in input concept descriptions may also include concept variables: when lists are not ground, subsumption is inverted to exhibit possible variables substitutions making subsumption between list members true. The mechanism exploits Prolog built-in unification.
Subsumption in EL 1 subsoneone(A, A, BL, BLF):2 literal(A), 3 not(member(A, BL)), 4 append([A], BL, BLF). 5 subsoneone(some(R,C1), some(R, C2N), BL, BLF):6 subs_el(C1, C2), 7 normalization_top(C2, C2N), 8 not(subs_el(BL,some(R,C2N))), 9 append([some(R,C2N)],BL,BLF) . 10 subsoneone(Any, top, [], [top]). 11 subsoneoneground(A, A):- literal(A). 12 subsoneoneground(some(R,C1), some(R, C2)):13 subs_el(C1, C2). 14 subsoneoneground(_, top).
Subsumption in ALN 1 subsoneone(bottom, _ , _, _). 2 subsoneone(_, top, _, _). 3 subsoneone(A, A, _, _):- literal(A). 4 subsoneone(atleast(N,R), atleast(M, R), _, _):5 integer(N), 6 integer(M), 7 >=(N, M). 8 subsoneone(atleast(N,R), atleast(M, R),_, _):9 var(M), 10 geqpositive(N,M). 11 subsoneone(atleast(N,R), atleast(M, R), MaxL, _):
1. L = LCS(C1; C2), DL = EL
C1 = 9R.(A u B) u 9R.(C u D);
C2 = 9R.(A u C) u 9R.(B u D) 2. L = LCS(C1; C2), DL = ALN
C1 = (> 3 G) u (6 7 S) u 8R.(6 2 M);
C2 = (> 4 G) u (6 3 S) u 8R.U 3. L = DIF F (C1; C2), DL = EL
C1 = A u B u 9R.(C u D u 9S.(H u J)); C2 = A u B u 9R.(9S.H) 4. L = DIF F (C1; C2), DL = ALN
C1 = A u 8R.(B u (6 4 S)) u (6 0 T );
C2 = A u 8R.(6 4 S) u 8T .(D u 8U.E u (> 2 V )) 5. L = ABD(C1; C2), DL = EL
C1 = 9R.(9S.H);
C2 = A u B u 9R.(C u D u 9S.(H u J)) 6. L = ABD(C1; C2), DL = ALN
C1 = (> 2 R) u 8R.:A u B; uC;
C2 = B u (> 3 R)
when the first one is retrieved. As pointed out since the introduction, our prototype is still inefficient at this stage: all results in Table 1 need a few seconds to be returned, and Query 4, which is the most complex one, asks for about 10 seconds.3 6
the feasibility of the proposed strategy for Least Common Subsumer, Concept Difference and Concept Abduction computation in E L and ALN .
tion, for each investigated DL, of further non-standard reasoning services in the prototype is part of our future work, together with the improvement of system efficiency.
tural subsumption is complete. For more expressive DLs, the fixpoint mechanism could still be exploited, but using some higher-order tableaux methods that are still to be defined and whose correctness and termination should be proved.