[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 .
[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.
Previous Page Next Page