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.
Previous Page Next Page