there were other approaches to· ATP, definitely more human-
oriented. One already referenced was the Semi Automated
Mathematics (SAM)
1963 to 1967. Although
much of this work did not get recorded in the scientific literature
(however, see [GOl]) there was developed a succession of systems
designed to interact with the mathematician. The systems had
good interfacing to the human user, with good expressive·power in
its input/output language. The notation adopted was a many
sorted c.J-order logic with equality. "-notation was .employed. The
SAM I system was primarily a proof checker, but the theorem prov-
ing power continued to increase through SAM V, which had sub-
stantial automatic capability. SAM's lemma mentioned earlier was
proved on SAM V. Also, a matching procedure for c.J-order logic was
studied by Gould in a 1966 Ph.D. thesis. Interaction was aided by a
natural deduction format that used subordinate proofs in the
sense of Fitch 1952 [Fil].
One bastion of dedication to the human oriented approach to
theorem proving was (is) MIT. One project out of the MIT environ-
ment in the mid-sixties was ADEPT, the Ph.D. thesis of L.M. Norton
[Nol]. ADEPT was a heuristic theorem prover for group theory.
Many heuristics were used, including a simple model to prune sub-
set relations; the heuristics were deemed powerful enough that no
backtracking was permitted. The limit of its capability was
~ group
The fascination with resolution as the basis of theorem proving
systems was overwhelming in the latter part of the 1960's. Not
only did the theorem proving community adopt the principle but
artificial intelligence researchers looked upon resolution as the
key to their needs regarding reasoning systems. Question-
answering (see Green and Raphael [GRl]) and robotics (see Fikes
and Nilsson [FNl]) were two areas where resolution theorem
Previous Page Next Page