System Overview

This section explains the languages we use to
represent the content of a puzzle. Computing
the representations from a text is a complex process
with several stages, as shown in Figure 2.
Most of the stages are independent of the puzzles
domain. Section 3 reviews the main challenges
in this process, and later sections outline
the various processing stages. More details of
some of these stages can be found at (Stanford
NLP Group, 2004).
First-Order Logic (FOL)
An obvious way of solving logic puzzles is to
use off-the-shelf FOL reasoners, such as theorem
provers and model builders. Although most
GRE logic puzzles can also be cast as constraintsatisfaction
problems (CSPs), FOL representations
are more general and more broadly applicable
to other domains, and they are closer
to the natural language semantics. GRE logic
puzzles have finite small domains, so it is practicable
to use FOL reasoners.
The ultimate representation of the content of
a puzzle is therefore written in FOL. For example,
the representation for the first part of
constraint (4) in Figure 1 is: 8x.room(x) !
9y.sculpture(y)^exhibit(y, x). (The treatment
of the modal ‘must’ is explained in §9.2).
Semantic Logic (SL)
Representing the meaning of natural language
texts in FOL is not straightforward because
human languages employ events, plural entities,
modal operations, and complex numeric
expressions. We therefore use an intermediate
representation, written in Semantic Logic
(SL), which is intended to be a general-purpose
semantic representation language. SL extends
FOL with event and group variables, the modal
operators ¤ (necessarily) and § (possibly), and
Generalized Quantifiers (Barwise and Cooper,

1981) Q(type, var, restrictor, body), where type
can be 8, 9, at-least(n), etc. To continue the example,
the intermediate representation for the
constraint is:
¤Q(8, x1, room(x1),Q(¸1, x2, sculpture(x2),
9e.exhibit(e) ^ subj(e, x2) ^ in(e, x1)))
Non-determinism
Although logic puzzles are carefully designed
to reduce ambiguities to ensure that there
is exactly one correct answer per question,
there are still many ambiguities in the analysis,
such as multiple possibilities for syntactic
structures, pronominal reference, and quantifier
scope. Each module ranks possible output representations;
in the event that a later stage reveals
an earlier choice to be wrong (it may be
inconsistent with the rest of the puzzle, or lead
to a non-unique correct answer to a question),
the system backtracks and chooses the next-best
output representation for the earlier stage.