AUTOMATED THEOREM PROVING 31

knowledge-based expert systems and other AI tasks. It is the pro-

totype language for the fifth generation computer systems being

undertaken by the Japanese. One

c~n

regard Prolog crudely as an

input resolution theorem prover with a few added control and con-

venience mechanisms. One may view Prolog programming as writ-

ing axioms about (or specifications for) the task to be performed

and then giving the system a statement (goal) which the system

must show follows from the axiom set. Traversing the correct

proof (when found) forces the correct variable instantiations and

side effects that solve the task. Readers intrigued by this should

read Kowalski [Ko3]. It should be noted that some of the ideas

used in logic programming go back to the_ idea of answer-

extraction and related ideas of Green and Raphael ([GRl],[Grl]).·

This last quarter century has seen automated theorem proving ·

grow from infancy to an adolescence, where its concepts have

aided AI and where a few open problems in discrete mathematics

'

have been proven. The next twenty-five years may well see open

problems of major import proved where one of the coauthors of

the work is a computer program.

Bibliography

[Acl] Ackerman, W. Solvable Cases of the Decision .Problem.

North-Holland, Amsterdam, 1954.

[An1] Andrews, P. Refutations by matings. IEEE 1r.ans. on Com-

puters, C-25, 1976, 801-807.

[An2] Andrews, P. Theorem proving by general matings.

Jau.r .

.Assoc. for Comput. Mach., 1981, 193-214.