In this chapter we shall occupy ourselves with default reasoning, or reasoning by default. In fact we indicate how default logic can be based on epistemic logic, and particularly how we may employ Halpern & Moses' minimal epistemic states for this purpose. In this way we obtain a simple and natural S5-based logic for default reasoning that is well-behaved in a certain way. (We show the logic to be cumulative in the sense of Kraus, Lehmann and Magidor [KLM90].)

Default logic, autoepistemic logic (AEL) and other approaches to non-monotonic reasoning suffer from a technical complexity that is not in line with naive common-sense reasoning. They employ fixed-point constructions or higher-order logic in order to define the belief sets that one would like to associate with some base set of knowledge.

Here we present a modal logic, called EDL, which is an extension of the epistemic logic of Chapter 1. The logic EDL was introduced in [MH91a, MH92], and in [MH93a, 95] we connected it to the theory of Halpern & Moses, as treated in Section 3.1, to obtain a logic for default reasoning. The combined approach is relatively simple compared with AEL, but, more importantly, it is better suited as a default logic than AEL, as we shall show subsequently.

Our approach — unlike AEL — does not involve any fixed points or higher-order formulas. The basis for this logic is the simple S5-modal logic of Chapter 1. EDL contains a knowledge (certainty) operator and (dual) possibility operator.

