How to represent knowledge is one of the key questions in the construction of expert systems. Its solution depends on a number of factors, the most important of which are how knowledge is to be acquired and how it is to be used. Since we are interested in the use of natural language for communication with computers, we require from a formalism suggested for knowledge representation that it be suitable as a target for the systematic translation from natural language expressions. We want to propose a theory, called Discourse Representation Theory (DRT), which was originally developed by Kamp to analyze natural language discourse, as a means to represent knowledge in an expert system. With Discourse Representation Theory it has been possible to solve certain cases of contextual relations which have puzzled linguists and logicians for a long time. In this paper we give a precise definition of DRT and describe the rules used to translate from natural language to Discourse Representation Structures (DRSs), the central notion of the theory. We show how the notation used in DRT relates to standard predicate logic and define its deductive theory. We also outline ways of implementing DRT and the proof procedures we intend to use.