Next: Programs for Playing Lemmings
Up: Predicting the Future
Previous: Persistent Behaviors
A computer program doing logical inference need not compute 53 + 18 by
deriving 53 + 18 = 71 from the laws of arithmetic. Instead it should
take advantage of the computer and get this result from the computer's
arithmetic. This is accomplished in various interactive theorem provers
by attaching a program, in Lisp for instance, to the function name,
in this case +. The following considerations apply.
- As a proof step, the prover is given an expression to evaluate,
e.g. the command is
The result of the evaluation is a sentence, e.g. 53 + 17 = 71,
which can then be used for further inference like any other logical
- The most straightforward evaluators can only be given ground
expressions to evaluate. Fancier ones can do algebraic and logical
simplification of expressions involving variables. For Lemmings
we contemplate only the ground case.
- For Lemmings the most important expressions to evaluate
will involve the scene as an argument.
- The attachments are done by the builder of the system, and therefore
have the same inferential status as the axioms. In principle, one
might use a program verification system to show that the functions
defined by the program satisfy the axioms involving the function
names. I am not aware that this has ever been done.
- As described in [McCarthy, 1962], attachments can be combined with
reflexion principles to allow the results of decision procedures
to be entered as formulas. I don't think Lemmings will require
Richard Weyhrauch  has the most elaborate system involving
attachment. I don't think Lemmings will require its complexities.
Mon Mar 2 16:21:50 PDT 1998