40
D.W. LOVELAND
[Pr1] Prawitz, D. An improved proof procedure. 1heoria., 1960,
102-139.
[Pr2] Prawitz, D. Advances and problems in mechanical proof
procedures. Mach. Jntetl. 4 {Meltzer aiid Michie, Eds.), Edin-
burgh University Press, Edinburgh, 1969, 73-89.
[PS1] Peterson, G.E. and M.E. Stickel. Complete sets of reductions
for some equational theories. Jour. Assoc. Jar Comput.
Mach., 1981, 233-264.
[Rel] Reiter, R. . A semantically guided deductive system for
automatic theorem proving. Proc. 1hird. Intern. Joint ConJ.
Artif. Jntell., 1973, 41-46. Also in IEEE 'I'rans. on Computers,
1976, 328-334.
[Rol] Robinson, J.A. A machine-oriented logic based on the reso-
lution principle. Jour. Assoc. for Comput. Mach., 1965, 23-41.
[Ro2] Robinson, J.A. Automatic deduction with hyper-resolution.
Intern. Jour. of Computer Math., 1965, 227-234.
[Ro3] Roussel, P. Prolog: manuel de
r~ference
et d'utilisation.
Rapport de recherche CNRS, Groupe Intelligence Artiticielle,
Universit~
Aix-Marseille II, 1975.
[RSl] Raulefs, P., J. Siekmann, P. Szabo and E. Unvericht. A short
survey on the state of the art in matching and unification
problems. S/GSAM Bulletin, May 1979, 14-20.
[Sal] Sandford, D.M. Using Sophisticated. Models in Resolution
1heorem Proving. Lecture Notes in Computer Science 90,
Springer-Verlag, Berlin, 1980.
[Shl] Shostak, R.E. Refutation graphs. ArtiJ. lntell., 1976.
[Sh2] Shostak, R.E. A practical decision procedure for arithmetic
with function symbols. Jour. Assoc. Jar Comput. Mach., 1979,
351-360.
[Sh3] Shostak, R.E. Deciding combinations of theories. Proc.
Sizth ConJ. on Auto. Deduction (Loveland, Ed.), Lecture
Notes in Comp. Sci. 138, Springer-Verlag, Berlin, June 1982,
209-223. .
Previous Page Next Page