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 sentence. - 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 this.

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