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.