Attachment

 

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.

1. 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.

2. 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.
3. For Lemmings the most important expressions to evaluate will involve the scene as an argument.
4. 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.
5. 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.