Il Milione: A Journey in the Computational Logic in Italy LOGICHE NON-CLASSICHE PER LA RAPPRESENTAZIONE DELLA CONOSCENZA E IL RAGIONAMENTO NON-CLASSICAL LOGICS FOR KNOWLEDGE REPRESENTATION AND REASONING Laura Giordano, Valentina Gliozzi, Nicola Olivetti, Gian Luca Pozzato, and Camilla B. Schwind 76 Il Milione: A Journey in the Computational Logic in Italy SOMMARIO/ABSTRACT munity, in the context of knowledge representation. In the following section, we describe the activity of our group in Riassumiamo brevemente la nostra attività di ricerca nel this area, concerning the use of modal, temporal, condi- campo delle logiche non-classiche iniziata negli anni ’90. tional and non-monotonic logics for Reasoning about Ac- In particolare, descriviamo la nostra ricerca riguardante tions and Change and for Belief Revision as well as in the l’applicazione delle logiche non-classiche alla rappresen- specification and verification of multi-agent systems. tazione della conoscenza e lo sviluppo di metodi di prova In section 3 we describe our activity regarding proof per logiche non-monotone e condizionali. methods for non-classical logics and, in particular, for KLM non-monotonic logics and for Conditional Logics. We briefly outline our research activity in the field of non- classical logics started in the 90s. In particular, we de- scribe our research in the application of non-classical log- 2 Knowledge Representation ics to knowledge representation and in the development of As mentioned above, our activity in Knowledge Represen- proof methods for non-monotonic and conditional logics. tation has been mainly concerned with the formalization of change, which is crucial both in the context of Reasoning Keywords: Non-classical logics, knowledge representa- about Actions as well as in the context of Belief Revision. tion, proof methods Concerning Reasoning about Actions, we have proposed a few modal and temporal formalisms for modelling ac- 1 Introduction tions execution. In modal and temporal action theories, action execution is modelled by introducing action modal- Our interest in the field of non-classical logic started with ities, and the Ramification problem is addressed by making our work in Logic Programming at the beginning of the use of modal or temporal operators (see section 2.1). Such 90s. At that time we were working with Alberto on ex- action theories have been used in the specification and ver- tensions of LP for dealing with hypothetical, conditional, ification of agent interaction protocols as well as in the defeasible and abductive reasoning. Those activities in- specification, verification and composition of web services clude the development of goal directed proof methods for (section 2.2). Concerning Belief Revision, our research has Horn like fragments of modal logics K, S4, S5 and their mainly focused on the relationships between Belief Revi- use in the definition of structuring constructs for logic pro- sion and Conditional Logics (section 2.3). In the following grams; the study of negation as failure in a hypothetical we describe the above activities, as well as our recent activ- logic programming (NProlog); the semantic characteriza- ity concerning reasoning about typicality and inheritance tion of truth maintenance systems (TMS), and its relation with exceptions in Description Logics (section 2.4). with stable model semantics; proof procedures for abduc- tive logic programming; and the definition of a conditional 2.1 Reasoning About Actions logic programming language (CondLP). Since that time, we have started working on non-classical logics both fo- The idea of representing actions as modalities comes from cusing on the use of such logics in knowledge representa- Dynamic Logics [15]. As observed in [17], classical dy- tion and on developing proof methods for the automatiza- namic logic adopts essentially the same ontology as Mc- tion of conditional and non-monotonic logics. Carthy’s situation calculus, by taking “the state of the Non-classical logics are widely used within the AI com- world as primary, and encoding actions as transformations 77 Il Milione: A Journey in the Computational Logic in Italy on states”. Indeed, actions can be represented in a natu- 2.3 Belief Revision ral way by modalities, and states as sequences of modal- A lot of work has been devoted to the problem of finding a ities. In this setting, the action law, saying that action a formal relation between Conditional Logics and Belief Re- has effect f when executed in a state in which P holds, vision [4, 18]. Conditional Logics provide a semantics to can be expressed by the formula: P → [a]f . Moreover, conditional sentences of the form “if A, then B”, denoted the precondition law, saying that action a is executable in by A ⇒ B. Belief Revision is the area of Knowledge a state in which condition C holds, can be expressed by Representation that deals with the problem of how to in- the formula: C →< a > f . Based on this idea, in [10] tegrate a new information in a given belief set. The most we have defined a modal action theory in which the frame problem is tackled by using a non-monotonic formalism known theory of Belief Revision is the so-called AGM the- ory (from Alchourrón, Gardenfors, and Makinson who first which maximizes persistency assumptions and the ramifi- proposed it) that specifies a set of rationality postulates for cation problem is tackled by introducing a modal causality integrating a new information about a static domain into a operator which is used to represent causal dependencies belief set of the same domain. among fluents. This action theory can also deal with in- complete initial state and with nondeterministic actions. The idea that there might be a relation between evalu- ation of conditional sentences and Belief Revision dates In [10], we have developed a temporal action theory back to Ramsey, who proposed an acceptability criterion based on a dynamic extension of Linear Temporal Logic for conditionals in terms of belief change. According to (LTL). This logic, called DLTL (Dynamic Linear Time this criterion, in order to decide whether to accept a con- Temporal Logic) [16], extends LTL by strengthening the ditional A ⇒ B in a belief set K, one should add A to K “until” operator by indexing it with regular programs. The by changing it as little as possible, and see if B follows. advantage of using a linear time temporal logic is that it If it does, one should accept the conditional, otherwise is a well established formalism for specifying the behav- one should reject it. In spite of the intuitiveness of Ram- ior of distributed systems, for which a rich theory has been sey’s criterion, its formalisation in the framework of Belief developed and the verification task can be automated by Revision is not straightforward. Many proposals, such as making use of automata based techniques. In particular, [4] run into the well-known Triviality Result, according to for DLTL, in [11] a tableau-based algorithm for obtaining which there is no interesting Belief Revision system com- a Büchi automaton from a formula in DLTL has been pre- patible with the proposed formalization. In [7, 8] we have sented, whose construction can be done on-the-fly, while proposed a Conditional Logic that corresponds to Belief checking for the emptiness of the automaton. Revision, thus establishing a relation between the two do- An alternative approach to reasoning about actions, mains, without running into the Triviality Result. based on Conditional Logics, has been proposed in [14]. 2.4 Reasoning About Typicality in Description 2.2 Specification and Verification of Agent Inter- Logics action Protocols The family of description logics (DLs) is one of the most The temporal action theory described above has been used important formalisms of knowledge representation. DLs in the specification and verification of communication pro- correspond to tractable fragments of first order logic, and tocols [12]. We have followed a social approach [22] to are reminiscent of the early semantic networks and of agent communication, where communication is described frame-based systems. They offer two key advantages: a in terms of changes to the social relations between par- well-defined semantics based on first-order logic and a ticipants, and protocols in terms of creation, manipulation good trade-off between expressivity and complexity. DLs and satisfaction of commitments among agents. The de- have been successfully implemented by a range of systems scription of the interaction protocol and of communicative and they are at the base of languages for the semantic web actions is given in a temporal action theory, and agent pro- such as OWL. grams, when known, can be specified as complex actions A DL knowledge base comprises two components: (i) (regular programs in DLTL). the TBox, containing the definition of concepts (and pos- We have addresses several kinds of verification prob- sibly roles), and a specification of inclusions relations lems, including run-time verification of protocols as well among them, and (ii) the ABox containing instances of as static verification of agent compliance with the proto- concepts and roles, in other words, properties and rela- cols. Some of these problems can be formalized either as tions of individuals. Since the very objective of the TBox validity or as satisfiability problems in the temporal logic is to build a taxonomy of concepts, the need of represent- and can be solved by model checking techniques. Other ing prototypical properties and of reasoning about defea- problems, as compliance, are more challenging and require sible inheritance of such properties naturally arises. The a special treatment [13]. The proposed approach has also traditional approach is to handle defeasible inheritance by been used in the specification of Web Services and, in par- integrating some kind of non-monotonic reasoning mech- ticular, for reasoning about service composition. anism. This has led to study non-monotonic extensions of 78 Il Milione: A Journey in the Computational Logic in Italy DLs. However, finding a suitable non-monotonic exten- A-worlds exist whenever there are A-worlds, by prevent- sion for inheritance reasoning with exceptions is far from ing infinitely descending chains of worlds. This condition obvious. therefore corresponds to the finite-chain condition on the In [5], we have considered a novel approach to defeasi- accessibility relation (as in modal logic G). ble reasoning based on the use of a typicality operator T. We have extended our approach to the cases of CL and The intended meaning is that, for any concept C, T(C) C by using a second modality which takes care of states singles out the instances of C that are considered as “typ- (intuitively, sets of worlds). Regarding CL, we have shown ical” or “normal”. Thus, an assertion as “normally stu- that we can map CL-models into P-models with an addi- dents do not pay taxes” is represented by T(Student) ⊑ tional modality. In both cases, we can define a decision ¬TaxPayer . The DL obtained is called ALC + T. procedure to solve the validity problem in CoNP. Also, we In the logic ALC + T, one can have consistent knowl- have given a labelled calculus for the strongest logic R, edge bases containing the inclusions T(Student) ⊑ where the preference relation is assumed to be modular. ¬TaxPayer ; T(Student ⊓ Worker ) ⊑ TaxPayer ; The calculus defines a systematic procedure which allows T(Student ⊓ W orker ⊓ ∃HasChild .⊤) ⊑ ¬TaxPayer , the satisfiability problem for R to be decided in nondeter- corresponding to the assertions: normally a student does ministic polynomial time. not pay taxes, normally a working student pays taxes, but From the completeness of our calculi we get for free the normally a working student having children does not pay finite model property for all the logics considered. With the taxes (because he is discharged by the government), etc.. exception of the calculus for C, in order to ensure termina- Furthermore, if the ABox contains the information that for tion, our tableau procedures for KLM logics do not need instance T(Student ⊓ Worker )(john), one can infer that any loop-checking, nor blocking, nor caching machinery. TaxPayer (john). Termination is ensured only by adopting a restriction on the order of application of the rules. 3 Proof Methods for Non-classical Logics 3.2 Proof Methods for Conditional Logics Our interest in the area of proof methods started with our work in Logic Programming In [20] we have introduced proof methods for some stan- At the beginning of the Nineties, our interest for proof dard Conditional Logics. We have considered the selection methods for non-classical logics were mainly devoted to function semantics. Intuitively, the selection function f se- extend goal directed proof methods to non-classical log- lects, for a world w and a formula A, the set of worlds ics, and, in particular to modal logics. In the same pe- f (w, A) which are “most similar to w” given the informa- riod, Dale Miller [19] was putting the basis of intuition- tion A. In this respect, the selection function can be seen istic logic programming, based on the idea of having uni- as a sort of modality indexed by formulas of the language. form proofs. Our work in this field was mainly concerned A conditional formula A ⇒ B holds in a world w if B with modal extensions of logic programmimg [1, 3] as well holds in all the worlds selected by f for w and A. as with abductive, hypothetical and conditional extension We have introduced cut-free sequent calculi for the ba- of logic programming [2]. In the following, we describe sic Conditional Logic CK and for some of its extensions, our more recent activity concerning proof methods for non- namely CK+{ID, MP, CS, CEM} including all the com- monotonic and conditional logics. binations of these extensions except those including both CEM and MP. Our calculi make use of labels representing 3.1 Proof Methods for KLM Logics possible worlds. Two types of formulas are involved in the In [9] we have introduced analytic tableau calculi for all rules of the calculi: world formulas of the form x : A, rep- non-monotonic logics introduced by Kraus, Lehmann, and resenting that A holds at world x, and transition formulas A Magidor (KLM). Such logics, namely R, P, CL, and C, of the form x −→ y, representing that y ∈ f (x, A). The have a preferential semantics in which a preference relation completeness of the calculi is an immediate consequence is defined among worlds or states. It has been observed that of the admissibility of cut. KLM logics correspond to the flat (i.e. unnested) fragment We have also shown that one can derive a decision pro- of well-known Conditional Logics. cedure from the cut-free calculi. Whereas the decidabil- Our tableau method provides a sort of run-time transla- ity of these systems was already proved by Nute (by a tion of P into modal logic G. The idea is simply to interpret finite-model property argument), our calculi give the first the preference relation as an accessibility relation: a con- constructive proof of decidability. As usual, the terminat- ditional A |∼ B holds in a model if B is true in all minimal ing proof search mechanism is obtained by controlling the A-worlds, where a world w is an A-world if it satisfies backward application of some critical rules. By estimating A, and it is a minimal A-world if there is no A-world w′ the size of the finite derivations of a given sequent, we have preferred to w. The relation with modal logic G is moti- also obtained a polynomial space complexity bound for the vated by the fact that we assume, following KLM, the so- logics considered. called smoothness condition, which ensures that minimal Our calculi can be the starting point to define goal- 79 Il Milione: A Journey in the Computational Logic in Italy oriented proof procedures, according to the paradigm of [9] L. Giordano, V. Gliozzi, N. Olivetti, and G.L. Pozzato. Miller’s Uniform Proofs recalled above. As a preliminary Analytic Tableaux Calculi for KLM Logics of Non- result, in [21] we have presented a goal-directed calculus monotonic Reasoning. ACM Transactions on Compu- for a fragment of CK and its extensions with MP and ID. tational Logic (ToCL), to appear. Proof methods for other Conditional Logics have been introduced in [6]. In detail, some labelled tableaux calculi [10] L. Giordano, A. Martelli and C. Schwind. Ramifica- have been defined for the Conditional Logic CE and its tion and causality in a modal action logic. Journal of main extensions, including CV, whose flat fragment corre- Logic and Computation, 10(5):625–662, 2000. spond, respectively, to KLM systems P and R. [11] L. Giordano, A. Martelli. Tableau-Based Automata Construction for Dynamic Linear Time Temporal 4 Conclusions and Future Works Logic. Annals of Mathematics and Artificial Intelli- gence, 46(3): 289-315 (2006). We believe that the temporal action theory we have devel- oped for the specification and verification of agent inter- [12] L. Giordano, A. Martelli, C. Schwind. Specifying action protocols can be profitably used in the specification and Verifying Interaction Protocols in a Temporal Ac- and verification of web services. In this context, new is- tion Logic, J. of Applied Logic, 5(2): 214-234 (2007). sues arise, as for instance the problem of modelling service composition and that of service compliance (which still re- [13] L. Giordano and A. Martelli. Verifying Agent Con- quires a general solution). formance with Protocols specified in a Temporal Ac- Concerning reasoning about typicality in description tion Logic. In AI*IA 2007. Proceedings., LNAI, 4733, logics, we are currently studying a minimal model seman- pp. 145-156, Springer, 2007. tics for ALC + T to maximize typical instances of a con- [14] L. Giordano and C. Schwind. Conditional logic of cept. By means of this semantics we are able to infer de- actions and causation. Artificial Intelligence, 157(1- feasible properties of (explicit or implicit) individuals. 2):239–279, 2004. REFERENCES [15] D. Harel. First order dynamic logic. In Extensions of Classical Logic, Handbook of Philosophical Logic II, [1] M. Baldoni, L. Giordano, and A. Martelli. A modal ex- pp. 497–604, 1984. tension of logic programming: Modularity, beliefs and hypothetical reasoning. Journal of Logic and Compu- [16] J.G. Henriksen and P.S. Thiagarajan, Dynamic Linear tation, 8(5):597–635, 1998. Time Temporal Logic. Annals of Pure and Applied logic, 96(1-3):187–207, 1999. [2] D.M. Gabbay, L. Giordano, A. Martelli, N. Olivetti and M.L. Sapino. Conditional reasoning in Logic Pro- [17] L.T. McCarty. Modalities over actions, I. model the- gramming. J. of Logic Programming, 44(1-3):37–74, ory. KR ’94, Proceedings, pp. 437–448, 1994. 2000. [18] D. Makinson. The Gärdenfors impossibility theorem [3] D.M. Gabbay and N. Olivetti. Goal-Directed Proof in non-monotonic contexts. Studia Logica, 49(1):1–6, Theory (Applied Logic Series V. 21) , Springer, 2000. 1990. [4] P. Gärdenfors. Belief Revisions and the Ramsey Test [19] D. Miller, G. Nadathur, F. Pfenning, and A. Scedrov. for Conditionals. Philosoph. Review, 95:81–93, 1986. Uniform Proofs as a Foundation for Logic Program- ming. Annals of Pure and Applied Logic, 51(1-2):125– [5] L. Giordano, V. Gliozzi, N. Olivetti, and G.L. Poz- 157, 1991. zato. Preferential Descritpion Logics. In LPAR 2007. LNAI, 4790, pp. 257-272, Springer, 2007. [20] N. Olivetti, G.L. Pozzato, and C.B. Schwind. A Se- quent Calculus and a Theorem Prover for Standard [6] L. Giordano, V. Gliozzi, N. Olivetti, and Conditional Logics. ACM Transactions on Computa- C.B. Schwind. Tableau Calculi for Preference- tional Logic (ToCL), 8(4):22/1–22/51, 2007. Based Conditional Logics. In TABLEAUX 2003, LNAI, 2796, pp. 81-101, Springer, 2003. [21] N. Olivetti and G.L. Pozzato. Theorem Proving for Conditional Logics: CondLean and G OAL DUCK. J. [7] L. Giordano, V. Gliozzi, and N. Olivetti. Iterated Be- of Applied Non-Classical Logics (JANCL), to appear. lief Revision and Conditional Logic. Studia Logica, 70(1):23–47, 2002. [22] M. P. Singh. A Social Semantics for Agent Commu- nication Languages. Issues in Agent Communication [8] L. Giordano, V. Gliozzi, and N. Olivetti. Weak AGM 2000, pp. 31-45. postulates and strong Ramsey Test: A logical formal- ization. Artificial Intelligence, 168(1-2):1–37, 2005. 80 Il Milione: A Journey in the Computational Logic in Italy 5 Contacts Laura Giordano Dipartimento di Informatica - Università del Piemonte Orientale “A. Avogadro” via Bellini 25/G - 15100 Alessandria - Italy Email: laura@mfn.unipmn.it Valentina Gliozzi Dipartimento di Informatica - Università degli Studi di Torino - Italy corso Svizzera 185 - 10149 Turin Email: gliozzi@di.unito.it Nicola Olivetti LSIS - UMR CNRS 6168 Université Paul Cézanne (Aix-Marseille 3) - France Avenue Escadrille Normandie-Niemen 13397 Marseille Cedex 20 Email: nicola.olivetti@univ.u-3mrs.fr - nicola.olivetti@lsis.org Gian Luca Pozzato Dipartimento di Informatica - Università degli Studi di Torino - Italy corso Svizzera 185 - 10149 Turin Email: pozzato@di.unito.it Camilla B. Schwind École d’Architecture de Marseille - Luminy - France 184 avenue de Luminy - 13288 Marseille Cedex 9 Email: Camilla.Schwind@map.archi.fr L. Giordano got the Ph.D. in Computer Science from the Università degli Studi di Torino in 1993. Since 1998 she is Professore Associato at the Facoltà di Scienze Matematiche, Fisiche e Naturali, Università del Piemonte Orientale - Amedeo Avogadro. Her research interests include: Non-monotonic Reasoning, Belief Revision, Reasoning about Action and Change, Multiagent Systems, Proof Methods for non-classical logics. V. Gliozzi graduated in Philosophy at the Università degli Studi di Torino in 1997, and she got the Ph.D. in Computer Science from the same university in 2002 (with a thesis on Belief Revision and Conditional Logics). Since 2005 she is a researcher at the Department of Computer Science at Università di Torino. Her main research interests include logic, knowledge representation, non-classical logics. N. Olivetti got the Ph.D. in Computer Science from the Università degli Studi di Torino in 1995. He is a Professor of Computer Science at the Paul Cézanne University (Aix-Marseille, France), and he is a member of the CNRS laboratory LSIS. His main research interests are automated deduction for non-classical logics (conditional, substructural, and many- valued logics), foundation and proof-theory of non-monotonic reasoning, extensions of logic programming, and Belief Revision. G.L. Pozzato was born in Moncalieri (Turin) in 1978. He took his “Laurea” degree “summa cum laude” in Computer Science in 2003, and his Ph.D. in Computer Science in 2007, both at the Università degli Studi di Torino. Since 2007 he is a researcher at the Department of Computer Science of the Università degli Studi di Torino. His research interests include non-monotonic reasoning, non-classical logics, proof-theory, and Description Logics. C. B. Schwind is a researcher of Computer Science at the CNRS laboratory LIF (Marseille, France). Her main research interests are: Conditional Logic, Multi-agent systems, and analytic tableaux for non-monotonic and conditional logics. She has also been actively involved in basic research in the following topics: Natural Language Understanding, Temporal and Modal Logics, Deductive Data Bases, Computer Assisted Language Learning, Action Logics and the Frame Problem, Modal Non Monotonic Logics. 81