20
D.W. LOVELAND
prospered particularly well because a tight control on the intro-
duction of new clauses was better appreciated after several years
of attempting to constrain growth via resolution refinements, and
because the associated deletion rules for links and clauses seemed
possibly more effective than previous ideas for restraining redun-
dant computation. A theorem prover being built by Jorg Siekmann
and colleagues at Karlsruhe [BEl] (see later remarks) uses the
Kowalski connection graph procedure as the basis of its syntactic
processor and Wolfgang Bibel has used an alternative form of
these ideas and those of Prawitz [Pr2] in constructing his "sys-
tematic proof procedure". (See [Bil] and [Bi3]; see [Bi4] for
comprehensive treatment of this procedure.) The ideas of Bibel
have found independent and somewhat different realization in the
work of Peter Andrews. The theorem prover of Andrews differs in
an important way from all others we discuss in this paper (except
the SAM project) in that it works ·within higher-order logic. We
consider this theorem prover next.
In the late seventies, the development of TPS, a theorem
prover for type theory, was undertaken by Peter Andrews and col-
leagues [An3], [MCl]. This prover, though firmly in the logic camps
as regards approaches to theorem proving, also shows traits of the
human simulation approach, but to date these traits are weak.
One trait is much attention to a good proof development presenta-
tion to the user. The language of the prover is a type theory
embodying A-abstractions.
As
is essential to the provers of the
logic school, it has a precise formal system-- the language just
mentioned and a formal proof system. However, the .Proof system
is complex, involving a natural deduction style proof format, a
mating procedure used within the search process, and the ability
to move from the mating format to the more decipherable natural
deduction format. The mating procedure, like a connection graph
Previous Page Next Page