Connections Between Answer Set Semantics and Information Terms Semantics in Constructive E L? (Extended Abstract)

Abstract

Constructive description logics are interpretations of description logics (DLs) under appropriate constructive semantics. The application of such non-classical semantics to description logics is motivated by the interest in using the formal properties of constructive semantics in knowledge representation. Starting from di erent constructive semantics, several constructive description logics have been proposed, see e.g. [4,6,11]. 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., [2,8,9,10]); however, the interaction between formal and practical aspects of constructive DLs has been scarcely investigated in the literature. To bridge this gap, in [1] we have proposed a simple constructive DL based on E L and we have discussed its relationship with Answer Set Programming (ASP). Exploiting such a connection, we have presented a Datalog encoding managing a reasoning task over the constructive semantics (namely, the generation of \valid states" of a knowledge base) and we have provided a prototype based on the standard OWL-EL pro le, together with \o the shelf" tools for manipulation of OWL 2 ontologies and ASP reasoning. Our constructive interpretation of E L is based on information terms (ITs) semantics [3,6,12], a constructive semantics related to the BHK (Brower-HeytingKolmogorov) interpretation of logical connectives [13]. 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, let us consider the E L concept 9R:C and the formula 9R:C(d), to be understood as \the individual d belongs to 9R:C". The validity of 9R:C(d) in a model M can be explained by an information term (e; ) providing the ller e such that (dM; eM) (the pair of elements interpreting d and e in M) belongs to RM (the relation interpreting R in M) and, inductively, an information term justifying the validity of the formula C(e). Information terms have been used to represent the state or answer of a formula (and, by extension, a notion of \snapshot" representing a valid state of a knowledge base). The relation between information terms and answer sets

-

semantics has been rstly studied in [ 7 ], where propositional theories are considered. Along these lines, [ 1 ] extends this approach, for the rst time, to the context of constructive description logics.

In this work, we continue the investigation started in [ 1 ] 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?. Similarly to [ 3,6 ], negated formulas of the kind :C(d) are treated akin to atomic formulas with respect to their IT interpretation: 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.

We can then show how the results linking IT semantics and answer sets semantics can be extended in presence of negative information. Following [ 7 ], 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. Intuitively, as a result, we can show that the answer sets of an E L? formula K (and, by extension, of an E L? KB) correspond to the \positive answers" encoded by the minimal ITs of K that respect such negative constraints.

We note that the constructive reading of formulas provided by information terms 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 [ 5 ], 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.

This ongoing work represents a rst step towards the extension of this approach 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 terms semantics presented in [ 6 ]. An other issue to be investigated is the application of the mentioned formal results to representation and reasoning tasks, for example by extending the Datalog encoding and prototype discussed in [ 1 ] for ASP based generation of information terms. We also aim at developing procedures for the manipulation of information terms (see, e.g., [ 2 ]), in order to apply IT semantics in concrete problems.

An extended version of this paper is available at https://dkm.fbk.eu/technologies/ constructive-description-logics.

References

1. Bozzato , L. : ASP based generation of information terms for constructive EL . Fundam. Inform . 161 ( 1-2 ), 29 { 51 ( 2018 )

2. Bozzato , L. , Ferrari , M. : Composition of semantic web services in a constructive description logic . In: RR2010. LNCS , vol. 6333 , pp. 223 { 226 . Springer ( 2010 )

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. , Ferrari , M. , Fiorentini , C. , Fiorino , G.: A decidable constructive description logic . In: JELIA 2010. LNCS , vol. 6341 , pp. 51 { 63 . Springer ( 2010 )

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

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

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

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

9. Hilia , M. , Chibani , A. , Djouani , K. , Amirat , Y. : Semantic service composition framework for multidomain ubiquitous computing applications . In: ICSOC 2012. LNCS , vol. 7636 , pp. 450 { 467 . Springer ( 2012 )

10. 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 )

11. Mendler , M. , Scheele , S. : Towards Constructive DL for Abstraction and Re nement . J. Autom. Reasoning 44 ( 3 ), 207 { 243 ( 2010 )

12. 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 )

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