Epistemic logic concerns the notions knowledge and belief ('επιστημη — episteme — is Greek for ‘knowledge’), and stems from philosophy where it has been developed to give a formal treatment of these notions. (Sometimes the logic of belief is separately referred to as doxastic logic, from the Greek word δoξα — doxa —, meaning ‘surmise’ or ‘presumption’. In this book we shall use epistemic logic for the logic of knowledge and belief.) In [Hin62] the Finnish logician and philosopher Jaakko Hintikka presented a logic for knowledge and belief that was based on modal logic. Modal logic is a so-called philosophical logic dealing with the notions of necessity and contingency (possibility) ([Kri63], [Che80], [HC68, HC84]), and it appeared that epistemic logic could be viewed as an instance of this more general logic by interpreting necessity and possibility in an epistemic manner. For a thorough treatment of epistemic logic from the perspective of philosophy we refer to [Len80].

Especially in the last decade the use of logic and logìcal formalisms in artificial intelligence (AI) has increased enormously, including that of those logics that have been developed originally in and for philosophy. Epistemic logic is one of these so-called philosophical logics that has been ‘discovered’ by computer scientists and AI researchers. Particularly, the relevance of epistemic logic has been realised by researchers interested in the formal description of knowledge of agents in distributed and intelligent systems in order to specify or verify protocols, and represent knowledge and formalise reasoning methods, respectively.

Knowledge and belief play an important role in everyday life. In fact, most of what we do has to do with the things we know or believe. Likewise, it is not so strange that when we have to specify the behaviour of artificial agents in order to program or implement them in some particular way, it is thought to be important to be interested in the ‘knowledge’ and ‘belief’ of such an agent. In many areas of computer science and artificial intelligence one is concerned with the description or representation of knowledge of users or even the systems themselves. For example, in database theory one tries to model knowledge about parts of reality in certain formal ways to render it implementable and accessible to users. In AI one tries to design knowledge-based decision-support systems that are intended to assist professional users in some specialists field when making decisions by providing pieces of knowledge and preferably some deductions from the input data by means of some inference mechanism. The representation and manipulation of knowledge of some sort is ubiquitous in the information sciences.

This book is not about knowledge representation in general, but rather concentrates on the logic of knowledge and belief. What (logical) properties do knowledge and belief have? What is the difference between knowledge and belief? We do not intend to answer these questions in a deep philosophical discussion of these notions.

THE SYNTAX OF LINEAR LOGIC

The connectives of linear logic

Linear logic is not an alternative logic ; it should rather be seen as an extension of usual logic. Since there is no hope to modify the extant classical or intuitionistic connectives, linear logic introduces new connectives.

Exponentials : actions vs situations

Classical and intuitionistic logics deal with stable truths:

if A and A ⇒ B, then B, but A still holds.

This is perfect in mathematics, but wrong in real life, since real implication is causal. A causal implication cannot be iterated since the conditions are modified after its use ; this process of modification of the premises (conditions) is known in physics as reaction. For instance, if A is to spend $1 on a pack of cigarettes and B is to get them, you lose $1 in this process, and you cannot do it a second time. The reaction here was that $1 went out of your pocket. The first objection to that view is that there are in mathematics, in real life, cases where reaction does not exist or can be neglected : think of a lemma which is forever true, or of a Mr. Soros, who has almost an infinite amount of dollars. Such cases are situations in the sense of stable truths. Our logical refinements should not prevent us to cope with situations, and there will be a specific kind of connectives (exponentials, “!” and “?”) which shall express the iterability of an action, i.e. the absence of any reaction ; typically!A means to spend as many dollars as one needs.

Abstract

The paper studies the properties of the subnets of proof-nets. Very simple proofs are obtained of known results on proof-nets for MLL-, Multiplicative Linear Logic without propositional constants.

Preface

The theory of proof-nets for MLL-, multiplicative linear logic without the propositional constants 1 and ⊥, has been extensively studied since Girard's fundamental paper [5]. The improved presentation of the subject given by Danos and Regnier [3] for propositional MLL- and by Girard [7] for the first-order case has become canonical: the notions are defined of an arbitrary proof-structure and of a ‘contex-forgetting’ map (·)- from sequent derivations to proof-structures which preserves cut-elimination; correctness conditions are given that characterize proof-nets, the proof-structures R such that R = (D)-, for some sequent calculus derivation D. Although Girard's original correctness condition is of an exponential computational complexity over the size of the proof-structure, other correctness conditions are known of quadratic computational complexity.

A further simplification of the canonical theory of proof-nets has been obtained by a more general classification of the subnet of a proof-net. Given a proof-net R and a formula A in R, consider the set of subnets that have A among their conclusions, in particular the largest and the smallest subnet in this set, called the empire and the kingdom of A, respectively. One must give a construction proving that such a set is not empty: in Girard's fundamental paper a construction of the empires is given which is linear in the size of the proof-net.

Introduction

The aim of this paper is to give a purely graph-theoretical definition of noncommutative proof nets, i.e. graphs coming from proofs in MNLL (multiplicative noncommutative linear logic, the (⊗, ℘)-fragment of the one-sided sequent calculus for classical noncommutative linear logic, introduced in [Abr91]). Analogously, one of the aims of [Gir87] was to give a purely graph-theoretical definition of proof nets, i.e. graphs coming from the proofs in MLL (multiplicative linear logic, the (⊗, ℘)-fragment of the one-sided sequent calculus for classical linear logic - better, for classical commutative linear logic). - The relevance of the purely graph-theoretical definition of proof nets for the development of commutative linear logic is well-know; thus we hope the results of this paper will be useful for a similar development of noncommutative linear logic.

The language for MNLL is an extension of the language for MLL, obtained simply adding, as atomic formulas, propositional letters with an arbitrary finite number of negations written after the propositional letter (linear post-negation) or before the propositional letter (linear retronegation). Every formula A of MNLL may be translated into a formula Tv(A) of MLL (simply by replacing each propositional letter with an even number of negations by the propositional letter without negations, and each propositional letter with an odd number of negations by the propositional letter with only one negation after the propositional letter).

Abstract

The syntactic calculus, a fragment of noncommutative linear logic, was introduced in 1958 because of its hoped for linguistic application. Working with a Gentzen style presentation, one was led to the problem of finding all derivations f : A1 … An → B in the free syntactic calculus generated by a context free grammar g (with arrows reversed) and to the problem of determining all equations f = g between two such derivations. The first problem was solved by showing that f is equal to a derivation in normal form, whose construction involves no identity arrows and no cuts (except those in g) and the second problem is solved by reducing both f and g to normal form.

The original motivation for the syntactic calculus came from multilinear algebra and a categorical semantics was given by the calculus of bimodules. Bimodules RFS may be viewed as additive functors R → Mod S, where R and S are rings (of several objects). It is now clear that Lawvere's generalized bimodules will also provide a semantics for what may be called labeled bilinear logic.

Introduction.

I was asked to talk about one precursor of linear logic that I happened to be involved in, even though it anticipated only a small fraction of what goes on in the linear logic enterprise. I would now call this system “bilinear logic”, meaning “non-commutative linear logic” or “logic without Gentzen's three structural rules”.

Abstract

We present stochastic interactive semantics for propositional linear logic without modalities. The framework is based on interactive protocols considered in computational complexity theory, in which a prover with unlimited power interacts with a verifier that can only toss fair coins or perform simple tasks when presented with the given formula or with subsequent messages from the prover. The additive conjunction &, is described as random choice, which reflects the intuitive idea that the verifier can perform only “random spot checks”. This stochastic interactive semantic framework is shown to be sound and complete. Furthermore, the prover's winning strategies are basically proofs of the given formula. In this framework the multiplicative and additive connectives of linear logic are described by means of probabilistic operators, giving a new basis for intuitive reasoning about linear logic and a potential new tool in automated deduction.

Introduction

Linear logic arose from the semantic study of the structure of proofs in intuitionistic logic. Girard presented the coherence space and phase space semantics of linear logic in his original work on linear logic [Gir87]. While these models provide mathematical tools for the study of several aspects of linear logic, they do not oifer a simple intuitive way of reasoning about linear logic. More recently, Blass [Bla92], Abramsky and Jagadeesan [AJ94], Lamarche, and Hyland and Ong have developed semantics of linear logic by means of games and interaction. These new approaches have already proven fruitful in providing an evocative semantic paradigm for linear logic and have found a striking application to programming language theory in the work of Abramsky, Jagadeesan, and Malacaria [AJM93] and in the work of Hyland and Ong [HO93].

Abstract

The problems of inheritance reasoning in taxonomical networks are crucial in object-oriented languages and in artificial intelligence. A taxonomical network is a graph that enables knowledge to be represented. This paper focuses on the means linear logic offers to represent these networks and is a follow-up to the note on exceptions by Girard [Gir92a]. It is first proved that all compatible nodes of a taxonomical network can be deduced in the taxonomical linear theory associated to the network. Moreover, this theory can be integrated in the Unified Logic LU [Gir92b] and so taxonomical and classical reasoning can be combined.

Introduction

The problems of inheritance reasoning in taxonomical networks are crucial in object-oriented languages and in artificial intelligence. A taxonomical network is a graph that enables knowledge to be represented. The nodes represent concepts or properties of a set of individuals whereas the edges represent relations between concepts. The network can be viewed as a hierarchy of concepts according to levels of generality. A more specific concept is said to inherit informations from its subsumers. There are two kinds of edges: default and exception. A default edge between A and B means that A is generally a B or A has generally the property B. An exception edge between A and B means that there is an exception between A and B, namely A is not a B or A has not the property B. Nonmonotonic systems were developed in the last decade in order to attempt to represent defaults and exceptions in a logical way: the set of inferred grounded facts is the set of properties inherited by concepts.