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 proof 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, 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 reasoning1 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
DLs E L, ALN .
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 for the existence of subsumption relations 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.
In the next section, we recall some preliminary notions of the formalism and reasoning services we adopt. In Section 3 we shortly recall how to model the three problems in the integrated framework. Then,we describe the architecture of the prototype implementing the solving strategy in Section 4, before delving into details of subsumption program, on which the whole prototype relies, in Section 5. We show how to query the presented prototype in Section 6, and, finally, close the paper with discussions and future work. 2
adopt for knowledge representation; the reader interested in further details may consult
a reference book [
noted as Concepts Names and Role Names, respectively. Each DL allows for a different set of constructors for describing concepts. The set of constructors allowed by a DL characterizes it in terms of expressiveness and reasoning complexity: the more a DL is expressive, the harder is inferring new knowledge on its descriptions [19, Ch.3].
representation of the domain of interest, the intensional knowledge which takes the
name TBox in DL systems. By the way, in this paper we admit an empty TBox, given
that it has been shown that the presence of a TBox affects the termination of some of
the services we implement even for very simple DLs [
Constructive Description Logics [
The semantic of concept descriptions is conveyed through an Interpretation I = ( I ; I ) , where I is a non–empty set denoting the domain of I and I is an interpretation function such that: i) I maps each concept name A in a set AI I ; ii) I maps each role name R in a binary relation rI I I .
reasoning service in DL checks for specificity hierarchies, by determining whether a concept description is more specific than another one or, formally, if there is a subsumption relation between them.
Definition 1 (Subsumption). Given two concept descriptions C and D in a DL L, we say that D subsumes C if CI DI . We write C v D.
can be computed by so-called structural subsumption algorithms, i.e., algorithms that
compare the syntactic structure of (possibly normalized) concept descriptions.
Algorithms for structural subsumption in ALN have been proposed in the literature [
subsumption algorithm, which, although quite inefficient, allows for easily inverting subsumption in our Prolog implementation. 3
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, where E1, En, are concept terms in DL, such that ( ) is true (i.e., , each subsumption and non-subsumption statement in (1) is true). If is satisfiable in DL then E is called a solution for and the set of solutions for is defined as:
SOL( ) = fE = hE0; : : : ; Eni j E is a solution for g Definition 2 (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 other E 0 2 SOL( ) with E 0 E . 3.1
Non-standard Services in DLs as OSPs
Least Common Subsumer
Definition 3. [
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. @.
mation retrieval, Concept Difference [
Definition 4. [
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, in spite of its name, a Concept Difference problem may
have several solutions [
duction.
Definition 5. [
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.
[3, Prop.1]). 3.2
Optimality by Fixpoint
Definition 6 (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 by the following induction: starting from a solution E , let
E0 = E
Ei+1 = bP(Ei) for i = 0; 1; 2; : : :
vious 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. However, also when after n iterations En is not a fixpoint, En can be considered as an approximation of an optimal solution, since Ei+1 Ei for every i = 0; : : : ; n.
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.
approach to non-standard inference above recalled [
Among possible languages for prototyping, we believe that Prolog combines in a unique fashion three distinguishable advantages: 1. its built-in unification easily parses concept terms, so the implementation of a parsing module can be skipped over 2. the double nature of programs-as-predicates allows us to isolate Subsumption both as a predicate and as a DL-specific module that can be changed according to the adopted Description Logic, while keeping fixed the incremental computation, and
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 .3
http://dl.dropbox.com/u/28260263/CILC2012exe.rar.
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 special purpose lists manipulation and concepts normalization.
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. The formalization of Concept Difference and Concept Abduction problems is given in Appendix to enhance paper readability. 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).
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)).
timal Solution Problem in which we search for solutions which are optimal w.r.t. a given preorder, by incrementally trying to find solutions which are better than the one at hand, till the 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 (lines 18–20). In fact, given that L1 is represented as a Prolog list, the predicate append performs a sort of conjunction of the appended variable to L1.
We notice that, even though different clauses are needed to check if L2 is better than L1 in E L (lines 21–24) and ALN (lines 25–34), such a distinction is only due to efficiency reasons: subs aln needs two parameters more than subs el and the adoption of a logic-independent 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 5.1.
5.1
Subsumption Both in E L and in ALN , the subsumption algorithm takes as input concept descriptions written as conjunctions, formalized as Prolog lists. Given two concept descriptions C1 and C2 in a DL DL, in order to prove whether C2 subsumes C1 (formally C1 v C2), the algorithm recursively searches, for each 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.
The predicate making sumbsumption inversion possible is my member (see calls in lines 15 and 18 in E L, for example), whose code is included in support modules and shown in the following: 1 mymember(X, L):2 ground(L), !, 3 member(X, L). 4 mymember(X, [X]). 5 mymember(X, [X|L]). 6 mymember(X, [_|L]) :7 mymember(X, L).
and non-ground (lines 4–7) lists. The former case reverts to the use of built-in predicate member, which lists all members of the ground list at hand. The latter case allows for avoiding premature variables unification in membership check.
exploit syntactical features of the DL at hand to either check subsumption between ground elements or unify variables to values making subsumption true.
subsumption in E L, to make the reader aware of the overall list comparison mechanism, shared also by the corresponding implementation in ALN . For the sake of synthesis, we therefore provide only clauses related to the one-to-one comparison in the case of ALN .
after. We recall that the implemented algorithm exploits a structural characterization of subsumption, which makes the above mentioned inversion easy, despite the inherent inefficiency introduced.
alphabet of our Prolog code, are not ground), the inversion could generate the same solution and unify a variable to the same value more than once. In order to prevent such an inefficiency and redundancy source, we manage a list, which we call BL (acronym for Black List), of variables substitutions already produced by subs el clauses. Clauses in lines 20–29 succeed, in fact, when both structural subsumption holds and the involved variable unification has not been adopted before (see line 22 and line 29). Whenever a subsoneone clause succeeds, the concept associated to the variable value causing the success is added to the list BL, which thus represents our progressive solution. In particular, in line 27, it is prevented the success with variable values producing concepts subsuming BL, which are useless w.r.t. the construction of our target solution. 1 subs_el(C1, C2):2 manage_concept(C1, C1L, el), 3 manage_concept(C2, C2L, el), !, 4 subsmanymany(C1L, C2L, []). 5 subsmanymany(L1, [], _) :6 not(ground(L1)) -> putTop(L1); true. 7 subsmanymany(L1, [C|L2], BL):8 ground(C) -> ( 9 subsonemanyground(L1, C), 10 subsmanymany(L1, L2, BL)); 11 (subsonemany(L1, C, BL, BLF), 12 subsmanymany(L1, L2, BLF)). 13 subsonemany(L,A, BL, BLF):14 not(member(top, BL)), 15 mymember(B, L), 16 subsoneone(B, A, BL, BLF). 17 subsonemanyground(L,A):18 mymember(B, L), 19 subsoneoneground(B, A). 20 subsoneone(A, A, BL, BLF):21 literal(A), 22 not(member(A, BL)), 23 append([A], BL, BLF). 24 subsoneone(some(R,C1), some(R, C2N), BL, BLF):25 subs_el(C1, C2), 26 normalization_top(C2, C2N), 27 not(subs_el(BL,some(R,C2N))), 28 append([some(R,C2N)],BL,BLF) . 29 subsoneone(Any, top, [], [top]). 30 subsoneoneground(A, A):- literal(A). 31 subsoneoneground(some(R,C1), some(R, C2)):32 subs_el(C1, C2). 33 subsoneoneground(_, top). 34 putTop(L):35 term_variables(L,Vars), 36 allTop(Vars). 37 allTop(Vars) :38 Vars = [] -> true; (Vars = [top| Rest], allTop(Rest)).
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, _):
C1 = 9R.(A u B) u 9R.(C u D);
C2 = 9R.(A u C) u 9R.(B u D)
C2 = 9R.(P u Q u 9R.P u 9R.Q) C1 = (> 3 G) u (6 7 S) u 8R.(6 2 M );
C2 = (> 4 G) u (6 3 S) u 8R.U 4. L = LCS(C1; C2), DL = ALN
C1 = (> 3 G) u 8R.(6 2 M ) ;
C2 = (6 1 G) u 8R.(6 3 M ) 12 var(N), 13 integer(M), 14 integer(MaxL), 15 leqBounded(M,N,MaxL). 16 subsoneone(atmost(N,R), atmost(M, R),_, _):17 integer(N), 18 integer(M), 19 !, 20 =<(N,M). 21 subsoneone(atmost(N,R), atmost(M, R),_, MaxM):22 var(M), 23 integer(MaxM), 24 leqBounded(N, M, MaxM). 25 subsoneone(atmost(N,R), atmost(M, R),_, _):26 var(N), 27 geqpositive(M,N). 28 subsoneone(_, all(R, top), MaxL, MaxM):29 nonvar(R). 30 subsoneone(all(R,C1), all(R, C2), MaxL, MaxM):31 subsoneone(C1, C2, MaxL, MaxM). 32 subsoneone(atmost(0, R), all(R, C), _, _). 6
C2 = A u B u 9R.(C u D u 9S.(H u J )) C1 = (> 2 R) u 8R.:A u B; uC; C2 = B u (> 3 R) C2 = A u B u 9R.(9S.H)
C1 = A u B u 9R.(C u D u 9S.(H u J ));
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 )) C1 = 8R.?; C2 = 8R.(:P u P1)
C1 = 9R.(9S.H); 10. L = ABD(C1; C2), DL = ALN
C1 = (> 3 G) u 8R.(6 2 M ) ; C2 = ?
tions, like in the case of Concept Abduction and Concept Difference, the system stops searching for solutions when the first one is retrieved.
the feasibility of the proposed strategy for Least Common Subsumer, Concept Difference and Concept Abduction computation in E L and ALN .
The extension of the approach to different DL sublanguages, and the implementation, 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. In particular, by investigating on the queries execution, we noticed that the main source of complexity is due to the adoption of a generate-and-test strategy: all solutions need to be produced before discarding the not relevant ones. We therefore will investigate on how the program efficiency can be increased by designing a concurrent goal solution strategy, exploiting meta-programming.
approach to DLs for which Structural Subsumption is complete. For more expressive
gram inverting Subsumption. One possibility would be to implement the higher-order
tableaux method presented by Colucci et al. [
Concept Abduction abd(C, D, H, DL) :manage_concept(C, CM, DL), manage_concept(D, DM, DL), find_abd(CM, DM, DM, H, DL), !. find_abd(C, D, H1, H3, DL):better_abd(C, D, H1, H2, DL), !, find_abd(C, D, H2, H3, DL). find_abd(C, D, H, H, DL). better_abd( C, D, H1, H2, el):abd1(C, D, H2, el), subs_el(H1, H2),!, not(subs_el(H2, H1)). Concept Difference