(Gil]
AUTOMATED THEOREM PROVING
Gilmore, P.C. A program for the production of proofs for
theorems derivable within the ftrst order predicate calcUlus
from axioms. Proc. Intern.. Con/. on ln.for. Processing, Paris:
UNESCO House, 1959.
(Gi2] Gilmore, P.C. A proof method for quantification theory: its
justification and realization. IBM Jour. Resea.rch a.nd
Det~el.,
1960, 28-35.
[Gi3] Gilmore, P.C.
An
examination of the geometry· theorem
machine. ArtiJ.In.teLL., 1970, 171-187.
[GMt] Gerhart, S.L., D.R. Musser, D.H. Thompson, D.A. Baker, R.L.
Bates, R.W. Erickson, R.L. London, D.G. Taylor and D.S. Wile.
An overview of AFFIRM: a specification and verification sys-
tem. Proc. ln.tem.. FRd.era.tion of /nfor. Proc. 80, Australia,
1980, 343-348.
[Go1] Goldfarb, W.D. The undecidability
ot
the second-order
unification problem. 'lheor. Com.pu.ter Science, 1981, 225-
230.
[Go2] Good, D. The proof of a distributed system in GYPSY. Univ.
of Texas, Austin, Inst. for Comp. Sci. Technical Report 30,
1982.
(Go3] Gould, W.E. A matching procedure for (A)-order logic. Air
Force Cambridge Research Laboratories, Report 66-781-4,
1966 .•
[GOl] Guard, J.R., F.C. Oglesby, J.H. Bennett and L.G. Settle. Semi-
automated mathematics. Jour. Assoc. for Com.put. Ma.ch.,
1969, 49-62.
[Grl] Green, C. Theorem-proving by resolution as a basis for
question-answering
systems~
Ma.ch. InteU.
4
(Meltzer and
Michie, Eds.), Edinburgh University Press, Edinburgh, 1969,
183-205.
[GRl] Green, C. and Raphael, B. The use of theorem-proving tech-
niques in question-answering systems. Proc. of the
23rd
Na.tiona.l
Conf. of ACM, Brandon Systems Press, Princeton,
1968, 169-181.
Previous Page Next Page