AUTOMATED THEOREM PROVING
11
procedure, links potentially compiementary literals but here one
uses a matrix format. A significant improvement is the freedom
fro1Il.conjunctive normal form. It· is not necessary to use the dis-
tributive law to obtain clauses; rather, one can directly use
expressions such as A " (B v ( C "
D)),
a freedom that can
significantly reduce a type of redundancy within the input expres-
sion (see [An2]). Arcs pass between potentially complementary
literals; these are all identified before "unifying" substitutions are
sought for certain adjacent nodes (the atomic formulas therein,
actually). The order of finding complementary pairs (via unifiers)
and simplifying greatly influence computation time and is subject
to heuristic guidance. Andrews employs syntactic heuristics such
as working with the most constrained path to ·minimize instantia-
tion commitment. A key point of the mating method is the highly
controlled rate of expansion of copies of quantified subformulas.
The existing matrix is thoroughly explored for possible contradic-
tions before an essential expansion is made in the number of
clauses to be explored. Andrews uses the higher order unification
process of Huet [Hul], a nondeterministic algorithm often non-
terminating, which also invites, or forces, heuristics to be incor-
porated in the processing, as Andrews has done.
The mode of operation of TPS is either automatic or interac-
tive, so either the user or the mating process can guide the
development of the natural deduction proof. In automatic mode
TPS has proven Cantor's theorem as well as numerous first-order
theorems.
The difficulty of finding the right substitution instances in
higher order unification, where entire formulas can replace a vari-
able, almost surely means that heuristics based on human .
"insight" (or use of the interactive mode) will play an increasingly
important role in provers such as TPS.
Previous Page Next Page