ASP Based Generation of Information Terms for Constructive E L

Abstract

Constructive description logics define interpretations of description logics under different constructive semantics. These logics have been mostly studied from the point of view of their formal properties: limited practical approaches have been shown for their use in knowledge representation and Semantic Web languages and tools (which, on the other hand, constitute the distinctive applications of description logics). In this paper we demonstrate a solution to address this aspect: from the theoretical point of view, we first introduce an information terms semantics for the minimal description logic E L and we establish formal results linking this constructive semantics to answer set semantics. Using these results, on the practical side, we then present a prototype managing one aspect of such semantics (the generation of information terms of a knowledge base) using OWL-EL ontologies and “off the shelf” tools.

Constructive description logics define interpretations of description logics under con

structive semantics. The need for such reinterpretation of description logics in nonclassical semantics mostly arises for the interest in applying the formal properties of these semantics to solve modelling or reasoning problems. Starting from different representation interests and reference constructive semantics, several constructive characterizations of description logics have been recently proposed, like e.g. [ 6,11,19,22 ].

However, constructive description logics have been mostly studied from the point of

view of their formal properties, but limited practical approaches have been shown for their application to knowledge representation and Semantic Web languages and tools (which, on the other hand, constitute the distinctive application of description logics).

Among the “real world” use of constructive description logics in applications and systems, for example, we can cite reasoning over incomplete data streams [18], managing conflicts over legal ontologies [15], and a framework for the composition of semantic services in heterogeneous domains [16] (based on [5]).

In this paper we want to demonstrate a direction for the solution of this aspect: from

the theoretical point of view, we introduce a minimal constructive description logic based on E L [ 2 ] and we extend to its semantics formal results linking it to Answer

Set Programming (ASP); on the practical side, by taking advantage of these properties,

we present a prototype managing one task over the constructive semantics (namely, the generation of valid “snapshots” of a knowledge base) over (a subset of) the standard

OWL-EL profile [21] and “off the shelf” tools for ontology management (OWL API) and Answer Set Programming (DLV solver).

In particular, in our work we chose to concentrate on the description logic E L be

cause, on one hand, it is one of the simplest description logics over which semantics enjoying constructive properties can be defined (cfr. explicit definability property [ 11 ]).

On the other hand, E L is recognized as one of the reference languages for (low com

plexity) description logics and, as such, it is at the base of the OWL-EL profile [ 21 ] and languages of well-known large ontologies (e.g. Gene Ontology1 and GALEN2).

The task we consider in this work regards the generation of valid information terms for a given knowledge base. Intuitively, in our semantics information terms are mathematical objects providing a constructive justification for the truth of a formula. Notably, they can be seen as representing the state of such formula: thus, in this light, generating information terms for a knowledge base correspond to validate its representations by generating a set of its possible valid states. This approach was used in the CooML modelling language [ 23 ] and related works for the generation of valid “snapshots” of information systems descriptions [ 12,14 ]: we will follow the direction of these works (in particular the relations to ASP studied in [ 13 ]) to formulate our solution. Related to this task is the algorithm GENIT used in [ 7 ] to generate states and validate the output of actions over constructive ALC.

As mentioned, the solution we propose is based on the relations across information

terms semantics and answer sets semantics: we note that this allow us, for the first time, to examine these relations also in the context of constructive description logics. We can summarize the contributions of this paper as follows: – We introduce (in Section 2) an information terms semantics for the minimal description logic E L [ 2 ]. This constructive semantics is a straightforward restriction of the basic constructive description logic BCDL [ 11 ] to the syntax of E L. – On the base of the relations across information terms semantics and answer sets for nested expressions highlighted in [ 13 ], we provide (in Section 3) results establishing a formal relation between answer sets for formulas in E L and for their information terms. In Section 4, these properties are used to formulate a datalog rewriting for the generation of the sets of information terms of an input E L knowledge base – Using these formal results, in Section 5 we present Asp-it3, a prototype implementation of an information terms generator for ontologies in OWL-EL. Asp-it applies the presented datalog rewriting to the input ontology: the computation of answer sets is obtained by interacting with the DLV solver and the resulting information terms are returned as an annotation to the OWL axioms in the original ontology.

1 http://geneontology.org/ 2 http://www.opengalen.org/ 3 https://github.com/dkmfbk/asp-it

E Lc: a constructive semantics for E L

In this section we present a constructive semantics based on the minimal description

logic E L [ 2 ]. We will refer to this logic as E Lc: the presentation and information terms semantics of E Lc are defined as a straightforward restriction of the logic BCDL [ 11 ].

Syntax. The language L for E Lc is based on the disjoint denumerable sets NR of role

names, NC of concept names and NI of individual names.

Differently with respect to standard presentations of description logics, in L we consider a set NG of special concepts, called generators, where NG \ NC = ;. Generators are used in the definition of a limited form of subsumption, which facilitates the characterization of the logic in a constructive semantics. A generator G is an atomic concept with associated a finite set of individual names DOM(G) (the domain of G) which fixes the interpretation of G. In our language, we use bounded quantified formulas of the kind 8GC, meaning that every element of DOM(G) belongs to the concept C. Also, differently from the usual presentation of E L, we limit the use of the > constructor as a special kind of generator >N 2 NG such that DOM(>N ) = N and for all generators

