AUTOMATED THEOREM PROVING

23

Oppen [N02] where it is . shown how to combine decision pro-

cedures for satisfiability applied to quantifier-free theories. Shos-

tak has recently presented an interesting alternate method for

combining decision procedures [Sh3]. Just recently, a very

interesting decision procedure over

a

subset of elementary (plane)

geometry has become known to the ATP community, although

discovered by Wen-Tsiin Wu in 1978, in China (see [Wul]). "The clev-

erness and novelty of the procedure within a field so well studied

for so long illustrates how much we have yet to learn about deci-

sion procedures and the analytical approach to theorem proving

in general..

We have deferred technical discussions of the human simula-

tion approach represented by Bledsoe, Nevins and others. We have

done so because the presentation is relatively lengthy and would

disrupt our historical overview. However, because the human

simulation approach is structurally complex even at. the top (over-

view) level, and also a less familiar architecture to mathematicians

than those systems following the logic approach, we do summarize

some of the components and devices used in human-oriented

theorem provers. To do so we adapt an overview list from Bledsoe

[Bll], which we recommend for a more in-depth survey of human-

oriented systems (actually non-resolution systems in general).

Some of the components are used in provers of the logic approach

as well, as will be noted by the reader.

Concepts important to human-oriented theorem proving sys-

tems:

Knowledge base-- a data base (library) of facts, stored by con-

text to the degree possible. This often means storing by object

named rather than property named.

Rewrite rules -- often obtained from an equation by choosing a

direction and then regarding the statement as a replacement rule,