This was one of the first ever implemented AI programs. It's interesting because it was designed in part by Allen Newell, a leading exponent of the symbol-processing approach to cognitive modelling. His work culminated in 1990 with the publication of a book on unified theories of cognition. The paper cited below is one of the first statements of his views on AI as a theory of cognition. So please read [Elements of a Theory...]. Pay most attention to Newell's views of what such a theory should do (pp 151-153) and of its relation to other schools of psychology (pp 163-166).

How does the program actually work? The important point is that you start with a set of axioms of logic from which a theorem is to be proven. These axioms can be thought of as ``sentences'' describing what you originally know. A theorem is also a sentence, which has to be derived from the axioms.

As well as the axioms, you have a number of *rules of inference*
which convert old sentences into new ones. There is a very close analogy
to a one-person board game. The axioms are the starting positions; rules
of inference are the permitted moves; proving a theorem is equivalent to
asking whether a given state of the board is reachable by a sequence of
legal moves from one of the starting positions.

In principle, one could *exhaustively generate* all possible
sentences from the axioms, stopping when one of them was the same as the
theorem to be proven. This is what the authors refer to as the ``British
Museum algorithm''. Because this algorithm generates all possible
sentences, it's guaranteed to find a sentence that matches the theorem
to be proved, should one exist.

In practice, this is impossible on any present or future computer,
because of the *combinatorial explosion* in the number of possible
moves. So one needs *heuristics*: methods which save time by looking
only at plausible moves. In the jargon of AI, they *prune the search
tree*. However, unless the heuristics are to be as slow as the original
exhaustive computation, they can only make a guess at plausibility,
relying on hopefully informative but sometimes deceptive surface
features. Hence they do not *guarantee* a solution.

Wed Feb 14 23:52:04 GMT 1996