Reasoning on Information Term Semantics with ASP for Constructive E L?

Abstract

Constructive description logics represent di erent re-interpretations of description logics (DLs) under constructive semantics. Constructive 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?.

Introduction

Constructive description logics are interpretations of description logics (DLs) under di erent constructive semantics. The application of such non-classical semantics to description logics is motivated by the interest in applying the formal properties of constructive semantics to di erent aspects of knowledge representation. Starting from di erent constructive semantics, several constructive description 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 di erent 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 E L 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 pro le and \o the shelf" tools for manipulation of OWL 2 ontologies and ASP reasoning.

Our constructive interpretation of E L is based on information term semantics [ 5,9 ]: the information terms (ITs) are syntactical objects that provide a constructive justi cation for the classical truth of a formula. Information terms have been used to represent the state or answer of a formula (and, for extension, a notion of \snapshot" representing a valid state of a knowledge base). In particular, [ 2 ] follows the direction studied in [ 10 ], where the relation between information term and answer set semantics has been rst studied over propositional theories. In fact, we remark that [ 2 ] extends for the rst 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 rst step we introduce falsum in E L, thus providing a constructive interpretation for the DL E L?. 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 E L? in presence of negative information. These connections can be then leveraged to reason on the constructive reading of E L? 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 rst present (see Section 2) the de nition of the IT interpretation of E L? (that we call E Lc?); then, in Section 3 we extend the de nition 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 E Lc?. Finally, in Section 4 we brie y discuss how to extend to E Lc? 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 E Lc?

We present a constructive semantics based on information term semantics (as in BCDL [ 9 ]) for the description logic E L? [ 1 ]; we refer to this logic as E Lc?. 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. In addition, we introduce a set NG of special concepts, called generators, where NG \ NC = ;. Generators are used in the de nition of a limited form of subsumption, which facilitates the characterization of the logic in a constructive semantics. A generator G is an atomic concept associated with a nite set of individual names dom(G) (the domain of G) which xes the interpretation of G. In our language, we use bounded quanti ed formulas of the kind 8GC, meaning that every element of dom(G) belongs to the concept C; thus, the formula 8GC can be read as the subsumption relation G v C.3

In the language L for E Lc?, concepts C are inductively de ned as:

C ::= > j ? j A j :C1 j C1 u C2 j 9R:C1 where A 2 NC [ NG and R 2 NR.4 The formulas K of L are de ned as:

K ::= R(c; d) j C(c) j 8GC where c; d 2 NI, R 2 NR, G 2 NG and C is a concept (as de ned above). We point out that 8GC 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 2 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 nite 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 2 NR, c; d 2 NI and C is a concept. The TBox contains formulas of the kind 8GC, representing subsumption axioms.

In the following we refer to languages LN restricted to nite subsets N of NI. Given a nite N NI, let NGN be the set of generators G 2 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; 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 de ned as usual: ?M = ;

>M = (9R:C)M = fc 2

M (C1 u C2)M = C1M \ C2M (:C)M =

M n CM M j 9d 2

M s.t. (c; d) 2 RM, d 2 CMg A formula K is valid in M, written M j= K, i one of the following conditions holds:

M j= R(c; d) i (cM; dM) 2 RM

M j= C(d) i M j= 8GC i dM 2 CM GM

CM If is a set of formulas, M j= means that M j= K, for every K in . 3 While non-conventional in DL languages, as noted in [ 9 ], the de nition of generators with a xed domain simpli es the following presentations of the constructive semantics. Alternatively, domain of generators can be de ned 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 C1 and the axiom C1 u C1 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 information to introduce constraints. The set NI contains names for wines, colors and regions. The set NC contains the concepts Wine, de ning wines, and ExcRegion, de ning regions to be excluded. We introduce the generators Food and Color , de ning foods and colors respectively, and we set: dom(Food ) = f sh; meat g and dom(Color ) = fred ; whiteg, where sh, 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) (Ax2)

8Food 9goesWith:Color

8Color 9isColorOf :(Wine u :(9hasRegion: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 originating 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) Wine(chardonnay ) Wine(cabernet ) hasRegion(barolo; piedmont ) hasRegion(chardonnay ; lombardy ) hasRegion(cabernet ; california) isColorOf (red ; barolo) isColorOf (white; chardonnay ) isColorOf (red ; cabernet ) goesWith( sh; white) goesWith(meat ; red ) ExcRegion(california) We can take as N any nite set containing individual names occurring in the ABox. We point out that a classical model M for KW must interpret the generator Food as the set f shM; meat Mg and Color as fred M; whiteMg. Instead, ExcRegion can be interpreted by any superset of fcaliforniaMg satisfying the axioms. 3 Information term semantics. The constructive semantics for E Lc? 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 justi es the truth of K in a classical model M. For instance, the validity of the formula 9R:C(d) in a model M can be explained by an information term (e; ) providing the ller e s.t. (dM; eM) 2 RM and, inductively, an information term justifying eM 2 CM. A simple formula K does not need any constructive explanation, thus the associated information term is an atom, denoted by tt. Given a nite subset N of NI and a formula K of LN , we de ne the set of information terms itN (K) by induction on K as follows.

itN (K) = f tt g; if K is a simple 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 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 veri ed by the models of the knowledge base.

The justi cation 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 2 itN (K). We de ne the realizability relation M h i K by induction on the structure of K:

M htti K i

M j= K; where K is a simple formula M

h( ; )i C1 u C2(c) i M h(d; )i 9R:C(c) i

M M j= R(c; d) and M h i C1(c) and M

h i C2(c) h i C(d) M h i 8GC i , for every d 2 dom(G), M h (d)i C(d) Example 2. Let us consider the knowledge base KW de ned in Example 1. An element 2 itN (Ax1) is a function mapping each food f 2 dom(Food ) to an information term (f ) 2 itN (9goesWith:Color (f )). Thus, every (f ) has the form (c; tt), meaning that c is a proper color for f . An element 1 2 itN (Ax1) is:

[ sh 7! (white; tt); meat 7! (red ; tt) ] Similarly, we can de ne 2 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 subconcept of Ax2. We point out that every model M of the ABox of KW satis es both M h 1i Ax1 and M h 2i 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 nite subset of NI, K a formula of LN and

itN (K). For every model M, M h i K implies M j= K. 2 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 rst-order translation of E Lc? formulas (see similar translations in [ 3 ]), that we exploit as an intermediate representation to de ne the notion of reduction of a formula. Let N be a nite subset of NI. By L1N we denote the rst-order language having constants N , a unary predicate symbol A, for every A 2 NC [ NG, a binary relation symbol R, for every R 2 NR, the logical constants t (true) and f (false), the connectives : and ^. We also introduce unary function symbols f9R:C to be used as Skolem functions to properly translate existential concepts 9R:C. Firstly, we introduce the translation C mapping a concept C to a rst-order formula F of L1N , having 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) C1 u C2 7!

> 7! C1 ^ C2 t

? 7! 9R:C 7! f :C 7!

: C R(x; f9R:C (x)) ^ C (f9R:C (x)) In translating C, we stipulate that di erent occurrences of the same existential subformulas 9R:D of C are associated with di erent Skolem function (e.g., f91R:D, f92R:D, and so on). Given a formula K 2 LN , the rst-order translation (K) of K is de ned as follows:

C(d) 7! 8GC 7!

C (d) C (c1) ^

R(c; d) 7! R(c; d) ^ C (cn); where fc1; : : : ; cng = dom(G) Example 3. Let KW be the knowledge base from Example 1. The rst-order translation of Ax1 is (C = 9goesWith:Color ): (Ax1) =

C (meat ) ^ C ( sh)

C = goesWith(x; fC (x)) ^ Color (fC (x)) Similarly, Ax2 is translated as follows:

D = 9isColorOf :(Wine u :E )

E = 9hasRegion: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)) ) An interpretation I for LN 1 1 is a classical interpretation for the language LN satisfying the following condition:

