is possible due to the inductive nature of many data structures,
such as lists, used by programs. The program is capable of deter-
mining the variable of induction and also the induction predicate
in many simple cases. A fairly sophisticated set of heuristics is
used to guide the above tasks, particularly for the selection of an
induction predicate. Besides its automatic mode, the prover can
be used as a sophisticated proof checker (within its stylized
domain) by supplying it with conjectures during a proof session. A
conjecture is tackled and,
proved, added to the prover's library
of proven results. Any result in the library may be used, generally
as a rewrite rule. Through these conjectures and. user-supplied
recursivelY:·defined functions which can help the prover find the
right induction setting (with all such supplied functions checked
by the prover for existence and uniqueness), quite deep theorems
can be formally verified. Although Boyer and Moore and some oth-
ers tend to think of their system as human-oriented, because of
the heuristics used and the strong human interaction possible, we
place the prover between the two approaches because the system
also has a very dominant, carefully designed, logic with mostly
syntactic heuristic rules, created directly to aid performance, not
because humans use the principle.
In 1975-76 a flurry of interest occurred in proof procedures in
the resolution flavor that utilized a graph representation, with
literals or (conjunctive normal form) clauses as vertices and possi-
ble complementary literals (under substitution) connected by
edges. (See Kowalski [Ko2], Sickel [Sil], Shostak [Shl] and
Andrews [Anl].) Actually, the first explicit graph proof procedure
in the resolution flavor was the "resolution graph" in 1970 (see
[YRl]) and related ideas appeared earlier in Davis [Dal], Loveland
(Lol] and Prawitz [Pr2]. But the connection graph concept (to
adopt Kowalski's term for the class of related procedures)
Previous Page Next Page