36
D.W. LOVELAND
[He1] Hewitt, C. Description and theoretical analysis (using sche-
mata) of PLANNER: a language for proving theorems and
manipulating models in a robot. Ph.D. thesis, MIT, 1971.
Also as MIT-AI-lab report AI-TR-258, 1972 .
c:
[Ho1] Hoare, C.A.R.
An
axiomatic basis for computer program-
ming. Com.mun. Assoc. for Com.put. Mach., 1969, 576-580.
[HOl] Huet, G. and D.C. Oppen. Equations and rewrite rules: a sur-
vey . .Fbrm.al Languages - Perspectives and Open Problems.
(Book, Ed.), Academic Press, New York, 1980, 349-405.
[Hut] Huet, G.P. A unification algorithm for typed A-calculus.
'Jheor. Com.p11.t. Science, 1975, 27-57.
[Hu2] Huet, G. Confluence reductions: Abstract properties and
applications to term rewriting systems. Jour. Assoc. for
Comput. Mach., 1980, 797-821.
[JPl] Jensen, D.C. and
T.
Pietrzykowski. Mechanizing -order type
theory through unification.
Therw.
Computer Sci.,
1976,
123-171.
[KB1] Knuth, D.E. and P.B. Bendix. Simple word problems in
universal algebra. Combinatorial Problems
in
Abstract Alge-
bras
(Leech, Ed.), Pergamon, New York, 1970, 283-270.
[Ki1] King, J.C. A program veri/fer. Ph.D. thesis, Carnegie-Mellon
Univ., 1969.
[KK1] Kowalski, R. and D. Kuehner. Linear resolution with selec-
tion function. Artif. /ntell., 1971, 227-260.
[Kl1] Kling, R.E. A paradigm for reasoning by analogy. Artif.
/ntell., 1971, 147-178.
[Ko 1] Kowalski, R.A. Predicate logic as a programming language.
Intern. Aclera.tion
/nfor . .Proc. 74, North-Holland, 1974.
[Ko2] Kowalski, R. A proof procedure based on connection graphs.
Jour. Assoc. Com.p11.t. llach., 1975.
[Ko3] Kowalski, R.A.
l.IJgic
for Problem Solving. North-Holland,
1980.
Previous Page Next Page