18
D.W. LOVELAND
system but by our understanding of the term we leave. the system
firmly entrenched in the logic camp. This is not to say that
domain-dependent information cannot influence search control.
There is a weighting system that assigns values to terms, following
user-proscribed rules, which is apparently very successful. How-
ever, the rules are purely syntax directed, although not limited to
weights on nonlogical symbols. AURA now is viewed by its origina-
tors as a useful research tool for solving open problems subject to
precise axiomatic formulations. (See Wos
et al.
[WW3].)
We should mention at this point an effort to make a flexible
theorem prover available "to the people". More correctly, the pur-
pose is to provide a structured set of tools, called LMA (for Logic
Machine Architecture), that does include a default prover, named
ITP, for those wishing to experiment with their own variation of
theorem prover, not necessarily resolution based. ITP has the full
capability of AURA. Lusk, McCune and Overbeek are designing the
package in PASCAL for portability (see Lusk
et al.
[LMl]).
A very interesting effort that differs considerably from the
resolution based prover of Wos
et al.
and the strong human-
oriented prover of Bledsoe is the Computational Logic Theorem
Prover (see (BMl], [BM2], [BM3]). This effort by R. Boyer and J.
Moore, begun about 1972, focuses on inductive domains. The
prover uses the language of quantifier-free first order logic with
equality and features a general induction principle among the
inference rules with the other inference rules, primarily rewrite
rules. The latter are constantly undergoing change; for example,
a proven equality can be converted to a rewrite rule for later use
at the user's option. Besides working within traditional mathemat-
ics, primarily number theory using recursive arithmetic, they have
proved properties of programs and algorithms, so-called "proofs of
correctness", of particular interest within computer science. This
Previous Page Next Page