[FOM] Smullyan' workings review

[John McCarthy]

My student Robert Filman formalized one of Smullyan's fairy chess
problems (What piece fell off a5?).  Filman pushed the solutions
through Richard Weyhrauch's interactive theorem prover FOL.  However,
FOL allowed, and Filman used, Lisp progams attached, in Weyhrauch's
sense, to function and predicate symbols.  This allowed these
functions to be evaluated by the computer when supplied with constant
arguments.  For example, that that the black king is in check in the
given position is directly observable rather than having to be deduced 
from axioms giving the positions of the pieces.

Filman's solution of Smullyan's puzzle, used a feature of Weyhrauch's
FOL that corresponds to the way humans solve such puzzles - combining
logical reasoning with direct observation.  In this case, it was
direct observation of a partial (without specifying the occupant of
a5) chess position.  Filman's "chess eye" did not allow more than what
the human chess eye does.  Thus it doesn't do look-ahead.

Even with attachment, Filman's project was barely feasible.
Attachment and quite a bit more are required to make interactive
problem solving convenient.  Neither Filman nor I could specify the
"quite a bit more".