for each generator G 2 NGN , I j= G(c) i c 2 dom(G) Next proposition states the correspondence between rst-order translation and classical semantics: Proposition 2. Let K be a formula of LN .

(i). If M j= K, then there is an interpretation I for L1N such that I j= (K). (ii). If I j= (K), with I an interpretation for L1N , then there is an interpretation M for LN such that M j= K. 3 ( )

Answer Set Semantics for Formulas and Information

Terms

Following the construction in [ 10 ], we adapt the de nitions concerning logic programs with nested expressions [ 14 ] to E Lc? formulas. The rst step to de ne a notion of answer sets for E Lc? formulas is thus to de ne a notion of interpretation 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 2 NC [ NG, R 2 NR and c; d 2 N . Given a formula K of LN , the satis ability relation I j= K, and its extension to sets of formulas , is de ned as follows:

I j= >(c) for every c 2 N I j= H i H 2 I, where either H = A(c) and A 2 NC [ NG, or H = R(c; d) I j= G(c) i c 2 dom(G), where G 2 NG I j= :C(c) i I 6j= C(c) I j= C u D(c) i I j= C(c) and I j= D(c) I j= 9R:C(c) i there is d 2 N such that R(c; d) 2 I and I j= C(d) I j= 8GC i for every e 2 dom(G); I j= C(e)

I j= i I j= K for every K 2 We remark that I 6j= ?(c), for every c 2 N ; moreover, I satis es condition ( ) of previous section. The de nition of J 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 2 NC [ NG, R 2 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-interpretation over L1N obtained by properly interpreting Skolem functions. More speci cally, I+ is the smallest extension of I satisfying the following property: for every formula K = 9R:C(c) of LN such that I j= K, let d such that R(c; d) 2 I and I j= C(d), and let fK be a Skolem function associated with 9R:C; then, I+ contains the formulas R(c; fK (c)) and d = fK (c).

The reduct of a formula K 2 LN w.r.t an lp-interpretation I, denoted by KI , 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 1 w.r.t. an lp-interpretation J (over L1N ), denoted by F J , is the formula oFf 2L1NLNinductively de ned as follows:5

HJ = H; if H is an atomic formula of L1N (:C)J = f if J j= C t otherwise (C ^ D)J = CJ ^ DJ We de ne the reduct on formulas K of LN and set of formulas as follows: KI = ( (K))I+

I = f KI j K 2 g 5 Atomic formulas of L1N are the -images of atomic formulas of LN . We remark that, for positive formulas K, we have KI = (K).

Example 4. We show the de nition of reduct of axioms in KW (see Example 1) based on the rst-order translation displayed in Example 3. Let I be the lp-interpretation coinciding with the ABox of KW . The extension I+ is obtained by adding to I the formulas (D = 9isColorOf :(Wine u :E ) and E =

9hasRegion: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 ; : : : The reduction KWI is computed as follows: since Ax1 is a positive formula, then AxI1 = (Ax1). Instead, AxI2 coincides with the formula (Ax2)I+ such that: (Ax2)I+

= ( D(red ))I+ ^ ( D(white))I+ ( D(red ))I+ ( D(white))I+ = isColorOf (red ; fD(red)) ^ Wine(fD(red)) ^ t = 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 2 fred ; whiteg, I+ 6j= (hasRegion(c; fE (c)) ^ ExcRegion(fE (c)). 3 We introduce the notion of answer set for formulas: De nition 1. An lp-interpretation I is an answer set for a set of positive formulas LN (resp. L1N ) i I j= and, for every I0 I, I0 j= implies I0 = I. An lp-interpretation I is an answer set for a set of formulas LN i I+ is an answer set for I .

In the following we want to extend this notion of answer set to pieces of information. We call piece of information over LN an expression of the kind h iK with K 2 LN a formula and 2 itN (K). Given a piece of information h iK, the following de nes the sets of answers ans(h iK) obtainable from it: ans(httiK) = fKg; with K a simple 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 nite 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 itN (Ax2) de ned in Example 2; we have: H1 = 9goesWith:Color H2 = 9isColorOf :H3 H3 = Wine u :(9hasRegion:ExcRegion) ans(h 1iAx1) = ans(h 1( sh)i H1( sh)) [ ans(h 1(meat )i H1(meat )) 1 2 itN (Ax1) and = ans(httiColor (white)) [ f goesWith( sh; white) g [

ans(httiColor (red )) [ f goesWith(meat ; red ) g = f Color (white); goesWith( sh; white);

Color (red ); goesWith(meat ; red ) g ans(h 2iAx2) = ans(h 2(red )i H2(red )) [ ans(h 2(white)i H2(white)) = f isColorOf (red ; barolo) g [ ans(h(tt; tt)iH3(barolo)) [

f isColorOf (white; chardonnay ) g [ ans(h(tt; tt)iH3(chardonnay ))g = f isColorOf (red ; barolo); Wine(barolo); :(9hasRegion:ExcRegion)(barolo); isColorOf (white; chardonnay ); Wine(chardonnay ); :(9hasRegion:ExcRegion)(chardonnay ) g 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 model M, M h i K i

nite subset of NI, K a formula of LN . For every

M j= 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 satis ability of a nite 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 nite subset of NI, K a formula of LN . For every lp-interpretation I, I j= K i there exists an information term 2 itN (K) such that I j= ans(h iK).

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

De nition 2. Let K be a formula of LN and K 2 itN (K). An lp-interpretation

I is a minimal model of h iK i : { I j= ans(h iK) and, { for every lp-interpretation I0

I, I0 j= ans(h iK) implies I0 = I.

Note that, by Theorem 1, this de nition implies that, for every model M for LN such that M j= I, it holds that M h i K.

nite subset of NI, K a formula of LN and I an lp

In the other direction, we need to de ne a notion of minimality on pieces of information and introduce default reasoning as follows.

De nition 3. Let K be a positive formula of LN . A piece of information h iK is minimal i there is no 0 2 itN (K) such that ans(h 0iK) 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 de ned as follows: ans+(h iK) = f H 2 ans(h iK) j H = A(c), with A 2 NC [ NG, or H = R(c; d) g ans (h iK) = f H 2 ans(h iK) j H = :C(d) or H = ?(d) g Note that ans+(h iK) is an lp-interpretation.

Example 6. The set ans(h 2iAx2) in Example 5 can be partitioned into positive answers and constraints as follows: ans+(h 2iAx2) = f isColorOf (red ; barolo); Wine(barolo);

isColorOf (white; chardonnay ); Wine(chardonnay ) g ans (h 2iAx2) = f :(9hasRegion:ExcRegion)(barolo); :(9hasRegion:ExcRegion)(chardonnay ) g 3 We introduce the notion of answer set and minimality concerning pieces of information.

De nition 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 i ans+(h iK) j= ans (h iK).

De nition 5. Let K be a formula of LN . A piece of information h iK is min

imal i , for every 0 2 itN (K) such that ans+(h 0iK) ans+(h iK), it holds that ans+(h iK) 6j= ans (h 0iK).

Using these de nitions, 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 i there exists

a minimal piece of information h iK such that I = ans+(h iK). 4

Discussion: ASP based IT generation for E Lc?

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 E Lc? knowledge base consists in computing its answer sets and then, by exploiting the recursive de nition of ans(h iK), reconstruct the corresponding (minimal) information term .

In [ 2 ] we have presented alternative datalog encodings for an input E L knowledge base in order to generate its answer sets and build minimal information terms from them. In the case of negative information of E Lc?, we need to adapt the datalog encoding in order to consider the constraints provided by the negative sub-formulas, so that the candidate answer sets not matching the constraints are discarded. A possible way to encode negative constraints, re ecting the definition of reduct KI 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) check (a; lD)

nom(a); not 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 de nition of a suitable datalog encoding for E Lc? 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).

Conclusions

In this paper we present the relation between answer set semantics and information term semantics in the context of the description logic E L?. Following [ 2 ], we rst provide the de nition of the information term semantics for E L?. Then, we show how to extend the results presented in [ 2 ] concerning the correspondence between answer set semantics and information term semantics to E L?. By introducing a notion of reduction, similar to the one used in Answer Set Programming, 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 brie y discuss how these results can be used to generate the information terms of an input KB over E Lc?.

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 eld 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 rst 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.

Appendix: Proofs

Lemma 1. Let N be a nite subset of NI, K a formula of LN and I an lp

interpretation. Then: (i). We rst note that, by the de nition of I+, if fD(d) = e in I+, then fD(d) behaves like e in I+, namely: (z) for every concept C, I j= C(e) i I+ j= 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 j= :C(d), then by de nition I 6j= C(d). By induction hypothesis, I+ 6j= (C(d)), which implies I+ j= : (C(d)), namely I+ j= (:C(d)). Similarly, if I+ j= (:C(d)), we conclude I j= :C(d). { Let K = C1 uC2(d). Note that (C1 uC2(d)) = (C1(d))^ (C2(d)). If I j= K, then I j= C1(d) and I j= C2(d). By induction hypothesis, I+ j= (C1(d)) and I+ j= (C2(d)). Conversely, if I+ j= (K), we get I j= K. { Let K = 9R:C(d). Note that (K) = R(d; f9R:C (d)) ^ C (f9R:C (d)). Let us assume I j= 9R:C(d). By hypothesis, there exists e 2 N such that R(d; e) 2 I and I j= C(e). By induction hypothesis and the de nition of the extension I+, I+ j= R(d; e) and I+ j= (C(e)). BCy((fz9)R,:Cw(edg))e;t wI+e cj=onRcl(udd;ef9IR+:C =(d)) and I+ j= (C(f9R:C (d))), namely I+ j= j (K). Conversely, let us assume I+ j= (K). Then, I+ j= R(d; f9R:C (d)) and I+ j=

C (f9R:C (d)). By the de nition of I+, I contains a formula of the kind R(d; e) and, by (z), we get I+ j= C (e). By induction hypothesis we get I j= C(e), thus I j= 9R:C(d). { Let K = 8GC. 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 j= F i I j= F I . Thus, I j= K i I+ j= (K) (by point (i)), i I+ j= ( (K))I+ (by the previous remark), i I+ j= KI (by de nition of KI ). (iii). Considering the de nition of ans and reduction KI , we show the claim by induction on the structure of K (and de nition of ans): { Let K be atomic. Then we have that KI = K and (ans(httiK))I = fKg thus the claim immediately follows. { Let K = :C(d). Since K is a simple formula, we have that (ans(httiK))I = fKgI . Thus, it immediately follows that I+ j= KI i I+ j= (ans(httiK))I . { Let K = C1 u C2(d). Then we have KI = ( C1 (d))I ^ ( C2 (d))I and (ans(h( ; )iK))I = ans(h iC1(d))I [ ans(h iC2(d))I . By induction hypothesis, I+ j= ( C1 (d))I i I+ j= ans(h iC1(d))I and I+ j= ( C2 (d))I i I+ j= ans(h iC2(d))I . Thus I+ j= KI i I+ j= (ans(h( ; )iK))I . { Let K = 9R:C(d). Then KI = R(d; f9R:C (d)) ^ ( C (f9R:C (d)))I and (ans(h(e; )iK))I = fR(d; e)g [ (ans(h iA(e)))I .

Let us suppose that I+ j= KI : then, we have I+ j= R(d; f9R:C (d)) and I+ j= ( C (f9R:C (d)))I . Thus, by (z), I+ j= R(d; e) and I+ j= ( C (e))I . By induction hypothesis we have that I+ j= ans(h iC(e))I . Thus, we have that IT+hejn=w(eanhsa(vhe(eI;+ )=iKR)()dI;. eC) oannvderIs+ely=, saunpsp(hoseiCt(hea)t)II.+Byj=de(annist(ioh(ne;of )Ii+Ka))nId.

j j induction hypothesis, we obtain that I+ j= KI . { If K = 8GC, then KI = ( C (c1))I ^ ^ ( C (cn))I for fc1; : : : ; cng = dom(G) and ans(h iK)I = Se2dom(G)(ans(h (e)iC(e)))I . By induction hypothesis, for each e 2 dom(G), I+ j= ( C (e))I i (ans(h (e)iC(e)))I . Thus, by the above de nitions we have that, I+ j= KI i I+ j= (ans(h iK))I . tu

Theorem 3. If I is an answer set for a formula K 2 LN , then there exists

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= KI and thus, by Lemma 1, I j= K. By Theorem 2, then there exists 2 itN (K) s.t. I j= ans(h iK).

We can prove that I is minimal: suppose that J I with J j= ans(h iK). Then, by Theorem 2, J j= K. Let us show that J + j= (ans(h iK))I . Consider H 2 ans(h iK). If H is atomic (and H is not ?(d)), then HI = H and thus it holds J + j= HI . Otherwise, if H = :C(d), since I+ j= HI then we have HI = t and thus it holds J + j= HI . This proves that J + j= (ans(h iK))I : thus, by Lemma 1, we obtain that J + j= KI . Since I is an answer set for K, then by de nition we obtain J = I. tu

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 j= ans(h iK) 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 2, 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

Proof. Assuming that I = ans+(h iK) is an answer set for the minimal piece of information h iK, then by de nition I j= ans (h iK). Let us show that I is an answer set for K.

By the condition above (and the de nition of positive an negative answers), it holds that I j= ans(h iK). Thus, by Theorem 2 we have I j= K and by Lemma 1, it holds that I+ j= KI .

To show that I is minimal, let us consider J I s.t. J + = KI . Then, by Theorem 2 and Lemma 1, there exists 2 itN (K) s.t. J + j=j (ans(h iK))I . This implies that: (a). J + j= (ans+(h iK))I (b). J + 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 = ftg. This implies that I j= ans (h iK): this is an absurd, as it would contradict the minimality condition of h iK. tu

Theorem 6. Let K be a formula of LN . I is an answer set for K i 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 de nition, then I+ j= KI . By Lemma 1, we have that there exists 2 itN (K) such that: (a). I+ j= (ans(h iK))I .

Moreover, given that I is an answer set: (b). for every J

I, J + 6j= KI , that is for any 2 itN (K), J + 6j= (ans(h iK))I .

From (a) and the de nition of the reduct, we have that (ans (h iK))I = ftg, and so I j= ans (h iK).

From (b), for every J I, J + 6j= (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 j= 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 + 6j= (ans(h iK))I : thus, in particular J + 6j= (ans (h iK))I . This means that f 2 (ans (h iK))I and thus I 6j= ans (h iK). By de nition of minimality, this implies that h iK is minimal.

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 . Fundam. Inform., 161 ( 1-2 ): 29 { 51 , 2018 .

3. L. Bozzato , T. Eiter , and L. Sera ni. Reasoning with Justi able Exceptions in EL? Contextualized Knowledge Repositories . In Description Logic, Theory Combination, 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 language . 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 semantics . In ASP2007: Answer Set Programming , Advances in Theory and Implementation , 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 Computer 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 Re nement . 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 .