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