Reasoning on Information Term Semantics with ASP for Constructive EL⊥ Loris Bozzato1 and Camillo Fiorentini2 1 Fondazione Bruno Kessler, Via Sommarive 18, 38123 Trento, Italy 2 DI, Univ. degli Studi di Milano, Via Celoria 18, 20133 Milano, Italy Abstract. Constructive description logics represent different re-inter- pretations of description logics (DLs) under constructive semantics. Con- structive description logics have been mostly studied for their formal properties, while limited practical approaches have been shown for their use in Knowledge Representation languages and tools (which, on the other hand, constitute the distinctive applications of description logics). To address this aspect, we recently studied the relation of constructive DLs based on Information Term semantics with Answer Set semantics in the context of the positive logic EL. In this paper we continue this study in the direction of more expressive DLs by considering the introduction of negative information, leading to a constructive interpretation for the DL EL⊥ . We show that formal results linking the constructive semantics to answer set semantics can be extended to the case of negative information in EL⊥ . 1 Introduction Constructive description logics are interpretations of description logics (DLs) under different constructive semantics. The application of such non-classical se- mantics to description logics is motivated by the interest in applying the formal properties of constructive semantics to different aspects of knowledge represen- tation. Starting from different constructive semantics, several constructive de- scription logics have been proposed, see e.g. [6,9,16]. Constructive description logics have been mostly studied from a theoretical viewpoint, and they have also been applied to tackle different representation and reasoning problems (see, e.g., [4,12,13,15]); however, the interaction between formal and practical aspects of constructive DLs has been scarcely investigated. To bridge this gap, in [2] we have introduced a simple constructive DL based on EL and we have disussed its relationship with Answer Set Programming (ASP). From the practical point of view, by taking advantage of such a relation, we have presented a datalog encoding managing one reasoning task over the constructive semantics (namely, the generation of valid “states” of a knowledge base) and we have developed a prototype based on the standard OWL-EL profile and “off the shelf” tools for manipulation of OWL 2 ontologies and ASP reasoning. Copyright c 2020 for this paper by its authors. Use permitted under Creative Com- mons License Attribution 4.0 International (CC BY 4.0). Our constructive interpretation of EL is based on information term seman- tics [5,9]: the information terms (ITs) are syntactical objects that provide a constructive justification for the classical truth of a formula. Information terms have been used to represent the state or answer of a formula (and, for exten- sion, a notion of “snapshot” representing a valid state of a knowledge base). In particular, [2] follows the direction studied in [10], where the relation be- tween information term and answer set semantics has been first studied over propositional theories. In fact, we remark that [2] extends for the first time the study of relations between IT semantics and ASP to the context of constructive description logics. In this paper, we continue the investigation started in [2] by “pushing the envelope” towards more expressive DLs: as a first step we introduce falsum in EL, thus providing a constructive interpretation for the DL EL⊥ . Then, we show how the results linking IT semantics and answer set semantics can be extended in presence of negative information. Intuitively, following [10], negative information can be represented similarly to default negation in ASP: negative formulas are used as constraints and answer sets are formulated over a suitable positive reduction of the input formulas w.r.t. negative information. Our goal in this paper is to show that results connecting IT semantics and answer set semantics can be expanded to EL⊥ in presence of negative information. These connections can be then leveraged to reason on the constructive reading of EL⊥ using ASP tools, for example for computing the valid ITs of a knowledge base as in [2]: this task represents an essential step in order to use transformations of ITs in reasoning, e.g., to represent change of states as in [4]. In the following sections, we first present (see Section 2) the definition of the IT interpretation of EL⊥ (that we call ELc⊥ ); then, in Section 3 we extend the definition of answer sets for formulas and answer sets to this logic and we show how to extend the results connecting the IT semantics and answer set semantics for ELc⊥ . Finally, in Section 4 we briefly discuss how to extend to ELc⊥ the datalog implementation from [2] for the generation of IT of knowledge bases. Proofs of the main results from Section 3 are provided in the Appendix. 2 Constructive Description Logic ELc⊥ We present a constructive semantics based on information term semantics (as in BCDL [9]) for the description logic EL⊥ [1]; we refer to this logic as ELc⊥ . 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. In addition, we introduce 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 gen- erator G is an atomic concept associated with 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 ele- ment of dom(G) belongs to the concept C; thus, the formula ∀G C can be read as the subsumption relation G v C.3 In the language L for ELc⊥ , concepts C are inductively defined as: C ::= > | ⊥ | A | ¬C1 | C1 u C2 | ∃R.C1 where A ∈ NC ∪ NG and R ∈ NR.4 The formulas K of L are defined as: K ::= R(c, d) | C(c) | ∀G C where c, d ∈ NI, R ∈ NR, G ∈ NG and C is a concept (as defined above). We point out that ∀G C represents the inclusion (subsumption) between concepts G and C. A formula K is atomic if K has the form R(s, t), >(t), ⊥(t), A(t) with A ∈ NC ∪ NG; K is simple if it is an atomic or a negated formula (namely, K = ¬C(t)); K is positive if it does not contain a negation or ⊥. A theory K (that is, a knowledge base) is a finite set of formulas which is partitioned as usual into ABox and TBox. The ABox contains formulas of the kind C(d) and R(c, d), with R ∈ NR, c, d ∈ NI and C is a concept. The TBox contains formulas of the kind ∀G C, representing subsumption axioms. In the following we refer to languages LN restricted to finite subsets N of NI. Given a finite N ⊆ NI, let NGN be the set of generators G ∈ NG such that dom(G) ⊆ N . By LN we denote 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 as usual: ⊥M = ∅ >M = ∆M (C1 u C2 )M = C1M ∩ C2M (¬C)M = ∆M \ C M (∃R.C)M = {c ∈ ∆M | ∃d ∈ ∆M s.t. (c, d) ∈ RM , d ∈ C M } A formula K is valid in M, written M |= K, iff one of the following conditions holds: M |= R(c, d) iff (cM , dM ) ∈ RM M |= C(d) iff dM ∈ C M M |= ∀G C iff GM ⊆ C M If Γ is a set of formulas, M |= Γ means that M |= K, for every K in Γ . 3 While non-conventional in DL languages, as noted in [9], the definition of generators with a fixed domain simplifies the following presentations of the constructive seman- tics. Alternatively, domain of generators can be defined by extending the language with nominals and directly including the domains declaration in the knowledge base. 4 Note that concept negation ¬C1 does not appear in the standard syntax of EL⊥ . It can be simulated by introducing a new concept C 1 and the axiom C1 u C 1 v ⊥. Example 1. We reprise the running example presented in [2], inspired by the classical example of food and wine pairings from [8], including negative informa- tion to introduce constraints. The set NI contains names for wines, colors and regions. The set NC contains the concepts Wine, defining wines, and ExcRegion, defining regions to be excluded. We introduce the generators Food and Color , defining foods and colors respectively, and we set: dom(Food ) = {fish, meat} and dom(Color ) = {red , white}, where fish, meat, red and white are elements of NI. The set NR contains the role names goesWith, to represent the matches between wine colors and foods, isColorOf , to associate a color with a wine, hasRegion, to map a wine to its origin region. We introduce the knowledge base KW consisting of the TBox axioms: (Ax1 ) ∀Food ∃goesWith.Color (Ax2 ) ∀Color ∃isColorOf .(Wine u ¬(∃hasRegion.ExcRegion)) Intuitively, axiom Ax1 asserts that each Food matches an appropriate wine Color ; Ax2 states that for every Color there is at least a Wine not originat- ing from an ExcRegion (excluded region). Note that the negated subconcept of Ax2 behaves like a constraint. The ABox of KW consists of the following assertions: Wine(barolo) isColorOf (red , barolo) Wine(chardonnay) isColorOf (white, chardonnay) Wine(cabernet) isColorOf (red , cabernet) hasRegion(barolo, piedmont) goesWith(fish, white) hasRegion(chardonnay, lombardy) goesWith(meat, red ) hasRegion(cabernet, california) ExcRegion(california) We can take as N any finite set containing individual names occurring in the ABox. We point out that a classical model M for KW must interpret the gen- erator Food as the set {fish M , meat M } and Color as {red M , white M }. Instead, ExcRegion can be interpreted by any superset of {california M } satisfying the axioms. 3 Information term semantics. The constructive semantics for ELc⊥ is based on the notion of information term [17]. Information term semantics is related to the BHK (Brower-Heyting-Kolmogorov) interpretation of logical connectives [18]: 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 instance, the validity of the formula ∃R.C(d) in a model M can be explained by an infor- mation term (e, η) providing the filler e s.t. (dM , eM ) ∈ RM and, inductively, an information term η justifying eM ∈ C M . A simple formula K does not need any constructive explanation, thus the associated information term is an atom, denoted by tt. Given a finite subset N of NI and a formula K of LN , we define the set of information terms itN (K) by induction on K as follows. itN (K) = { tt }, if K is a simple formula itN ((C1 u C2 )(c)) = { (α, β) | α ∈ itN (C1 (c)) and β ∈ itN (C2 (c)) } itN (∃R.C(c)) = { (d, α) | d ∈ N and α ∈ itN (C(d)) } S itN (∀G C) = { φ : dom(G) → d∈dom(G) itN (C(d)) | φ(d) ∈ itN (C(d)) } Note that no constructive information is associated with negated sub-formulas, which are treated similarly to atomic formulas: negative sub-formulas can be seen as “constraints” that need to be verified by the models of the knowledge base. The justification of formulas in classical models with respect to one of their information terms is given by the realizability relation. Let M be a model for LN , K a formula of LN and η ∈ itN (K). We define the realizability relation M  hηi K by induction on the structure of K: M  htti K iff M |= K, where K is a simple 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) Example 2. Let us consider the knowledge base KW defined in Example 1. An element φ ∈ itN (Ax1 ) is a function mapping each food f ∈ dom(Food ) to an information term φ(f ) ∈ itN (∃goesWith.Color (f )). Thus, every φ(f ) has the form (c, tt), meaning that c is a proper color for f . An element ψ1 ∈ itN (Ax1 ) is: [ fish 7→ (white, tt), meat 7→ (red , tt) ] Similarly, we can define ψ2 ∈ itN (Ax2 ) as follows: [ red 7→ (barolo, (tt, tt)), white 7→ (chardonnay, (tt, tt)) ] where there is no constructive information associated with the negated subcon- cept of Ax2 . We point out that every model M of the ABox of KW satisfies both M  hψ1 i Ax1 and M  hψ2 i Ax2 . 3 The following result, provable by induction on the structure of K, shows the relation between classical and constructive semantics (see Lemma 2 in [9]). Proposition 1. Let N be a finite subset of NI, K a formula of LN and η ∈ itN (K). For every model M, M  hηi K implies M |= K. Thus, the constructive semantics preserves the classical declarative reading of DL formulas. The converse of Proposition 1 does not hold in general, unless we assume stronger conditions, such as the reachability of M (i.e., every element in the domain of M is denoted by a constant, see e.g. [7]). First-order translation. We introduce a first-order translation of ELc⊥ for- mulas (see similar translations in [3]), that we exploit as an intermediate rep- resentation to define the notion of reduction of a formula. Let N be a finite subset of NI. By L1N we denote the first-order language having constants N , a unary predicate symbol A, for every A ∈ NC ∪ NG, a binary relation symbol R, for every R ∈ NR, the logical constants t (true) and f (false), the connectives ¬ and ∧. We also introduce unary function symbols f∃R.C to be used as Skolem functions to properly translate existential concepts ∃R.C. Firstly, we introduce the translation γC mapping a concept C to a first-order formula F of L1N , hav- ing x as possible free variable; γC (t) denotes the formula obtained by replacing every occurrence of x in γC with the term t. A 7→γ A(x) > 7→γ t ⊥ 7→γ f ¬C 7→γ ¬γC C1 u C2 7→γ γC1 ∧ γC2 ∃R.C 7→γ R(x, f∃R.C (x)) ∧ γC (f∃R.C (x)) In translating C, we stipulate that different occurrences of the same existential 1 subformulas ∃R.D of C are associated with different Skolem function (e.g., f∃R.D , 2 f∃R.D , and so on). Given a formula K ∈ LN , the first-order translation Φ(K) of K is defined as follows: C(d) 7→Φ γC (d) R(c, d) 7→Φ R(c, d) ∀G C 7→Φ γC (c1 ) ∧ · · · ∧ γC (cn ), where {c1 , . . . , cn } = dom(G) Example 3. Let KW be the knowledge base from Example 1. The first-order translation of Ax1 is (C = ∃goesWith.Color ): Φ(Ax1 ) = γC (meat) ∧ γC (fish) γC = goesWith(x, fC (x)) ∧ Color (fC (x)) Similarly, Ax2 is translated as follows: D = ∃isColorOf .(Wine u ¬E ) E = ∃hasRegion.ExcRegion Φ(Ax2 ) = γD (red ) ∧ γD (white) γD = isColorOf (x, fD (x)) ∧ γ(Wineu¬E) (fD (x)) γ(Wineu¬E) = Wine(x) ∧ ¬ ( hasRegion(x, fE (x)) ∧ ExcRegion(fE (x)) ) 3 An interpretation I for L1N is a classical interpretation for the language L1N satisfying the following condition: for each generator G ∈ NGN , I |= G(c) iff c ∈ dom(G) (∗) Next proposition states the correspondence between first-order translation and classical semantics: Proposition 2. Let K be a formula of LN . (i). If M |= K, then there is an interpretation I for L1N such that I |= Φ(K). (ii). If I |= Φ(K), with I an interpretation for L1N , then there is an interpre- tation M for LN such that M |= K. 3 Answer Set Semantics for Formulas and Information Terms Following the construction in [10], we adapt the definitions concerning logic pro- grams with nested expressions [14] to ELc⊥ formulas. The first step to define a notion of answer sets for ELc⊥ formulas is thus to define a notion of interpreta- tion akin to the one used in logic programs. In this regard, an lp-interpretation I over LN is a set of atomic formulas H of LN such that H = A(c) or H = R(c, d), where A ∈ NC ∪ NG, R ∈ NR and c, d ∈ N . Given a formula K of LN , the sat- isfiability relation I |= K, and its extension to sets of formulas Γ , is defined as follows: I |= >(c) for every c ∈ N I |= H iff H ∈ I, where either H = A(c) and A ∈ NC ∪ NG, or H = R(c, d) I |= G(c) iff c ∈ dom(G), where G ∈ NG I |= ¬C(c) iff I 6|= C(c) I |= C u D(c) iff I |= C(c) and I |= D(c) I |= ∃R.C(c) iff there is d ∈ N such that R(c, d) ∈ I and I |= C(d) I |= ∀G C iff for every e ∈ dom(G), I |= C(e) I |= Γ iff I |= K for every K ∈ Γ We remark that I 6|= ⊥(c), for every c ∈ N ; moreover, I satisfies condition (∗) of previous section. The definition of J |= F , where J is an lp-interpretation over L1N and F a formula of L1N , is similar. We point out that J must be a set of formulas of the kind A(t1 ) and R(t1 , t2 ), where A ∈ NC ∪ NG, R ∈ NR, t1 and t2 are ground terms (namely, they do not contain variables). Given an lp-interpretation I over LN , the extension I + of I is an lp-interpre- tation over L1N obtained by properly interpreting Skolem functions. More specifi- cally, I + is the smallest extension of I satisfying the following property: for every formula K = ∃R.C(c) of LN such that I |= K, let d such that R(c, d) ∈ I and I |= C(d), and let fK be a Skolem function associated with ∃R.C; then, I + contains the formulas R(c, fK (c)) and d = fK (c). The reduct of a formula K ∈ LN w.r.t an lp-interpretation I, denoted by K I , is obtained from the formula Φ(K) of L1N by replacing every negated subformula ¬C(c) with either t or f, in compliance with I + . Formally, the reduct of a formula F ∈ L1N w.r.t. an lp-interpretation J (over L1N ), denoted by F J , is the formula of L1N inductively defined as follows:5 H J = H, if H is an atomic formula of L1N  f if J |= C (¬C)J = (C ∧ D)J = C J ∧ DJ t otherwise We define the reduct on formulas K of LN and set of formulas Γ as follows: + K I = (Φ(K))I Γ I = { KI | K ∈ Γ } 5 Atomic formulas of L1N are the Φ-images of atomic formulas of LN . We remark that, for positive formulas K, we have K I = Φ(K). Example 4. We show the definition of reduct of axioms in KW (see Exam- ple 1) based on the first-order translation displayed in Example 3. Let I be the lp-interpretation coinciding with the ABox of KW . The extension I + is ob- tained by adding to I the formulas (D = ∃isColorOf .(Wine u ¬E ) and E = ∃hasRegion.ExcRegion): isColorOf (red , fD (red )), fD (red ) = barolo, isColorOf (white, fD (white)), fD (white) = chardonnay, hasRegion(fD (red ), fE (fD (red ))), fE (fD (red )) = piedmont, hasRegion(fD (white), fE (fD (white))), fE (fD (white)) = lombardy, . . . I The reduction KW is computed as follows: since Ax1 is a positive formula, then + Ax1 = Φ(Ax1 ). Instead, AxI2 coincides with the formula Φ(Ax2 )I such that: I + + + Φ(Ax2 )I = (γD (red ))I ∧ (γD (white))I + (γD (red ))I = isColorOf (red , fD (red)) ∧ Wine(fD (red)) ∧ t I+ (γD (white)) = isColorOf (white, fD (white)) ∧ Wine(fD (white)) ∧ t Note that both occurrences of the constraint ¬E are reduced to t, since we have that, for c ∈ {red , white}, I + 6|= (hasRegion(c, fE (c)) ∧ ExcRegion(fE (c)). 3 We introduce the notion of answer set for formulas: Definition 1. An lp-interpretation I is an answer set for a set of positive for- mulas Γ ⊆ LN (resp. Γ ⊆ L1N ) iff I |= Γ and, for every I 0 ⊆ I, I 0 |= Γ implies I 0 = I. An lp-interpretation I is an answer set for a set of formulas Γ ⊆ LN iff I + is an answer set for Γ I . In the following we want to extend this notion of answer set to pieces of infor- mation. We call piece of information over LN an expression of the kind hηiK with K ∈ LN a formula and η ∈ itN (K). 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 a simple 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 simple formulas. Note that negated formulas of the kind ¬C(d) are considered as simple formulas and their only possible information term is tt: intuitively, this corresponds to considering these formulas as constraints, i.e. we only require that C(d) does not hold, without any constructive information about non-validity. Example 5. Let us consider the information terms ψ1 ∈ itN (Ax1 ) and ψ2 ∈ itN (Ax2 ) defined in Example 2; we have: H1 = ∃goesWith.Color H2 = ∃isColorOf .H3 H3 = Wine u ¬(∃hasRegion.ExcRegion) ans(hψ1 iAx1 ) = ans(hψ1 (fish)i H1 (fish)) ∪ ans(hψ1 (meat)i H1 (meat)) = ans(httiColor (white)) ∪ { goesWith(fish, white) } ∪ ans(httiColor (red )) ∪ { goesWith(meat, red ) } = { Color (white), goesWith(fish, white), Color (red ), goesWith(meat, red ) } ans(hψ2 iAx2 ) = ans(hψ2 (red )i H2 (red )) ∪ ans(hψ2 (white)i H2 (white)) = { isColorOf (red , barolo) } ∪ ans(h(tt, tt)iH3 (barolo)) ∪ { isColorOf (white, chardonnay) } ∪ ans(h(tt, tt)iH3 (chardonnay))} = { isColorOf (red , barolo), Wine(barolo), ¬(∃hasRegion.ExcRegion)(barolo), isColorOf (white, chardonnay), Wine(chardonnay), ¬(∃hasRegion.ExcRegion)(chardonnay) } 3 We point out that ans(hηiK) in some sense unfolds the constructive meaning of hηiK. Actually, by induction on the structure of K, we can prove that: Theorem 1. Let N be a finite subset of NI, K a formula of LN . For every model M, M  hηi K iff M |= ans(hηiK). Accordingly, the problem of determining the realizability of a formula (w.r.t. an information term) can be reduced to the classical satisfiability of a finite set of atomic formulas. By Theorem 1, and taking into account that lp-interpretations are reachable models, we can strengthen Proposition 1 as follows: Theorem 2. Let N be a finite subset of NI, K a formula of LN . For every lp-interpretation I, I |= K iff there exists an information term η ∈ itN (K) such that I |= ans(hηiK). Now we can study the relations between answer sets for ELc⊥ formulas and pieces of information. Definition 2. Let K be a formula of LN and K ∈ itN (K). An lp-interpretation I is a minimal model of hηiK iff: – I |= ans(hηiK) and, – for every lp-interpretation I 0 ⊆ I, I 0 |= ans(hηiK) implies I 0 = I. Note that, by Theorem 1, this definition implies that, for every model M for LN such that M |= I, it holds that M  hηi K. Lemma 1. Let N be a finite subset of NI, K a formula of LN and I an lp- interpretation. Then: (i) I |= K iff I + |= Φ(K); (ii) I |= K iff I + |= K I ; (iii) I + |= K I iff there exists η ∈ itN (K) s.t. I + |= (ans(hηiK))I . In one direction we can show: Theorem 3. If I is an answer set for a formula K ∈ LN , then there exists η ∈ itN (K) such that I is a minimal model of hηiK. In the other direction, we need to define a notion of minimality on pieces of information and introduce default reasoning as follows. Definition 3. Let K be a positive formula of LN . A piece of information hηiK is minimal iff there is no η 0 ∈ itN (K) such that ans(hη 0 iK) ⊂ ans(hηiK). Similarly to [2], in the case of (sets of) positive formulas the following property can be shown: Theorem 4. Let K be a positive formula of LN and hηiK be a minimal piece of information for K. Then, ans(hηiK) is an answer set for K. In the general case (i.e. when negative information can occur in formulas), we need to generalize this result by including a notion of negative answer set: these sets represent constraints that positive answer sets need to meet, in order to be considered as valid answers for the piece of information given as input. Positive and negative answers of a piece of information hηiK are defined as follows: ans+ (hηiK) = { H ∈ ans(hηiK) | H = A(c), with A ∈ NC ∪ NG, or H = R(c, d) } ans− (hηiK) = { H ∈ ans(hηiK) | H = ¬C(d) or H = ⊥(d) } Note that ans+ (hηiK) is an lp-interpretation. Example 6. The set ans(hψ2 iAx2 ) in Example 5 can be partitioned into positive answers and constraints as follows: ans+ (hψ2 iAx2 ) = { isColorOf (red , barolo), Wine(barolo), isColorOf (white, chardonnay), Wine(chardonnay) } ans− (hψ2 iAx2 ) = { ¬(∃hasRegion.ExcRegion)(barolo), ¬(∃hasRegion.ExcRegion)(chardonnay) } 3 We introduce the notion of answer set and minimality concerning pieces of in- formation. Definition 4. Let K be a formula of LN and hηiK a piece of information. Then, ans+ (hηiK) is an answer set for hηiK iff ans+ (hηiK) |= ans− (hηiK). Definition 5. Let K be a formula of LN . A piece of information hηiK is min- imal iff, for every η 0 ∈ itN (K) such that ans+ (hη 0 iK) ⊂ ans+ (hηiK), it holds that ans+ (hηiK) 6|= ans− (hη 0 iK). Using these definitions, we can generalize Theorem 4 as follows: Theorem 5. Let K be a formula of LN and hηiK be a minimal piece of infor- mation for K with answer set ans+ (hηiK). Then, ans+ (hηiK) is an answer set for K. To complete the picture, we state the following characterization of answer sets: Theorem 6. Let K be a 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). 4 Discussion: ASP based IT generation for ELc⊥ As discussed in [2], and as a consequence of the results of previous section, a way to solve the reasoning task of generating information terms of an input ELc⊥ knowledge base consists in computing its answer sets and then, by exploiting the recursive definition of ans(hηiK), reconstruct the corresponding (minimal) information term η. In [2] we have presented alternative datalog encodings for an input EL knowl- edge base in order to generate its answer sets and build minimal information terms from them. In the case of negative information of ELc⊥ , we need to adapt the datalog encoding in order to consider the constraints provided by the nega- tive sub-formulas, so that the candidate answer sets not matching the constraints are discarded. A possible way to encode negative constraints, reflecting the def- inition of reduct K I provided in previous sections, is to use default negation under the answer set semantics [11] and check that the computed answer sets do not contradict the constraints. For example (using the rules of the translation P2 in [2]), information terms of a formula ¬D(a) can be computed by the rules: is it(tt, a, l¬D ) ← nom(a), not check (a, lD ). check (a, lD ) ← is it(x, a, lD ). Another option is to encode negative information as constraints rules (i.e. rules of the form ← b1 , . . . , bn .) in the rules generating the candidate answer sets, so that interpretations that verify the body of such rules are excluded from the computed answer sets. We leave as future work the formal definition of a suitable datalog encoding for ELc⊥ for the ASP based generation of information terms and the proof of its correctness with respect to the formal results shown in this paper. As noted in [2], an issue that deserves to be investigated is how the intrinsic complexity of IT generation can be related to the computation of answer sets (and whether complexity can be limited in practical scenarios). 5 Conclusions In this paper we present the relation between answer set semantics and informa- tion term semantics in the context of the description logic EL⊥ . Following [2], we first provide the definition of the information term semantics for EL⊥ . Then, we show how to extend the results presented in [2] concerning the correspon- dence between answer set semantics and information term semantics to EL⊥ . By introducing a notion of reduction, similar to the one used in Answer Set Pro- gramming, it is possible to use negative information as constraints that answer sets must verify; this leads to the notion of minimal pieces of information of a KB. Finally, we briefly discuss how these results can be used to generate the information terms of an input KB over ELc⊥ . We note that the constructive reading of formulas provided by information term semantics can be related to the recent interest in Explainable AI (which is being discussed also in the field of symbolic Knowledge Representation and Reasoning). For example, as shown in [7], the generation of a valid “snapshot” of a knowledge base (i.e. a valid information term for its set of formulas) can be used to verify the set of constraints encoded by the KB and, in case of a violation, to constructively identify the source of inconsistencies, in order to amend the KB. The work presented in this paper represents a first step towards the extension of this study to more expressive description logics: for example, an interesting goal is to extend the discussed results to the full language of ALC, exploiting the information term semantics presented in [9]. Another issue to be investigated is the application of the presented formal results to representation and reasoning tasks, for example by extending the datalog encoding and prototype discussed in [2] for ASP based generation of information terms. We also aim at developing procedures for the manipulation of information terms (see, e.g., [4]), in order to apply IT semantics in concrete problems. References 1. F. Baader. Terminological cycles in a description logic with existential restrictions. In IJCAI-03, pages 325–330. Morgan Kaufmann, 2003. 2. L. Bozzato. ASP based generation of information terms for constructive EL. Fun- dam. Inform., 161(1-2):29–51, 2018. 3. L. Bozzato, T. Eiter, and L. Serafini. Reasoning with Justifiable Exceptions in EL⊥ Contextualized Knowledge Repositories. In Description Logic, Theory Com- bination, and All That, volume 11560 of LNCS, pages 110–134. Springer, 2019. 4. L. Bozzato and M. Ferrari. Composition of semantic web services in a constructive description logic. In RR2010, volume 6333 of LNCS, pages 223–226. Springer, 2010. 5. L. Bozzato, M. Ferrari, C. Fiorentini, and G. Fiorino. A constructive semantics for ALC. In DL2007, volume 250 of CEUR-WP, pages 219–226. CEUR-WS.org, 2007. 6. L. Bozzato, M. Ferrari, C. Fiorentini, and G. Fiorino. A decidable constructive description logic. In JELIA 2010, volume 6341 of LNCS, pages 51–63. Springer, 2010. 7. L. Bozzato, M. Ferrari, and P. Villa. Actions over a constructive semantics for description logics. Fundam. Inform., 96(3):253–269, 2009. 8. R.J. Brachman, D.L. McGuinness, P.F. Patel-Schneider, L.A. Resnick, and A. Borgida. Living with CLASSIC: When and how to use a KL-ONE-like lan- guage. In Principles of Semantic Networks, pages 401–456. Morgan Kaufmann, 1991. 9. M. Ferrari, C. Fiorentini, and G. Fiorino. BCDL: basic constructive description logic. J. of Automated Reasoning, 44(4):371–399, 2010. 10. C. Fiorentini and M. Ornaghi. Answer set semantics vs. information term seman- tics. In ASP2007: Answer Set Programming, Advances in Theory and Implemen- tation, 2007. 11. M. Gelfond and V. Lifschitz. Classical Negation in Logic Programs and Disjunctive Databases. New Generation Computing, 9:365–385, 1991. 12. E. Hermann Haeusler, V. de Paiva, and A. Rademaker. Intuitionistic description logic and legal reasoning. In DEXA 2011 Workshops, pages 345–349. IEEE Com- puter Society, 2011. 13. M. Hilia, A. Chibani, K. Djouani, and Y. Amirat. Semantic service composition framework for multidomain ubiquitous computing applications. In ICSOC 2012, volume 7636 of LNCS, pages 450–467. Springer, 2012. 14. V. Lifschitz, L. R. Tang, and H. Turner. Nested expressions in logic programs. Ann. Math. Artif. Intell., 25(3-4):369–389, 1999. 15. M. Mendler and S. Scheele. Towards a type system for semantic streams. In SR2009 - Stream Reasoning Workshop (ESWC 2009), volume 466 of CEUR-WP. CEUR-WS.org, 2009. 16. M. Mendler and S. Scheele. Towards Constructive DL for Abstraction and Refine- ment. J. Autom. Reasoning, 44(3):207–243, 2010. 17. P. Miglioli, U. Moscato, M. Ornaghi, and G. Usberti. A constructivism based on classical truth. Notre Dame Journal of Formal Logic, 30(1):67–90, 1989. 18. A. S. Troelstra. From constructivism to computer science. Theoretical Computer Science, 211(1-2):233–252, 1999. A Appendix: Proofs Lemma 1. Let N be a finite subset of NI, K a formula of LN and I an lp- interpretation. Then: (i) I |= K iff I + |= Φ(K); (ii) I |= K iff I + |= K I ; (iii) I + |= K I iff there exists η ∈ itN (K) s.t. I + |= (ans(hηiK))I . Proof. (i). We first note that, by the definition of I + , if fD (d) = e in I + , then fD (d) behaves like e in I + , namely: (‡) for every concept C, I |= C(e) iff I + |= C(fD (d)). We can show the claim by induction of the form of the formula K. – Let K be atomic. If K = A(c) or R(c, d), then Φ(K) = K and (i) trivially holds. If K = >(c), then Φ(K) = t and K = ⊥(c), then Φ(K) = f; in both cases (i) holds. – Let K = ¬C(d). Note that Φ(¬C(d)) = ¬Φ(C(d)). If I |= ¬C(d), then by definition I 6|= C(d). By induction hypothesis, I + 6|= Φ(C(d)), which implies I + |= ¬Φ(C(d)), namely I + |= Φ(¬C(d)). Similarly, if I + |= Φ(¬C(d)), we conclude I |= ¬C(d). – Let K = C1 uC2 (d). Note that Φ(C1 uC2 (d)) = Φ(C1 (d))∧Φ(C2 (d)). If I |= K, then I |= C1 (d) and I |= C2 (d). By induction hypothesis, I + |= Φ(C1 (d)) and I + |= Φ(C2 (d)). Conversely, if I + |= Φ(K), we get I |= K. – Let K = ∃R.C(d). Note that Φ(K) = R(d, f∃R.C (d)) ∧ γC (f∃R.C (d)). Let us assume I |= ∃R.C(d). By hypothesis, there exists e ∈ N such that R(d, e) ∈ I and I |= C(e). By induction hypothesis and the definition of the extension I + , I + |= R(d, e) and I + |= Φ(C(e)). By (‡), we get I + |= R(d, f∃R.C (d)) and I + |= Φ(C(f∃R.C (d))), namely I + |= γC (f∃R.C (d)); we conclude I + |= Φ(K). Conversely, let us assume I + |= Φ(K). Then, I + |= R(d, f∃R.C (d)) and I + |= γC (f∃R.C (d)). By the definition of I + , I contains a formula of the kind R(d, e) and, by (‡), we get I + |= γC (e). By induction hypothesis we get I |= C(e), thus I |= ∃R.C(d). – Let K = ∀G C. We have Φ(K) = Φ(C(c1 ))∧· · ·∧Φ(C(cn )), thus we can proceed as in the case concerning u. (ii). One can easily prove that, for every formula F of L1N , I |= F iff I |= F I . + Thus, I |= K iff I + |= Φ(K) (by point (i)), iff I + |= (Φ(K))I (by the previous remark), iff I + |= K I (by definition of K I ). (iii). Considering the definition of ans and reduction K I , we show the claim by induction on the structure of K (and definition of ans): – Let K be atomic. Then we have that K I = K and (ans(httiK))I = {K} thus the claim immediately follows. – Let K = ¬C(d). Since K is a simple formula, we have that (ans(httiK))I = {K}I . Thus, it immediately follows that I + |= K I iff I + |= (ans(httiK))I . – Let K = C1 u C2 (d). Then we have K I = (γC1 (d))I ∧ (γC2 (d))I and (ans(h(α, β)iK))I = ans(hαiC1 (d))I ∪ ans(hβiC2 (d))I . By induction hypoth- esis, I + |= (γC1 (d))I iff I + |= ans(hαiC1 (d))I and I + |= (γC2 (d))I iff I + |= ans(hαiC2 (d))I . Thus I + |= K I iff I + |= (ans(h(α, β)iK))I . – Let K = ∃R.C(d). Then K I = R(d, f∃R.C (d)) ∧ (γC (f∃R.C (d)))I and (ans(h(e, α)iK))I = {R(d, e)} ∪ (ans(hαiA(e)))I . Let us suppose that I + |= K I : then, we have I + |= R(d, f∃R.C (d)) and I + |= (γC (f∃R.C (d)))I . Thus, by (‡), I + |= R(d, e) and I + |= (γC (e))I . By induction hypothesis we have that I + |= ans(hαiC(e))I . Thus, we have that I + |= (ans(h(e, α)iK))I . Conversely, suppose that I + |= (ans(h(e, α)iK))I . Then we have I + |= R(d, e) and I + |= ans(hαiC(e))I . By definition of I + and induction hypothesis, we obtain that I + |= K I . I – If K = ∀G C, then KS = (γC (c1 ))I ∧ · · · ∧ (γC (cn ))I for {c1 , . . . , cn } = dom(G) and ans(hφiK) = e∈dom(G) (ans(hφ(e)iC(e)))I . By induction hypothesis, I for each e ∈ dom(G), I + |= (γC (e))I iff (ans(hφ(e)iC(e)))I . Thus, by the above definitions we have that, I + |= K I iff I + |= (ans(hφiK))I . t u Theorem 3. If I is an answer set for a formula K ∈ LN , then there exists η ∈ 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 I and thus, by Lemma 1, I |= K. By Theorem 2, then there exists η ∈ itN (K) s.t. I |= ans(hηiK). We can prove that I is minimal: suppose that J ⊆ I with J |= ans(hηiK). Then, by Theorem 2, J |= K. Let us show that J + |= (ans(hηiK))I . Consider H ∈ ans(hηiK). If H is atomic (and H is not ⊥(d)), then H I = H and thus it holds J + |= H I . Otherwise, if H = ¬C(d), since I + |= H I then we have H I = t and thus it holds J + |= H I . This proves that J + |= (ans(hηiK))I : thus, by Lemma 1, we obtain that J + |= K I . Since I is an answer set for K, then by definition we obtain J = I. t u Theorem 4. Let K be a positive 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 2, for every lp-interpretation I s.t. I |= ans(hηiK) 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 2, 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 Theorem 5. Let K be a formula of LN and hηiK be a minimal piece of infor- mation for K with answer set ans+ (hηiK). Then, ans+ (hηiK) is an answer set for K. Proof. Assuming that I = ans+ (hηiK) is an answer set for the minimal piece of information hηiK, then by definition I |= ans− (hηiK). Let us show that I is an answer set for K. By the condition above (and the definition of positive an negative answers), it holds that I |= ans(hηiK). Thus, by Theorem 2 we have I |= K and by Lemma 1, it holds that I + |= K I . To show that I is minimal, let us consider J ⊂ I s.t. J + |= K I . Then, by Theorem 2 and Lemma 1, there exists β ∈ itN (K) s.t. J + |= (ans(hβiK))I . This implies that: (a). J + |= (ans+ (hβiK))I (b). J + |= (ans− (hβiK))I Considering (a), we have that ans+ (hβiK)I = ans+ (hβiK) (i.e. the reduction does not change the positive contents of the set). Thus, ans+ (hβiK) ⊆ J ⊂ I. Moreover, considering (b) (and the fact that J is consistent), the reduct (ans− (hβiK))I = {t}. This implies that I |= ans− (hβiK): this is an absurd, as it would contradict the minimality condition of hηiK. t u Theorem 6. Let K be a 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 “if” direction: if hηiK is a minimal piece of information, I = ans+ (hηiK) is an answer set for K. Let us now prove the other direction and consider an answer set I for K: by definition, then I + |= K I . By Lemma 1, we have that there exists η ∈ itN (K) such that: (a). I + |= (ans(hηiK))I . Moreover, given that I is an answer set: (b). for every J ⊂ I, J + 6|= K I , that is for any β ∈ itN (K), J + 6|= (ans(hβiK))I . From (a) and the definition of the reduct, we have that (ans− (hηiK))I = {t}, and so I |= ans− (hηiK). From (b), for every J ⊂ I, J + 6|= (ans+ (hηiK))I , thus we have that I = ans+ (hηiK). We need to show that hηiK is minimal. It holds that I is an answer set for hηiK since I |= ans− (hηiK). Let us consider a piece of information hβiK s.t. ans+ (hβiK) ⊂ I. We have by (b) that, if J = ans+ (hβiK), J + 6|= (ans(hβiK))I : thus, in particular J + 6|= (ans− (hβiK))I . This means that f ∈ (ans− (hβiK))I and thus I 6|= ans− (hβiK). By definition of minimality, this implies that hηiK is minimal. t u