G, DOM(G) N . In the language L for E Lc, concepts C are expressions of the kind:

C ::= A j C u C j 9R:C

K ::= R(s; t) j C(t) j 8GC where A 2 NC [ NG and R 2 NR. Let VAR be a denumerable set of individual variables, the formulas K of L are defined as: where s; t 2 NI [ VAR, R 2 NR, G 2 NG and C is a concept. A formula is atomic if it is of the kind A(t) with A 2 NC [ NG or R(s; t). A formula is closed if it does not contain variables.

A theory K (namely, a knowledge base) can be divided as usual in TBox and ABox.

An ABox is a finite set of closed formulas of the kind C(d) and R(c; d) with R 2 NR,

c; d 2 NI and C a concept. A TBox is a finite set of formulas of the kind 8GC (i.e. “restricted” concept inclusions).

In the following we refer to languages LN restricted to subsets N of NI. Given N

NI, let NGN be the set of generators G 2 NG s.t. DOM(G) N with DOM(>N ) = N .

We denote with LN the language built on the set N of individual names, the set NC of

concept names, the set NR of role names and the set NGN of generators.

Classical semantics. A model M for LN is a pair h M; Mi, where the domain M

is a non-empty set and M is a valuation map such that: for every c 2 N , cM 2 M; for every C 2 NC, CM M; for every R 2 NR, RM M M; for every G 2 NGN , if DOM(G) = fc1; : : : ; cng, then GM = fc1M; : : : ; cnMg. Classical interpretation of non-atomic concepts is defined by the evaluation of description logics operators: (C1 u C2)M = C1M \ C2M (9R:C)M = fc 2

M j there exists d 2 M s.t. (c; d) 2 RM and d 2 CMg

An assignment on M is a map : VAR ! M. If t 2 NI [ VAR, tM; is the element of M denoting t in M w.r.t. , namely: tM; = (t) if t 2 VAR and tM; = tM if t 2 NI. A formula K is valid in M w.r.t. , and we write M; j= K, if one of the following conditions holds:

M j= R(s; t) iff (sM; ; tM; ) 2 RM

M j= C(t) iff tM; M j= 8GC iff GM If is a set of formulas, M j= means that M j= K for every K 2 . K is a logical consequence of , and we write j= K iff, for every M, M j= implies M j= K.

As noted in [11], while non-conventional in description logics languages, the provided definition of generators with a fixed domain simplifies the following presentations of the logic: alternatively, domain of generators can be defined by extending the language with nominals.

Example 1. We build our running example over the one presented in [ 3,11 ]. In this example, inspired to the classical example of [ 8 ], we want to describe the correct pairings between food and wines using an E Lc knowledge base KW . The TBox of KW contains: (Ax1) 8F ood9goesW ith:Color (Ax2) 8Color9isColorOf:W ine with W ine 2 NC, isColorOf; goesW ith 2 NR and F ood; Color 2 NG. Intuitively, axiom (Ax1) states that each F ood has an appropriate wine Color and (Ax2) defines that there exists a W ine for every Color. Domains of the generators are defined as: DOM(F ood) = ff ish; meatg

DOM(Color) = fred; whiteg

The ABox of KW contains the following assertions:

W ine(barolo) W ine(chardonnay) isColorOf (red; barolo) isColorOf (white; chardonnay) goesW ith(f ish; white) goesW ith(meat; red)

We implicitly consider as the finite set N of individual names the set containing all the

individual names used in KW .

A (classical) model M for KW must interpret F oodM = ff ishM; meatMg and ColorM = fredM; whiteMg. Note that, by the interpretation of ABox assertions, baroloM and chardonnayM belong to W ineM, but since it is not a generator, W ineM might contain other domain elements. 3 Information terms semantics. The constructive semantics for E Lc is based on the notion of information term [ 20 ]. Information terms semantics is related to the BHK (Brower-Heyting-Kolmogorov) interpretation of logical connectives [ 26 ]: intuitively, an information term for a formula K is a syntactical object that constructively justifies the truth of K in a classical model M. For example, the validity of the formula 9R:C(a) in a model M can be explained by an information term (b; ) providing the filler b s.t. (aM; bM) 2 RM and, inductively, an information term justifying bM 2 CM.

Given a finite subset N of NI and a closed formula K of LN , we define the set of

information terms ITN (K) by induction on K as follows.

ITN (K) = f tt g; if K is an atomic formula ITN (C1 u C2(c)) = f ( ; ) j 2 ITN (C1(c)) and 2 ITN (C2(c)) g ITN (9R:C(c)) = f (d; ) j d 2 N and 2 ITN (C(d)) g

ITN (8GC) = f : DOM(G) ! Sd2DOM(G)ITN (C(d)) j (d) 2 ITN (C(d)) g

The justification of formulas in classical models with respect to one of their in

formation terms is given by the realizability relation. Let M be a model for LN , K a closed formula of LN and 2 ITN (K). We define the realizability relation M h i K by induction on the structure of K.

M

htti K iff M j= K; where K is an atomic formula M h( ; )i C1 u C2(c) iff M h i C1(c) and M h i C2(c) M h(d; )i 9R:C(c) iff M j= R(c; d) and M h i C(d) M h i 8GC iff, for every d 2 DOM(G), M h (d)i C(d)

If is a finite set of closed formulas fK1; : : : ; Kng of LN , ITN ( ) denotes the set of n-tuples = ( 1; : : : ; n) such that, for every j 2 f1; : : : ; ng, j 2 ITN (Kj ). We write M h i iff, for every j 2 f1; : : : ; ng, M h j i Kj .

Example 2. Let us consider the example knowledge base KW and the axiom (Ax1)

in its TBox: every element 2 ITN (Ax1) is a function mapping each food f 2

DOM(F ood) to an information term (f ) 2 ITN (9goesW ith:Color). Thus, every

(f ) has the form (c; tt), meaning that c is a Color that is admitted for f . For example, we can consider 1 2 ITN (Ax1) defined as:

[ f ish 7! (white; tt); meat 7! (red; tt) ] It is easy to see that if M is a model for the ABox of KW , then M if we consider 2 2 ITN (Ax2) where h 1i Ax1. Similarly, [ red 7! (barolo; tt); white 7! (chardonnay; tt) ] we have that M h 2i Ax2. 3

The following result, provable by induction on the structure of K, shows the relation

across the classical and constructive semantics.

Proposition 1. Let N be a finite subset of NI, K a closed formula of LN and ITN (K). For every model M, M h i K implies M j= K. 2 tu

Thus, the constructive semantics is compatible with the classical one: a consequence of this is that the constructive semantics maintains the classical declarative reading of DL formulas.

Such definition of constructive realization leads to a constructive version of the log

ical consequence relation, that we call constructive consequence. Given a set of closed formulas [ fKg 2 LN , we say that K is a constructive consequence of (denoted j=c K) iff, for every 2 ITN ( ), there exists a 2 ITN (K) such that for every model

M for LN , M h i implies M h i K.

One important aspect (deeper investigated in [ 3,11 ]) is that such relation j=c K implicitly defines a semantic map N transforming information terms in ITN ( ) to information terms of ITN (K) such that if M h i , then M h N ( )i K. This idea is strongly related to the proofs-as-programs paradigm: in BCDL it is shown how it is possible to extract this map from the proofs of a natural deduction calculus which is sound and complete w.r.t. constructive consequence.

Our interest in the remainder of the paper is somewhat preliminary to this step:

we want to be able to compute the information terms of a set of input E L formulas (corresponding to the input knowledge base) by means of the relations between answer sets semantics and information terms semantics. 3

Answer sets semantics for formulas and information terms

In this section we build on the work in [13], which investigates the relations between information terms and answer set semantics of logic programs with nested expressions, and we reinterpret it in our scenario.

Given the definition of formulas and information terms given above, we can give a

characterization of the “snapshot” of a formula defined by one of its information terms with the definition of piece of information. We call piece of information over LN an expression of the kind h iK with K 2 LN a closed formula and 2 ITN (K).

Following the construction in [13], we adapt the definitions for logic programs with

nested expressions [ 17 ] to the structure and reading of E Lc formulas. In this regard, we call lp-intepretation I any set of closed atomic formulas. Given a closed formula K 2 LN , the usual satisfiability relation I j= K can naturally be defined as: I j= K; iff K 2 I and K is atomic I j= C u D(c) iff I j= C(c) and I j= D(c) I j= 9R:C(c) iff R(c; d) 2 I for d 2 N and I j= C(d) I j= 8GC iff for every e 2 DOM(G); I j= C(e) I j=

iff I j= K for K 2

Clearly, this is consistent with the definition of classical logical consequence. We can define as follows the notion of answer set for our formulas:

Definition 1. An lp-interpretation I is an answer set for a set of closed formulas LN iff I j= and, for every I0 I, I0 j= implies I0 = I.

Given this definition of answer set on E Lc closed formulas, in the following we want to extend this notion to the pieces of information. The idea is to denote the set of “answers” that one can derive from the contents of informations terms on the given formula. As noted in [ 13 ], the formula represents intuitively a “query” for the information terms that realize it in an interpretation: for example, asking “9R:A(c)?” corresponds to asking for an information term (d; ) for the formula such that R(c; d) holds and is an answer satisfying A(d). Given a piece of information h iK, the following defines the sets of answers ans(h iK) obtainable from it:

ans(httiK) = fKg; with K an atomic formula ans(h( ; )iA1 u A2(c)) = ans(h iA1(c)) [ ans(h iA2(c)) ans(h(d; )i9R:A(c)) = fR(c; d)g [ ans(h iA(d))

ans(h i8GA) = Sd2DOM(G) ans(h (d)iA(d)) We remark that ans(h iK) is a finite set of atomic formulas4.

Example 3. If we recall the information term of answers for h 1iAx1 we have that:

1 2 ITN (Ax1), by the definition of sets

ans(h 1iAx1) = ans(h 1(f ish)i H1(f ish)) [ ans(h 1(meat)i H1(meat)) = ans(httiColor(white)) [ fgoesW ith(f ish; white)g [

ans(httiColor(red)) [ fgoesW ith(meat; red)g = fColor(white); goesW ith(f ish; white);

Color(red); goesW ith(meat; red)g where we abbreviate H1 = 9goesW ith:Color. Similarly, considering 2 2 ITN (Ax2) from previous example: ans(h 2iAx2) = fW ine(barolo); isColorOf (red; barolo);

W ine(chardonnay); isColorOf (white; chardonnay)g

We can show the following relation to lp-interpretations (by an easy induction on the structure of formulas):

Theorem 1. Let N be a finite subset of NI, K a closed formula of LN . For every lpinterpretation I, I j= K iff there exists an information term 2 ITN (K) such that I j= ans(h iK). tu

Moreover, we can connect this notion of set of atomic answers to the realizability rela

tion with the following theorem. By induction on the structure of K, we have: Theorem 2. Let N be a finite subset of NI, K a closed formula of LN . For every model M, M h i K iff M j= ans(h iK). tu

Note that this result reduces the problem of determining the realizability of a piece of

information to the classical satisfiability of a finite set of atomic formulas.

Now we can study the relations between answer sets for E Lc formulas and pieces of

information. Intuitively, ans(h iK) represents the information needed to get evidence for K according to the information term : we want to define a set that describes the minimal knowledge needed to justify the realizability of its piece of information.

We say that an lp-interpretation I is a minimal model of h iK if, for every model M

of LN , I is the subset minimal lp-interpretation such that M j= I implies M h i K.

Using previous results, in one direction we can show:

Theorem 3. If I is an answer set for a closed formula K 2 LN , then there exists a piece of information h iK, with 2 ITN (K), such that I is a minimal model of h iK. Proof. Since I is an answer set for K, we have that I j= K and by Theorem 1 there exists 2 ITN (K) s.t. I j= ans(h iK). By Theorem 2, for each M j= I this implies M h i K. We can prove that I is minimal: suppose that I0 I s.t. I0 j= ans(h iK), then by Theorem 1, I0 j= K. Since I is an answer set for K, then I0 = I. tu 4 This definition of answer sets for pieces of information corresponds to the notion of information content used in [ 7,14 ]. Definition 2. Let K be a closed formula of LN . A piece of information h iK is minimal iff there is no 0 2 ITN (K) such that ans(h 0iK) ans(h iK).

Intuitively, the answers ans(h iK) of minimal pieces of information characterize the

sets of atoms whose truth is strictly necessary to get evidence for K. Using this definition, we can then prove the other direction of the relation: Theorem 4. Let K be a closed formula of LN and h iK be a minimal piece of information for K. Then, ans(h iK) is an answer set for K.

Proof. By Theorem 1, for every lp-interpretation I s.t. I j= ans(h iK) (that is, every I s.t. ans(h iK) I, given that it is a set of atomic formulas) we have I j= K. Hence, considering I = ans(h iK), also ans(h iK) j= K.

Moreover, let us consider I0 ans(h iK) with I0 j= K. Then, by Theorem 1, there exists a 2 ITN (K) s.t. I0 j= ans(h iK). Thus, ans(h iK) I0 and, for the minimality of h iK, this implies that ans(h iK) = I0 = ans(h iK). tu

Thus, we can complete these results with the following theorem:

Theorem 5. Let K be a closed formula of LN . I is an answer set for K iff there exists a minimal piece of information h iK such that I = ans(h iK).

Proof. By Theorem 4 we directly have the “only-if” direction: if h iK is a minimal

piece of information, I = ans(h iK) is an answer set for K.

In the other direction, by Theorem 3 if I is an answer set for K, then there exists

h iK s.t. I is a minimal model for h iK. Thus, by Theorem 2, I j= ans(h iK) which implies that ans(h iK) = I (since I is the minimal set of atoms s.t. I j= K).

We can show that h iK is a minimal piece of information: let us suppose that there exists a 2 ITN (K) such that ans(h iK) ans(h iK). Thus, ans(h iK) I and, for the minimality of the answer set I, we have ans(h iK) = I = ans(h iK). tu

4

ASP based generation of information terms From the results of previous section, one solution to generate (minimal) information terms consists in computing the answer sets of the input set of formulas and then, for each formula K, use the recursive definition of ans(h iK) to reconstruct each information term . The computation of answer sets can be achieved by translating the initial knowledge base to a datalog program, for instance by applying transformations of formulas to datalog facts and rules akin to the ones used for the translation of nested expressions (see e.g. [ 24 ]).

In the following we provide a similar translation, but we also include a set of rules

that keep track and recursively compose the information terms for the input formulas.

The datalog rewriting we propose basically follows a generate-and-test approach: a

first rewriting (P1) of the input E L knowledge base translate the formulas by using their logical reading, in order to generate all the alternative interpretations that satisfies them; the second part (P2) of the rewriting, adds rules to reconstruct from these all the possible information terms of input formulas. Thus, while P1 is related to the definition of interpretation for each formula K, P2 corresponds to the definition of ans(h iK).

In the following, we assume the usual definitions for normal logic programs under

answer set semantics (see e.g. [ 10 ] for an introduction). Note, however, that in the formulation of rules (and in their implementation) we used the DLV notation for complex list terms: thus considerations about management of complex and function terms and finiteness of the domain apply (see e.g. [ 9 ]).

In this version of the rewriting, we consider the case in which knowledge about

roles is complete: in other words, we only consider roles assertions that are included in the input set of formulas. Formally, given a finite subset N 2 NI, we consider subsets R of the set RN = fR(c; d) j R 2 NR and c; d 2 N g of role assertions over N . As proposed in [ 24 ] for the translation of nested expressions, we use a labelling of concepts to decompose complex formulas. Considering a finite set L of constants, we call lC 2 L the label encoding the (possibly complex) concept C.

Let R be a finite subset of RN . Given an input set of closed formulas of LN with

R , for each formula K 2 , the model generating rewriting P1(K) is defined as:

A(b) 7! f is(b; A)

is(b; lA): g

R(a; b) 7! f rel(a; R; b): g C u D(a) 7! f is(a; lC ) is(a; lD) is(a; lCuD): is(a; lCuD): g [ P1(C(a)) [ P1(D(a)) 9R:C(a) 7! f is(x; lC )

rel(a; R; x); is(a; l9R:C ): g [ P1(C(x)) 8GC 7! f is(x; lC )

is(x; G): g [ P1(C(x)) where A 2 NC [ NG, C; D are possibly complex concepts, R 2 NR, a; b 2 NI (or variables) and x is a variable. For each (possibly complex) concept assertion C(d) 2 , we add in P1( ) its “labelled” fact L(C(d)) = f is(d; lC ): g. Moreover, we assume that for each generator G used in , with DOM(G) = fc1; : : : ; cng, the facts f is(c1; G):; : : : ; is(cn; G): g are added to P1( ).

The IT generating rewriting P2(K), for each K 2 is defined as follows:

A(b) 7! f is it(tt; b; lA)

is(b; A): g R(a; b) 7! f rel it(tt; a; R; b)

rel(a; R; b): g C u D(a) 7! f is it([x; y]; a; lCuD)

is it(x; a; lC ); is it(y; a; lD): g [ P2(C(a)) [ P2(D(a)) 9R:C(a) 7! f is it([x; y]; a; l9R:C )

rel it(tt; a; R; x); is it(y; x; lC ): g [ P2(C(x)) 8GC 7! f isa it([x; y]; G; lC )

is(x; G); is it(y; x; lC ): g [ P2(C(x)) where A 2 NC [ NG, C and D are concepts, R 2 NR, a; b 2 NI (or variables) and x; y are variables. Note that this encoding is consistent with the vision of formulas as “queries” and uses the definition of ans(h iK) to solve the problem for bindings of a “variable” . The complete rewriting for is obtained as P ( ) = P1( ) [ P2( ).

Example 4. Let us consider again our example knowledge base KW and suppose that we add a new wine teroldego to KW , by adding the ABox assertions:

W ine(teroldego)

isColorOf (red; teroldego) Now, by applying the rewritings to KW , we want to compute all possible alternative combinations of food and wines. We assume that R coincides to the set of role assertions in the ABox of KW . By applying the model generating rewriting P1 to KW , it is easy to check that an answer set for P1(KW ) contains the set of facts (derived from the rewriting of the ABox and domains of the generators): fis(f ish; F ood); is(meat; F ood); is(red; Color); is(white; Color) is(chardonnay; W ine); is(barolo; W ine); is(teroldego; W ine);

rel(f ish; goesW ith; white); rel(meat; goesW ith; red); rel(white; isColorOf; chardonnay); rel(red; isColorOf; barolo);

rel(red; isColorOf; teroldego)g By applying the IT generating rewriting P2 to the axiom (Ax2) we obtain the rules: isa it([x; y]; Color; lH2 ) is it([x; y]; z; lH2 ) is it(tt; x; lW ine) is(x; Color); is it(y; x; lH2 ): rel(tt; z; isColorOf; x); is it(y; x; lW ine): is(x; W ine): where H2 = 9isColorOf:W ine. Intuitively, by applying these rules to the model computed for P1(KW ), we obtain this set of substitutions for the first term of the derived isa it facts: [white; [chardonnay; tt]]; [red; [barolo; tt]]; [red; [teroldego; tt]].

These correspond to two functions mapping each color to the alternative wines: the first

equals 2 from previous examples, the second is [white 7! (chardonnay; tt); red 7! (teroldego; tt)]. Similarly, the application of the rewriting for (Ax2) produces the previously presented function 2.

Moreover, we can consider the following axiom that combines (Ax1) and (Ax2): (Ax3) 8F ood9goesW ith:(Color u 9isColorOf:W ine) One can verify that, by applying P2(Ax3) to the presented model, its computed information terms provide all the alternative associations between food and wines: [ f ish 7! (white; (tt; (chardonnay; tt))); meat 7! (red; (tt; (barolo; tt))) ] [ f ish 7! (white; (tt; (chardonnay; tt))); meat 7! (red; (tt; (teroldego; tt))) ] 3

We can provide a notion of correctness for these rewritings by the following results. By

the definition of P1 and the definition of lp-interpretations, we can prove: Lemma 1. Given a closed formula K 2 LN and an answer set I for P1( ): (i). if K = C(a) and I j= is(a; lC ), then there exists an lp-interpretation I0 for s.t. I0 j= K. (ii). if K = R(a; b) and I j= rel(a; R; b), then there exists an lp-interpretation I0 for s.t. I0 j= K.

Proof (Sketch). Point (ii). follows immediately considering that the fact rel(a; R; b) is

added in P1( ) only if R(a; b) 2 .

Point (i). can be shown by induction on the definition of the rules of P1. If the fact is(a; lC ): is present in P1( ), then it has been added by the labelling and C(a) 2 . Thus in every lp-interpretation I0 for it holds that I0 j= K. Otherwise, is(a; lC ) 2 I has been added in the application of a rule in P1( ) relative to a complex concept B or to a formula 8GC.

If B = C u D, then is(a; LCuD) 2 I and, by induction, there exists an lpintepretation I0 of such that I0 j= C u D(a). By definition, this implies I0 j= C(a).

If B = 9R:C, then rel(c; R; a) 2 I and is(c; l9R:C ) 2 I. The first implies that

R(c; a) 2 R. The second, by induction, implies that there exists an lp-interpretation I0 of such that I0 j= 9R:C(c) with I0 j= R(c; a). For the definition of lp-interpretations, one of the admissible interpretations I00 for 9R:C(c) is the one in which I00 j= R(c; a) and I00 j= C(a). Thus, if I0 = I00, then I0 j= C(a).

If is(a; lC ) 2 I has been added by a rule relative to 8GC, by definition I j= is(a; G) and a 2 DOM(G) with 8GC 2 . If I0 is an lp-interpretation of , then I0 j= 8GC and thus, for every d 2 DOM(G), I0 j= C(d). Hence, I0 j= C(a). tu

Given an lp-interpretation I for P ( ) and a closed formula K 2 LN , we define

IT (K; I) as the set of information terms “returned” by P2 as follows: – If K = C(a), let IT (C(a); I) = f j I j= is it( ; a; lC )g. – If K = R(a; b), let IT (R(a; b); I) = tt iff I j= rel it(tt; a; R; b). – If K = 8GC, let D = fc j I j= isa it([c; ]; G; lC )g: – if D = DOM(G), let:

IT (8GC; I) = f j (c) =

for c 2 DOM(G) and I j= isa it([c; ]; G; lC )g; – otherwise, IT (8GC; I) = ;.

Then, with respect to the reconstruction of information terms we can show, using the

definition of P2 and ans(h iK): Theorem 6. Let LN be an input set of closed formulas with R formula of LN , and I be the (unique) answer set for P ( ).

If 2 IT (K; I), then there exists an lp-interpetation I0 for , K a closed s.t. ans(h iK)

I0

Proof. We can show by induction on the structure of K that ans(h iK) I0.

If K = R(a; b), then P2(R(a; b)) = frel it(tt; a; R; b) rel(a; R; b):g and I j= rel it(tt; a; R; b) only if I j= rel(a; R; b):, which by P1 implies that R(a; b) 2 R with R . Thus for every lp-interpretation s.t. I0 j= , also fKg = ans(h iK) I0.

If K = A(c) with A 2 NC[NG and tt 2 IT (K; I), by the definition of P2, we have that I j= is(c; A). Thus for Lemma 1 and the definition of P1, I j= is(c; lA) and there exists an lp-interpretation I0 for s.t. A(c) 2 I0. This implies that ans(h iK) I0.

If K = C u D(c) and ( ; ) 2 IT (K; I), by the definition of P2, we have that I j= is it( ; c; lC ) and I j= is it( ; c; lD). Thus, for induction hypothesis, there exist

I1; I2 interpretations of s.t. ans(h iC(c)) I1 and ans(h iD(c)) I2. Thus

ans(h( ; )iK) I1 [ I2.

If K = 9R:D(c) and (d; ) 2 IT (K; I), by the definition of P2, we have that rel it(tt; a; R; d); is it( ; d; lC ) 2 I. By the definition of P2, the first implies that

R(a; d) 2 R and, by induction hypothesis, there exists an lp-interpretation for

ans(h iD(c)) I0. This implies that ans(h(d; )iK) I0.

If K = 8GC and 2 IT (K; I), by P2 we have that, for every c 2 DOM(G), (c) = and isa it([c; ]; G; lC ) 2 I. This means that is it( ; c; lC ) 2 I. By induction hypothesis, there exists Ic lp-interpretation of s.t. ans(h iC(c)) Ic. Thus, considering the lp-interpretation IG = Sc2DOM(G) Ic, we have ans(h iK) IG. tu We remark that an answer set for P1( ) does not coincides, in general, to an answer set for as defined in Section 3. Basically, the difference lies in the generation of fillers for existential formulas: for a formula 9R:C(a), while an answer set for “chooses” one of the possible b 2 N such that R(a; b) and C(b) are verified, the approach of P1 is to generate in its model all such possible alternatives of the fillers. If we want to be more faithful to the first interpretation, one option would be to generate a model for each filler alternative by adding in the translation of existential formulas K = 9R:C(a) disjunctive rules of the kind: f illsK (x) _ :f illsK (x) is(x; lC ) f illsK (x):

rel(a; R; x): f illsK (x); f illsK (y); y 6= x:

It is easy to see, however, that this generation approach leads to a “combinatorial ex

plosion” of the number of the models, as one has to consider all admitted combinations of fillers for each existential formula. Similar considerations can be given if, moreover, one does not want to restrict to a fixed input R RN but aims at computing all possible b 2 N satisfying rel(a; R; x). In this regard, connections of such generation with existential extensions of datalog [ 1 ] can be studied.

Note that the two rewritings P1 and P2 can be also used separately. For example, we might only apply the IT generating rewriting P2 if we are interested in verifying that the input knowledge base contains all the necessary “constructive information” needed to justify (i.e. compute an information term for) every input axiom5. 5

Asp-it prototype

The datalog translation presented in previous section has been implemented in a prototype, called Asp-it. Basically, the Asp-it prototype takes as input an OWL-EL ontology and, by using the presented datalog rewritings, outputs the ontology annotated with the information terms computed for each of its axioms.

Asp-it is implemented as a Java-based command line application: it accepts as input

an OWL-EL ontology (using the presented E L fragment), which corresponds to the input set of formulas of the presented rewritings; Asp-it produces as output the same

OWL ontology in which all logical axioms are annotated with the derived information terms using an OWL annotation property elc:hasIT; optionally, Asp-it can save to file the datalog rewriting used in the computation.

5 This basically corresponds to the role of the GENIT algorithm in [ 7 ].

Thus, information terms in the output ontology take the form of string RDF literals

and are structured as the list terms generated by the P2 rewriting (like, e.g. "[meat,[red,tt]]"). The newly added elc:hasIT annotation property is defined in a support schema file imported in the rewriting.

The structure of Asp-it has been realized mostly around our previous work on

CKRew6, a datalog rewriter for Contextualized Knowledge Repositories [ 4 ]. The loading and saving of OWL ontology files is managed using the OWL API7. Computation of models for the datalog rewritings is managed using an external call to the DLV solver8, by means of the DLVWrapper Java library [ 25 ].

The information terms generation process of Asp-it is shown in Figure 1. First of all,

Input ontology Γ

Rewrite

P(Γ)

Retrieve Info.Terms

Annotate hasIT DLV system

Datalog rewriting P(Γ) Output ontology Γ' the input OWL-EL ontology is loaded using the methods of the OWL API. Then the rewriting takes place, building up the datalog program associated to the input knowledge base: for each of the OWL logical axioms in , their structure is recursively traversed by the rewriting methods and the corresponding rules of P1 and P2 are added to the program. Next, the program is submitted to the DLV solver to compute its answer sets: the output models are then filtered to retrieve the terms corresponding to information terms of the input axioms (equivalent to the IT (K; I) set from Section 4).

The information terms elc:hasIT annotations are then written to the output ontol

ogy by means of the OWL API. Finally, the output ontology 0 (and, if requested, the computed datalog program) is saved to file.

Asp-it is distributed as an open source software at https://github.com/ dkmfbk/asp-it. The latest binary release of Asp-it can be downloaded at https: //dkm.fbk.eu/resources/asp-it/asp-it.zip. The binary package contains (in the folder demo) example files implementing the “food and wines” running example.

6 http://ckrew.fbk.eu/ 7 http://owlcs.github.io/owlapi/ 8 http://www.dlvsystem.com/dlv/

Conclusions and future works In this paper, our interest was to demonstrate a practical approach to the realization of semantics for constructive description logics (and the application of their formal properties) on the base of Semantic Web languages and tools. We first introduced a minimal constructive description logic E Lc based on the language of E L. Then, we extended to this interpretation results linking its information terms semantics to answer set semantics: on these bases, we proposed a datalog rewriting aimed at the computation of information terms of an input E Lc knowledge base. Finally, we have developed an open source tool implementing this computation, using well-known tools for the management of OWL ontologies and answer set programming. We remark that, while demonstrative from an applicative point of view, this exercise also lead to a first study of the relations of constructive semantics for description logics with answer set programming.

Of course, the presented work and prototype only represent a first step towards the

use of constructive description logics in practical applications on Semantic Web data.

As noted in previous sections, one fundamental direction would be to develop and inte

grate in current work procedures that are able to manipulate the computed information terms. In this regard, for example, it will be interesting to study the applicability of this work in conjunction to the Semantic Web service composition calculus based on

BCDL presented in [5]. From a formal point of view, a prosecution of this work should

involve the study of the expandability of the presented results and rewritings to more expressive description logics. For example, one direction would be to extend the results to the language of ALC, thus aiming at the full BCDL logic. Another direction would be to broaden the language in the E L family towards SROE L, corresponding to the full language of OWL-EL.

References

1. Alviano , M. , Faber , W. , Leone , N. , Manna , M. : Disjunctive datalog with existential quantifiers: Semantics, decidability, and complexity issues . TPLP 12 ( 4-5 ), 701 - 718 ( 2012 )

2. Baader , F. : Terminological cycles in a description logic with existential restrictions . In: IJCAI-03 . pp. 325 - 330 . Morgan Kaufmann ( 2003 )

3. Bozzato , L. , Ferrari , M. , Fiorentini , C. , Fiorino , G.: A constructive semantics for ALC . In: DL2007. CEUR-WP , vol. 250 , pp. 219 - 226 . CEUR-WS.org ( 2007 )

4. Bozzato , L. , Eiter , T. , Serafini , L. : Contextualized Knowledge Repositories with Justifiable Exceptions . In: DL2014. CEUR-WP , vol. 1193 , pp. 112 - 123 . CEUR-WS.org ( 2014 )

5. Bozzato , L. , Ferrari , M. : Composition of semantic web services in a constructive description logic . In: RR2010. Lecture Notes in Computer Science , vol. 6333 , pp. 223 - 226 . Springer ( 2010 )

6. Bozzato , L. , Ferrari , M. , Fiorentini , C. , Fiorino , G.: A decidable constructive description logic . In: JELIA 2010. Lecture Notes in Computer Science , vol. 6341 , pp. 51 - 63 . Springer ( 2010 )

7. Bozzato , L. , Ferrari , M. , Villa , P. : Actions over a constructive semantics for description logics . Fundam. Inform . 96 ( 3 ), 253 - 269 ( 2009 )

8. Brachman , R. , McGuinness , D. , Patel-Schneider , P. , Resnick , L. , Borgida , A. : Living with CLASSIC: When and how to use a KL-ONE-like language . In: Principles of Semantic Networks . pp. 401 - 456 . Morgan Kaufmann ( 1991 )

9. Calimeri , F. , Cozza , S. , Ianni , G. , Leone , N.: Enhancing ASP by functions: Decidable classes and implementation techniques . In: AAAI 2010 . AAAI Press ( 2010 )

10. Eiter , T. , Ianni , G. , Krennwallner , T. : Answer set programming: A primer . In: Reasoning Web 2009. Lecture Notes in Computer Science , vol. 5689 , pp. 40 - 110 . Springer ( 2009 )

11. Ferrari , M. , Fiorentini , C. , Fiorino , G.: BCDL: basic constructive description logic . J. of Automated Reasoning 44 ( 4 ), 371 - 399 ( 2010 )

12. Ferrari , M. , Fiorentini , C. , Momigliano , A. , Ornaghi , M.: Snapshot generation in a constructive object-oriented modeling language . In: LOPSTR 2007 , Selected Papers . Lecture Notes in Computer Science , vol. 4915 , pp. 169 - 184 . Springer ( 2008 )

13. Fiorentini , C. , Ornaghi , M. : Answer set semantics vs. information term semantics . In: ASP2007: Answer Set Programming , Advances in Theory and Implementation ( 2007 )

14. Fiorentini , C. , Momigliano , A. , Ornaghi , M. , Poernomo , I.: A constructive approach to testing model transformations . In: ICMT 2010. Lecture Notes in Computer Science , vol. 6142 , pp. 77 - 92 . Springer ( 2010 )

15. Haeusler , E.H. , de Paiva , V. , Rademaker , A. : Intuitionistic description logic and legal reasoning . In: DEXA 2011 Workshops . pp. 345 - 349 . IEEE Computer Society ( 2011 )

16. Hilia , M. , Chibani , A. , Djouani , K. , Amirat , Y. : Semantic service composition framework for multidomain ubiquitous computing applications . In: ICSOC 2012. Lecture Notes in Computer Science , vol. 7636 , pp. 450 - 467 . Springer ( 2012 )

17. Lifschitz , V. , Tang , L.R. , Turner , H.: Nested expressions in logic programs . Ann. Math. Artif. Intell . 25 ( 3-4 ), 369 - 389 ( 1999 )

18. Mendler , M. , Scheele , S. : Towards a type system for semantic streams . In: SR2009 - Stream Reasoning Workshop (ESWC 2009 ). CEUR-WP , vol. 466 . CEUR-WS.org ( 2009 )

19. Mendler , M. , Scheele , S. : Towards Constructive DL for Abstraction and Refinement . J. Autom. Reasoning 44 ( 3 ), 207 - 243 ( 2010 )

20. Miglioli , P. , Moscato , U. , Ornaghi , M. , Usberti , G.: A constructivism based on classical truth . Notre Dame Journal of Formal Logic 30 ( 1 ), 67 - 90 ( 1989 )

21. Motik , B. , Fokoue , A. , Horrocks , I. , Wu , Z. , Lutz , C. , Grau , B.C. : OWL 2 Web Ontology Language Profiles . W3C recommendation, W3C (Oct 2009 ), http://www.w3.org/TR/2009/RECowl2-profiles-20091027/

22. Odintsov , S. , Wansing , H.: Inconsistency-tolerant description logic. Part II: A tableau algorithm for CALCC . J. of Applied Logic 6 ( 3 ), 343 - 360 ( 2008 )

23. Ornaghi , M. , Benini , M. , Ferrari , M. , Fiorentini , C. , Momigliano , A. : A Constructive Modeling Language for Object Oriented Information Systems . Electr. Notes Theor. Comput. Sci . 153 ( 1 ), 55 - 75 ( 2006 )

24. Pearce , D. , Sarsakov , V. , Schaub , T. , Tompits , H. , Woltran , S.: A polynomial translation of logic programs with nested expressions into disjunctive logic programs: Preliminary report . In: ICLP 2002. Lecture Notes in Computer Science , vol. 2401 , pp. 405 - 420 . Springer ( 2002 )

25. Ricca , F. : The DLV java wrapper . In: AGP-2003 . pp. 263 - 274 ( 2003 )

26. Troelstra , A.S.: From constructivism to computer science . Theor. Comput. Sci . 211 ( 1-2 ), 233 - 252 ( 1999 )