AUTOMATED THEOREM PROVING
88
[B.M3] Boyer, R.S. and J.S. Moore. A. verification condition genera-
tor for FORTRAN.
1he Correctness Problem. in Computer
Sci-
ence
(Boyer and Moore, Eds.), Academic Press, London,
1981.
[Bol] Boyer, R.S. ·
Loclcing: a. Restrictitm. of Resolution.
Ph.D.
dissertation, Univ. of Texas, Austin, 1971.
[BTl] Bledsoe, W.W. and M. Tyson. The UT interactive theorem
prover. Uni11.
Te:r:as Jla.th Dept.
Jlem.o
ATP-17A,
May 1:978.
[Chl] Chang, C. The unit proof and the input proof in theorem
proving.
Jour. Assoc. for Com.put. Jla.ch.,
1970, 698-?0?.
[CJ1] Carter, W.C., W.H. Joyner, Jr. and D. Brand. Microprogram
verification considered necessary.
AF/PS Conf. .Proc. 47
(Nat. Computer Conf.), 1978, AFIPS Press, Montvale, 657-
664.
[CKl] Colmerauer, A., H. Kanoui, R. Pasero and P. Roussel. Un
Systt!me de communication hormne-machine en francais.
Research Report CRI 72-18, Groupe Intelligence Artificielle,
Universitt! Aix-Marseille II, 1973.
[CLl] Chang, C. and R.C. Lee.
Symbolic
Logic a.nd
Jlech.a.nica.l
7heorem Prooing.
Academic Press, New York, 1973.
[CM1] Clocksin, W.F. and C.S. Mellish.
.Progra.mming in .Prolog.
Springer-Verlag, Berlin, 1981.
[Col] Cook, S. The complexity of theorem-proving procedures.
Proc. 1hird. ACJI Sym.p.
on
1heory of Computing,
Shaker Hts.,
1971, 151-158.
[Dal] Davis, M. Eliminating the irrelevant from mechanical proofs.
Proc. Symp. Applied. Jla.th.,
XV, 1963, 15-30.
[Da2] Davis, M. The prehistory and early history of automated
deduction.
7he
Autom.a.tion of Rea.soni:ng I
{Siekmann and
Wrightson, Eds.), Springer-Verlag, 1983.
(DL1] Davis, M., G. Logemann and D. Loveland. A machine program
for theorem proving.
Comm. Assoc. for Com.put. Jla.ch.,
1962,
394-397.
Previous Page Next Page