We combine state-of-the-art techniques from computational linguistics and theorem proving to build an engine for playing text adventures, computer games with which the player interacts purely through natural language. The system employs a parser for dependency grammar and a generation system based on TAG, and has a component for resolving referring expressions. Most of these modules make heavy use of inferences offered by a modern theorem prover for description logic. Our game engine solves some problems inherent in classical text adventures, and is an interesting test case for the interaction between natural language processing and inference.