=Paper=
{{Paper
|id=Vol-487/paper-14
|storemode=property
|title=Non-Classical Logics for Knowledge Representation and Reasoning
|pdfUrl=https://ceur-ws.org/Vol-487/paper14.pdf
|volume=Vol-487
|dblpUrl=https://dblp.org/rec/conf/birthday/0001GOPS08
}}
==Non-Classical Logics for Knowledge Representation and Reasoning==
https://ceur-ws.org/Vol-487/paper14.pdf
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