This paper describes the design of the Tarski Translator, an English-to-logic and logic-to-English translator developed for Tarski's World, an educational Macintosh game designed by Jon Barwise and John Etchemendy. The translator consists of three parts: a grammar, a chart parser, and a unifier. The parser builds for each analysis of an English input sentence an attribute-value matrix that contains the corresponding logical formula as a submatrix. Formulas of first-order logic are built directly by unification without intermediate higher-order translations and without using rules of logical equivalence. The grammar is a categorial unification grammar in which the only combinatorial operation is function application. It contains novel solutions to a number of problems that arise in the mapping from English to logical formulas. By representing the translations of English phrases as layered structures, the Tarski grammar avoids having multiple representations for phrases that have different translations depending on their syntactic role. The basic unification algorithm is extended to allow list values in order to accommodate sentences with coordinate noun phrases and numerals. A compact and fast C-implementation of the translator has been completed for a future version of Tarski's World.