Doing arithmetic without diagrams

摘要

We describe a theorem prover for elementary number theory which proves theorems not by representing them as diagrams as in a semantic net, but rather by representing them in the traditional manner as lists. This theorem prover uses no chaining rules, forward or backward, but instead interaction between equations is based upon the use of many truth-value preserving transformations. These transformations are used in a manner similar to that in which a LISP interpreter executes LISP functions.