AUTOMATED THEOREM PROVING
39
[MWl] Manna, Z. and R. Waldinger.· A deductive approach to pro-
gram synthesis. ACM Prans. on Progr. Lang., 1980, 90-121.
[Nal] Naur, P. Proof of algorithms by general snapshots. BIT,
·.·.~
1966.
[Nel] Nevins, A.J. A human oriented logic for automatic theorem
proving. Jour. Assoc. for Comput. Mach., 1974, 606-621.
[Ne2] Nevins, A.J. Plane geometry theorem proving using forward
chaining. Artif.lntelL., 1975, 1-23.
[Ne3] Nevins, A.J. A relaxation approach to splitting in an
automatic theorem prover. Artif. /n.telL., 1975, 25-39.
[No1] Norton, L.M. ADEPT - a heuristic program for proving
theorems of group theory. Ph.D. Thesis, MIT, 1966. Also as
JIITProject MAC Report MAC-TR-33, 1966 ..
[NOl] Nelson, G. and D. Oppen. Fast decision procedures based on
congruence closure. Jour. Assoc. for Comput. Mach., 1980,
356-364.
[N02] Nelson, G. and D. Oppen. Simplification by cooperating deci-
sion procedures. ACM 1'rans. on Progr. 14ng. ancl Systems,
1979.
[NSl] Newell, A., J.C. Shaw and H.A. Simon. Empirical explorations
of the logic theory machine: a case study in heuristics.
Proc. Western Joint Computer Conf., 1956, 218-239. Also in
Computers and 1hought (Feigenbaum and Feldman, Eds.),
McGraw-Hill, 1963, 134-152.
[Pll] Plaisted, D.A. A simplified problem reduction format. Artif.
/n.teLl., 1982, 227-261.
[Pl2] Plotkin, G.D. Building-in equational theories. Mach. /n.tell. 7
(Meltzer and Michie, Eds.), Halsted Press, New York, 1972,
73-90.
[Pol] Polak, W. Program verification at Stanford: past, present,
future. German Workshop on Arttfi.ciallnteLligence 81 {Siek-
mann, Ed.), Informatik-Fachberichte 47, Springer-Verlag,
Berlin, 1981, 256-276.
Previous Page Next Page