Attempto Controlled English (ACE) - a subset of English that can be
unambiguously translated into first-order logic - is a knowledge
representation language. To support automatic reasoning in ACE we have
developed the Attempto Reasoner (RACE). RACE proves that one ACE text
is the logical consequence of another one, and gives a justification
for the proof in ACE. If there is more than one proof, RACE will find
all of them. Variations of the basic proof procedure permit query
answering and consistency checking. Reasoning in RACE is supported by
auxiliary first-order axioms and by evaluable functions. The current
implementation of RACE is based on the model generator Satchmo. As a
consequence, RACE cannot only be used for theorem proving but also for
model generation.