ASP Based Generation of Information Terms for Constructive EL Loris Bozzato Fondazione Bruno Kessler, Via Sommarive 18, 38123 Trento, Italy bozzato@fbk.eu 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 ap- proaches have been shown for their use in knowledge representation and Seman- tic 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 EL 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. 1 Introduction Constructive description logics define interpretations of description logics under con- structive semantics. The need for such reinterpretation of description logics in non- classical semantics mostly arises for the interest in applying the formal properties of these semantics to solve modelling or reasoning problems. Starting from different rep- resentation interests and reference constructive semantics, several constructive charac- terizations 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 sys- tems, 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 EL [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 EL 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, EL 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 GALEN 2 ). 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 mathe- matical 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, generat- ing 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 G EN I T 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 descrip- tion logic EL [2]. This constructive semantics is a straightforward restriction of the basic constructive description logic BCDL [11] to the syntax of EL. – 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 EL 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 EL knowledge base – Using these formal results, in Section 5 we present Asp-it3 , a prototype implementa- tion 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 2 ELc: a constructive semantics for EL In this section we present a constructive semantics based on the minimal description logic EL [2]. We will refer to this logic as ELc: the presentation and information terms semantics of ELc are defined as a straightforward restriction of the logic BCDL [11]. Syntax. The language L for ELc 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 con- sider 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 charac- terization 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 ∀G C, meaning that every element of DOM(G) belongs to the concept C. Also, differently from the usual presentation of EL, we limit the use of the > constructor as a special kind of generator >N ∈ NG such that DOM(>N ) = N and for all generators G, DOM(G) ⊆ N . In the language L for ELc, concepts C are expressions of the kind: C ::= A | C u C | ∃R.C where A ∈ NC ∪ NG and R ∈ NR. Let VAR be a denumerable set of individual variables, the formulas K of L are defined as: K ::= R(s, t) | C(t) | ∀G C where s, t ∈ NI ∪ VAR, R ∈ NR, G ∈ NG and C is a concept. A formula is atomic if it is of the kind A(t) with A ∈ 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 ∈ NR, c, d ∈ NI and C a concept. A TBox is a finite set of formulas of the kind ∀G C (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 ∈ 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 , ·M i, where the domain ∆M is a non-empty set and ·M is a valuation map such that: for every c ∈ N , cM ∈ ∆M ; for every C ∈ NC, C M ⊆ ∆M ; for every R ∈ NR, RM ⊆ ∆M × ∆M ; for every G ∈ NGN , if DOM(G) = {c1 , . . . , cn }, then GM = {cM M 1 , . . . , cn }. Classical interpretation of non-atomic concepts is defined by the evaluation of description logics operators: (C1 u C2 )M = C1M ∩ C2M (∃R.C)M = {c ∈ ∆M | there exists d ∈ ∆M s.t. (c, d) ∈ RM and d ∈ C M } An assignment on M is a map θ : VAR → ∆M . If t ∈ NI ∪ VAR, tM,θ is the element of ∆M denoting t in M w.r.t. θ, namely: tM,θ = θ(t) if t ∈ VAR and tM,θ = tM if t ∈ NI. A formula K is valid in M w.r.t. θ, and we write M, θ |= K, if one of the following conditions holds: M |= R(s, t) iff (sM,θ , tM,θ ) ∈ RM M |= C(t) iff tM,θ ∈ C M M |= ∀G C iff GM ⊆ C M If Γ is a set of formulas, M |= Γ means that M |= K for every K ∈ Γ . K is a logical consequence of Γ , and we write Γ |= K iff, for every M, M |= Γ implies M |= K. As noted in [11], while non-conventional in description logics languages, the pro- vided definition of generators with a fixed domain simplifies the following presenta- tions 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 ex- ample, inspired to the classical example of [8], we want to describe the correct pairings between food and wines using an ELc knowledge base KW . The TBox of KW contains: (Ax1 ) ∀F ood ∃goesW ith.Color (Ax2 ) ∀Color ∃isColorOf.W ine with W ine ∈ NC, isColorOf, goesW ith ∈ NR and F ood, Color ∈ 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) = {f ish, meat} DOM (Color) = {red, white} The ABox of KW contains the following assertions: W ine(barolo) isColorOf (red, barolo) goesW ith(f ish, white) W ine(chardonnay) isColorOf (white, chardonnay) 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 = {f ishM , meatM } and ColorM = {redM , whiteM }. Note that, by the interpretation of ABox assertions, baroloM and chardonnay M 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 ELc 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 ∃R.C(a) in a model M can be explained by an information term (b, α) providing the filler b s.t. (aM , bM ) ∈ RM and, inductively, an information term α justifying bM ∈ C M . 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. IT N (K) = { tt }, if K is an atomic formula IT N (C1 u C2 (c)) = { (α, β) | α ∈ IT N (C1 (c)) and β ∈ IT N (C2 (c)) } IT N (∃R.C(c)) = { (d, α) | d ∈ N and α ∈ IT N (C(d)) } S IT N (∀G C) = { φ : DOM (G) → d∈ DOM (G) IT N (C(d)) | φ(d) ∈ IT N (C(d)) } 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 η ∈ ITN (K). We define the realizability relation Mhηi K by induction on the structure of K. M  htti K iff M |= 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 ∃R.C(c) iff M |= R(c, d) and M  hαi C(d) M  hφi ∀G C iff, for every d ∈ DOM(G), M  hφ(d)i C(d) If Γ is a finite set of closed formulas {K1 , . . . , Kn } of LN , ITN (Γ ) denotes the set of n-tuples η = (η1 , . . . , ηn ) such that, for every j ∈ {1, . . . , n}, ηj ∈ ITN (Kj ). We write M  hηi Γ iff, for every j ∈ {1, . . . , n}, M  hηj i Kj . Example 2. Let us consider the example knowledge base KW and the axiom (Ax1 ) in its TBox: every element φ ∈ ITN (Ax1 ) is a function mapping each food f ∈ DOM (F ood) to an information term φ(f ) ∈ IT N (∃goesW ith.Color). Thus, every φ(f ) has the form (c, tt), meaning that c is a Color that is admitted for f . For ex- ample, we can consider ψ1 ∈ 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 Mhψ1 i Ax1 . Similarly, if we consider ψ2 ∈ ITN (Ax2 ) where [ red 7→ (barolo, tt), white 7→ (chardonnay, tt) ] we have that M  hψ2 i 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 η ∈ IT N (K). For every model M, M  hηi K implies M |= K. t u 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 Γ ∪ {K} ∈ LN , we say that K is a constructive consequence of Γ (denoted c Γ |= K) iff, for every γ ∈ ITN (Γ ), there exists a η ∈ ITN (K) such that for every model M for LN , M  hγi Γ implies M  hηi K. c One important aspect (deeper investigated in [3,11]) is that such relation Γ |= 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 EL 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 ∈ LN a closed formula and η ∈ ITN (K). Following the construction in [13], we adapt the definitions for logic programs with nested expressions [17] to the structure and reading of ELc formulas. In this regard, we call lp-intepretation I any set of closed atomic formulas. Given a closed formula K ∈ LN , the usual satisfiability relation I |= K can naturally be defined as: I |= K, iff K ∈ I and K is atomic I |= C u D(c) iff I |= C(c) and I |= D(c) I |= ∃R.C(c) iff R(c, d) ∈ I for d ∈ N and I |= C(d) I |= ∀G C iff for every e ∈ DOM(G), I |= C(e) I |= Γ iff I |= K for K ∈ Γ 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 |= Γ and, for every I 0 ⊆ I, I 0 |= Γ implies I 0 = I. Given this definition of answer set on ELc 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 “∃R.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) = {K}, with K an atomic formula ans(h(α, β)iA1 u A2 (c)) = ans(hαiA1 (c)) ∪ ans(hβiA2 (c)) ans(h(d, α)i∃R.A(c)) = {R(c, d)} ∪ ans(hαiA(d)) S ans(hφi∀G A) = d∈DOM(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 ψ1 ∈ ITN (Ax1 ), by the definition of sets of answers for hψ1 iAx1 we have that: ans(hψ1 iAx1 ) = ans(hψ1 (f ish)i H1 (f ish)) ∪ ans(hψ1 (meat)i H1 (meat)) = ans(httiColor(white)) ∪ {goesW ith(f ish, white)} ∪ ans(httiColor(red)) ∪ {goesW ith(meat, red)} = {Color(white), goesW ith(f ish, white), Color(red), goesW ith(meat, red)} where we abbreviate H1 = ∃goesW ith.Color. Similarly, considering ψ2 ∈ ITN (Ax2 ) from previous example: ans(hψ2 iAx2 ) = {W ine(barolo), isColorOf (red, barolo), W ine(chardonnay), isColorOf (white, chardonnay)} 3 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 lp- interpretation I, I |= K iff there exists an information term η ∈ ITN (K) such that I |= ans(hηiK). t u 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 |= ans(hηiK). t u 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 ELc 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 |= 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 ∈ LN , then there exists a piece of information hηiK, with η ∈ 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 |= K and by Theorem 1 there exists η ∈ ITN (K) s.t. I |= ans(hηiK). By Theorem 2, for each M |= I this implies M  hηi K. We can prove that I is minimal: suppose that I 0 ⊆ I s.t. I 0 |= ans(hηiK), then by Theorem 1, I 0 |= K. Since I is an answer set for K, then I 0 = I. t u 4 This definition of answer sets for pieces of information corresponds to the notion of informa- tion content used in [7,14]. In the other direction, we need to define a notion of minimality on pieces of information as follows: Definition 2. Let K be a closed formula of LN . A piece of information hηiK is mini- mal iff there is no η 0 ∈ ITN (K) such that ans(hη 0 iK) ⊂ 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 defini- tion, 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 infor- mation for K. Then, ans(hηiK) is an answer set for K. Proof. By Theorem 1, for every lp-interpretation I s.t. I |= 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 |= K. Hence, considering I = ans(hηiK), also ans(hηiK) |= K. Moreover, let us consider I 0 ⊆ ans(hηiK) with I 0 |= K. Then, by Theorem 1, there exists a β ∈ ITN (K) s.t. I 0 |= ans(hβiK). Thus, ans(hβiK) ⊆ I 0 and, for the minimality of hηiK, this implies that ans(hβiK) = I 0 = ans(hηiK). t u 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 |= ans(hηiK) which implies that ans(hηiK) = I (since I is the minimal set of atoms s.t. I |= K). We can show that hηiK is a minimal piece of information: let us suppose that there exists a β ∈ 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). t u 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 infor- mation term η. The computation of answer sets can be achieved by translating the ini- tial 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 EL 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 for- mulation 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 ∈ NI, we consider subsets R of the set RN = {R(c, d) | R ∈ NR and c, d ∈ N } 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 ∈ 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 ∈ Γ , the model generating rewriting P1 (K) is defined as: A(b) 7→ { is(b, A) ← is(b, lA ). } R(a, b) 7→ { rel(a, R, b). } C u D(a) 7→ { is(a, lC ) ← is(a, lCuD ). is(a, lD ) ← is(a, lCuD ). } ∪ P1 (C(a)) ∪ P1 (D(a)) ∃R.C(a) 7→ { is(x, lC ) ← rel(a, R, x), is(a, l∃R.C ). } ∪ P1 (C(x)) ∀G C 7→ { is(x, lC ) ← is(x, G). } ∪ P1 (C(x)) where A ∈ NC ∪ NG, C, D are possibly complex concepts, R ∈ NR, a, b ∈ NI (or variables) and x is a variable. For each (possibly complex) concept assertion C(d) ∈ Γ , we add in P1 (Γ ) its “labelled” fact L(C(d)) = { is(d, lC ). }. Moreover, we as- sume that for each generator G used in Γ , with DOM(G) = {c1 , . . . , cn }, the facts { is(c1 , G)., . . . , is(cn , G). } are added to P1 (Γ ). The IT generating rewriting P2 (K), for each K ∈ Γ is defined as follows: A(b) 7→ { is it(tt, b, lA ) ← is(b, A). } R(a, b) 7→ { rel it(tt, a, R, b) ← rel(a, R, b). } C u D(a) 7→ { is it([x, y], a, lCuD ) ← is it(x, a, lC ), is it(y, a, lD ). } ∪ P2 (C(a)) ∪ P2 (D(a)) ∃R.C(a) 7→ { is it([x, y], a, l∃R.C ) ← rel it(tt, a, R, x), is it(y, x, lC ). } ∪ P2 (C(x)) ∀G C 7→ { isa it([x, y], G, lC ) ← is(x, G), is it(y, x, lC ). } ∪ P2 (C(x)) where A ∈ NC ∪ NG, C and D are concepts, R ∈ NR, a, b ∈ 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 asser- tions 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): {is(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)} By applying the IT generating rewriting P2 to the axiom (Ax2 ) we obtain the rules: isa it([x, y], Color, lH2 ) ← is(x, Color), is it(y, x, lH2 ). is it([x, y], z, lH2 ) ← rel(tt, z, isColorOf, x), is it(y, x, lW ine ). is it(tt, x, lW ine ) ← is(x, W ine). where H2 = ∃isColorOf.W ine. Intuitively, by applying these rules to the model com- puted 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 ) ∀F ood ∃goesW ith.(Color u ∃isColorOf.W ine) One can verify that, by applying P2 (Ax3 ) to the presented model, its computed infor- mation 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 ∈ LN and an answer set I for P1 (Γ ): (i). if K = C(a) and I |= is(a, lC ), then there exists an lp-interpretation I 0 for Γ s.t. I 0 |= K. (ii). if K = R(a, b) and I |= rel(a, R, b), then there exists an lp-interpretation I 0 for Γ s.t. I 0 |= K. Proof (Sketch). Point (ii). follows immediately considering that the fact rel(a, R, b) is added in P1 (Γ ) only if R(a, b) ∈ Γ . 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) ∈ Γ . Thus in every lp-interpretation I 0 for Γ it holds that I 0 |= K. Otherwise, is(a, lC ) ∈ I has been added in the application of a rule in P1 (Γ ) relative to a complex concept B or to a formula ∀G C. If B = C u D, then is(a, LCuD ) ∈ I and, by induction, there exists an lp- intepretation I 0 of Γ such that I 0 |= C u D(a). By definition, this implies I 0 |= C(a). If B = ∃R.C, then rel(c, R, a) ∈ I and is(c, l∃R.C ) ∈ I. The first implies that R(c, a) ∈ R. The second, by induction, implies that there exists an lp-interpretation I 0 of Γ such that I 0 |= ∃R.C(c) with I 0 |= R(c, a). For the definition of lp-interpretations, one of the admissible interpretations I 00 for ∃R.C(c) is the one in which I 00 |= R(c, a) and I 00 |= C(a). Thus, if I 0 = I 00 , then I 0 |= C(a). If is(a, lC ) ∈ I has been added by a rule relative to ∀G C, by definition I |= is(a, G) and a ∈ DOM(G) with ∀G C ∈ Γ . If I 0 is an lp-interpretation of Γ , then I 0 |= ∀G C and thus, for every d ∈ DOM(G), I 0 |= C(d). Hence, I 0 |= C(a). t u Given an lp-interpretation I for P (Γ ) and a closed formula K ∈ 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) = {α | I |= is it(α, a, lC )}. – If K = R(a, b), let IT (R(a, b), I) = tt iff I |= rel it(tt, a, R, b). – If K = ∀G C, let D = {c | I |= isa it([c, α], G, lC )}: – if D = DOM(G), let: IT (∀G C, I) = {φ | φ(c) = α for c ∈ DOM(G) and I |= isa it([c, α], G, lC )}; – otherwise, IT (∀G C, 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 ⊆ Γ , K a closed formula of LN , and I be the (unique) answer set for P (Γ ). If η ∈ IT (K, I), then there exists an lp-interpetation I 0 for Γ s.t. ans(hηiK) ⊆ I 0 Proof. We can show by induction on the structure of K that ans(hηiK) ⊆ I 0 . If K = R(a, b), then P2 (R(a, b)) = {rel it(tt, a, R, b) ← rel(a, R, b).} and I |= rel it(tt, a, R, b) only if I |= rel(a, R, b)., which by P1 implies that R(a, b) ∈ R with R ⊆ Γ . Thus for every lp-interpretation s.t. I 0 |= Γ , also {K} = ans(hηiK) ⊆ I 0 . If K = A(c) with A ∈ NC∪NG and tt ∈ IT (K, I), by the definition of P2 , we have that I |= is(c, A). Thus for Lemma 1 and the definition of P1 , I |= is(c, lA ) and there exists an lp-interpretation I 0 for Γ s.t. A(c) ∈ I 0 . This implies that ans(hηiK) ⊆ I 0 . If K = C u D(c) and (α, β) ∈ IT (K, I), by the definition of P2 , we have that I |= is it(α, c, lC ) and I |= 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 = ∃R.D(c) and (d, α) ∈ IT (K, I), by the definition of P2 , we have that rel it(tt, a, R, d), is it(α, d, lC ) ∈ I. By the definition of P2 , the first implies that R(a, d) ∈ R and, by induction hypothesis, there exists an lp-interpretation for Γ ans(hαiD(c)) ⊆ I 0 . This implies that ans(h(d, α)iK) ⊆ I 0 . If K = ∀G C and φ ∈ IT (K, I), by P2 we have that, for every c ∈ DOM(G), φ(c) = α and isa it([c, α], G, lC ) ∈ I. This means that is it(α, c, lC ) ∈ I. By induc- tion hypothesis, there exists Ic lp-interpretation S of Γ s.t. ans(hαiC(c)) ⊆ Ic . Thus, considering the lp-interpretation IG = c∈DOM(G) Ic , we have ans(hφiK) ⊆ IG . t u 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 ∃R.C(a), while an answer set for Γ “chooses” one of the possible b ∈ 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 = ∃R.C(a) disjunctive rules of the kind: f illsK (x) ∨ ¬f illsK (x) ← rel(a, R, x). is(x, lC ) ← f illsK (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 pos- sible b ∈ 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 proto- type, 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 EL 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 G EN I T 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 de- fined 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 load- ing and saving of OWL ontology files is managed using the OWL API 7 . 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, Datalog rewriting P(Γ) Input Output ontology Rewrite Retrieve Annotate ontology Γ P(Γ) Info.Terms hasIT Γ' DLV system Fig. 1. Asp-it information terms generation process 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 knowl- edge base: for each of the OWL logical axioms in Γ , their structure is recursively tra- versed 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 an- swer 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 con- tains (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/ 6 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 prop- erties) on the base of Semantic Web languages and tools. We first introduced a minimal constructive description logic ELc based on the language of EL. Then, we extended to this interpretation results linking its information terms semantics to answer set se- mantics: on these bases, we proposed a datalog rewriting aimed at the computation of information terms of an input ELc 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 EL family towards SROEL, corresponding to the full language of OWL-EL. References 1. Alviano, M., Faber, W., Leone, N., Manna, M.: Disjunctive datalog with existential quanti- fiers: 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 log- ics. 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 Net- works. 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 construc- tive 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 test- ing 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 reason- ing. 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 Com- puter 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. Au- tom. 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 Lan- guage Profiles. W3C recommendation, W3C (Oct 2009), http://www.w3.org/TR/2009/REC- owl2-profiles-20091027/ 22. Odintsov, S., Wansing, H.: Inconsistency-tolerant description logic. Part II: A tableau algo- rithm for CALC C . J. of Applied Logic 6(3), 343–360 (2008) 23. Ornaghi, M., Benini, M., Ferrari, M., Fiorentini, C., Momigliano, A.: A Constructive Mod- eling 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)