This paper embeds the core part of Discourse Representation Theory in the classical theory of types plus a few simple axioms that allow the theory to express key facts about variables and assignments on the object level of the logic. It is shown how the embedding can be used to combine core analyses of natural language phenomena in Discourse Representation Theory with analyses that can be obtained in Montague Semantics.

We provide first-order axioms for the theories of finite trees with bounded branching and finite trees with arbitrary (finite) branching. The signature is chosen to express, in a natural way, those properties of trees most relevant to linguistic theories. These axioms provide a foundation for results in linguistics that are based on reasoning formally about such properties. We include some observations on the expressive power of these theories relative to traditional language complexity classes.

From a leading authority in artificial intelligence, this book delivers a synthesis of the major modern techniques and the most current research in natural language processing. The approach is unique in its coverage of semantic interpretation and discourse alongside the foundational material in syntactic processing.

In this paper it is shown how the DRT (Discourse Representation Theory) treatment of temporal anaphora can be formalized within a version of Montague Semantics that is based on classical type logic.