In this paper we discuss inference in computational semantics. In particular, we argue that state-of-the-art methods in first-order theorem proving and model generation are of direct relevance to inference for natural language processing. This claim is based on our experience of implementing van der Sandt’s approach to presupposition, and much of the paper discusses this application. Incidentally, the reader can experiment with this implementation over the internet: most of what is discussed below is available as part of Johan Bos’s DORIS system (Discourse Oriented Representation and Inference System1).