A calculus for first order Discourse Representation Structures

Abstract

This paper presents a sound and complete proof system for the first order fragment of Discourse Representation Theory. Since the inferences that human language users draw from the verbal input they receive for the most transcend the capacities of such a system, it can be no more than a basis on which more powerful systems, which are capable of producing those inferences, may then be built. Nevertheless, even within the general setting of first order logic the structure of the “formulas” of DRS-languages, i.e. of the Discourse Representation Structures suggest for the components of such a system inference rules that differ somewhat from those usually found in proof systems for the first order predicate calculus and which are, we believe, more in keeping with inference patterns that are actually employed in common sense reasoning.

This is why we have decided to publish the present exercise, in spite of the fact that it is not one for which a great deal of originality could be claimed. In fact, it could be argued that the problem addressed in this paper was solved when Gödel first established the completeness of the system of Principia Mathematica for first order logic. For the DRS-languages we consider here are straightforwardly intertranslatable with standard formulations of the predicate calculus; in fact the translations are so straightforward that any sound and complete proof system for first order logic can be used as a sound and complete proof system for DRSs: simply translate the DRSs into formulas of predicate logic and then proceed as usual. As a matter of fact, this is how one has chosen to proceed in some implementations of DRT, which involve inferencing as well as semantic representation; an example is the Lex system developed jointly by IBM and the University of Tübingen (see in particular (Guenthner et al. 1986)).

In the light of the close and simple connections between DRT and standard predicate logic, publication of what will be presented in this paper can be justified only in terms of the special mash we have tried to achieve between the general form and the particular rules of our proof system on the one hand and on the other the distinctive architecture of DRS-like semantic representation. Some additional justification is necessary, however, as there exist a number of other proof systems for first order DRT, some of which have pursued more or less the same aims that have motivated the system presented here. We are explicitly aware of those developed by (Koons 1988), (Saurer 1990), (Sedogbo and Eytan 1987), (Reinhart 1989), (Gabbay and Reyle 1994); perhaps there are others. (Sedogbo and Eytan 1987) is a tableau system, and (Reinhart 1989) and (Gabbay and Reyle 1994) are resolution based, goal directed. These systems may promise particular advantages when it comes to implementing inference engines operating on DRS-like premises. But they do not aim to conform to certain canons of actual inferencing by human interpreters of natural language; and indeed the proof procedures they propose depart quite drastically from what one could plausibly assume to go in the head of such an interpreter. Only (Koons 1988) and (Saurer 1990) are, like our system, inspired by the methods of natural deduction. But there are some differences in the choice of basic rules. In particular both (Koons 1988) and (Saurer 1990) have among their primitive rules the Rule of Reiteration, which permits the copying of a DRS condition from a DRS to any of its sub-DRSs. In our system this is a derived rule (see Section 4 below).

We will develop our system in several stages. The necessary intuitions and the formal background are provided in Sections 1 and 2. (The formal definitions can be found also in the first two chapters of (Kamp and Reyle 1993). The first system we present is for a sublanguage of the one defined in Section 2, which differs from the full language in that it lacks identity and disjunction. The core of the paper consists of Section 3, where the proof system for this sublanguage is presented, and Section 5, which extends the system for the full language, including disjunctions (Section 5.1) and identity (Section 5.2) and then establishes soundness and completeness for the full system. Section 4 deals with certain derived inference principles.