Journal of Logic, Language and Information 5 (3-4):297-348 (1996)
AbstractThis 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 )
Similar books and articles
Resolution Calculus for the First Order Linear Logic.Grigori Mints - 1993 - Journal of Logic, Language and Information 2 (1):59-83.
Undecidability and Intuitionistic Incompleteness.D. C. McCarty - 1996 - Journal of Philosophical Logic 25 (5):559 - 565.
Hans Kamp & Uwe Reyle, From Discourse to Logic: Introduction to Modeltheoretic Semantics of Natural Language, Formal Logic and Discourse Representation Theory. [REVIEW]Varol Akman - 1995 - Computational Linguistics 21 (2):265-268.
What Does Language Tell Us About Consciousness? First-Person Mental Discourse and Higher-Order Thought Theories of Consciousness.Neil Campbell Manson - 2002 - Philosophical Psychology 15 (3):221 – 238.
The Modal Object Calculus and its Interpretation.Edward N. Zalta - 1997 - In M. de Rijke (ed.), Advances in Intensional Logic. Kluwer Academic Publishers. pp. 249--279.
Systems of Illative Combinatory Logic Complete for First-Order Propositional and Predicate Calculus.Henk Barendregt, Martin Bunder & Wil Dekkers - 1993 - Journal of Symbolic Logic 58 (3):769-788.
Added to PP
Historical graph of downloads
Citations of this work
Incremental Dynamics.Jan van Eijck - 2001 - Journal of Logic, Language and Information 10 (3):319-351.
Dynamic Bracketing and Discourse Representation.Albert Visser & Kees Vermeulen - 1996 - Notre Dame Journal of Formal Logic 37 (2):321-365.
Direct Deductive Computation on Discourse Representation Structures.Uwe Reyle & Dov M. Gabbay - 1994 - Linguistics and Philosophy 17 (4):343 - 390.
References found in this work
From Discourse to Logic: Introduction to Modeltheoretic Semantics of Natural Language, Formal Logic and Discourse Representation Theory.Hans Kamp & Uwe Reyle - 1993 - Dordrecht: Kluwer Academic Publishers.
Logic: Techniques of Formal Reasoning.Donald Kalish, Richard Montague & Gary Mar - 1964 - New York, NY, USA: Oxford University Press USA.
A Natural Deduction System for Discourse Representation Theory.Werner Saurer - 1993 - Journal of Philosophical Logic 22 (3):249 - 302.