32

D.W. LOVELAND

[An3] Andrews, P.B. Transforming matings into natural deduction

proofs. Proc. Fifth ConJ. on Auto. Deduction (Bibel and

Kowalski, Eds.), Lecture Notes in Comp. Sci. 87, Springer-

Verlag, Berlin, July .1981, 281-292 .

• _'IZ.

[BBl] Ballantyne, A.M. and W.W. Bledsoe. On generating and using

examples in proof discovery. Mach. /ntell. 10, Ellis Harwood

Ltd., Chichester, 1982, 3-39.

[BEl] Blasius, K., N. Eininger, J. Siekmann, G. Smolka, A. Herold

and C. Walther. The Markgraf Karl refutation procedure

(Fall 1981). Proc. Seventh Intern. Joint Conf. on Artif.

Jn,teLl., Aug. 1981, 511-518.

[BF1] Breben, M., A. Ferro, E.G. Omodeo and J.T. Schwartz. Deci-

sion procedures for elementary sublanguages of set theory

II: Formulas involving restricted quantifiers, together with

ordinal integer, map, and domain notions. Commun. Pu.re

and Appl. Math., 1981, 177-195.

[Bil] Bibel, W. An approach to a systematic theorem proving pro-

cedure in first-order logic. Computing, 1974, 43-55.

[Bi2] Bibel, W. Syntax-directed, semantics-supported program

synthesis. Artif. /nteLL., 1980, 243-262.

[Bi3] Bibel, W. Mating in matrices. German Workshop on Arti,flciaL

Jn,teLLigence 81 (Siekmann, Ed.), Informatik-Fachberichte

47, Springer-Verlag, Berlin.

[Bi4] Bibel, W. Automated 1heorem Proving. Vieweg Verlag,

Braunschweig, 1982.

[Bll] Bledsoe, W.W. Non-resolution theorem proving. Artif. lnteLL.,

1977, 1-35. Also in Readings in Artif. lnteLL. (Webber and

Nilsson, Eds.), Tioga, Palo Alto, 1981, 91-108.

[Bl2] Bledsoe, W.W. Using examples to generate instantiations for

set variables. Proc. Intern. Joint Conf. Artif . ./nteLL., 1983.

[B.M1] Boyer, R.S. and J.S. Moore. Proving theorems about LISP

functions. Jour. Assoc. for Comput. Mach., 1975, 129-144.

[BM2] Boyer, R.S. and J.S. Moore. A Computational Logic.

Academic Press, New York, 1979.