88
D.W. LOVELAND
[LSl] Livesey, M. and J. Siekmann. Unification of A+C-terms
(bags) and A+C+I-terms (sets). Universitiit Karlsruhe
Interner Bericht Nr. 5/76, Karlsruhe, 1976.
[LS2] Loveland, D.W. and M.E. Stickel. A hole in goal trees: Some
guidance from resolution theory. Proc. Third intern. Joint
ConJ. on Artif. lntell., Stanford, 1973, 153-161. Also in IEEE
Jrans. on Computers C-25, 1976, 335-341.
[Lu1] Luckham, D. Refinement theorems in resolution theory.
Symp. on Automatic Demonstration, Lecture Notes in Math.
125, Springer-Verlag, Berlin, 1970, 163-190.
[Mal] Maslov, S. Ju. An inverse method of establishing deducibility
in classical predicate calculus. Dokl. Akad. Nauk. SSR, 1964,
17-20.
[Ma2] Maslov, S. Ju. Proof-search strategies for methods of the
resolution type. Mach. /ntett. 6 (Meltzer and Michie, Eds:),
American Elsevier, New York, 1971, 77-90.
[Mel] McCarthy, J. Computer programs for checking mathemati-
cal proofs. Proc. Amer. Math. Soc. Recursive .Pu.nction Thy.,
New York, 1961,219-227.
[MCl] Miller, D.A., E.L. Cohen and P.B. Andrews. A look at TPS.
Proc. Si:J:th Conf. on Auto. Deduction (Loveland, Ed.), Lecture
Notes in Comp. Sci. 138, Springer-Verlag, Berlin, June 1982,
50-69.
[MF1] Martin, W.A. and R.J. Fateman. The MACSYMA system.
Second Symp. on Symbolic Manipulation (Petrick, Ed.), Los
Angeles, 1971, 59-75.
[Mol] Moses, J. Algebraic simplification, a guide for the perplexed.
Second Symp. on Symbolic Manipulation (Petrick, Ed.), Los
Angeles, 1971, 282-304.
[Mul] Munyer, J.C. Analogy as a heuristic for mechanical
theorem-proving. Collected Abstracts of the ·Workshop on
Auto. Deduction, MIT, Aug. 1977.
[Mu2] Musser, D.R. On proving inductive properties of abstract
data types. Proc. Seventh ACM Symp. on Prine.· of Progr.
lAng., 1980. ·
Previous Page Next Page