This chapter introduces DRT and prepares the way for our computational work. We define DRS languages, discuss accessibility and the standard DRS construction algorithm, give a direct semantics for DRS languages, and show how to translate DRSs into first-order logic. We then implement a simple model checker, and implement the translation into first-order logic.