AUTOMATED THEOREM PROVING
3'1
[Ko4] Kowalski, R.A. Private communication.
[Ku1] Kuehner, D.G. A note on the relation between resolution
and Maslov's inverse method.
Mach. In.tell. 6
(Meltzer and
Michie, Eds.), American Elsevier, New York. 1971, 73·76.
[KV1] Kowalski, R. and M. Van Emden. The semantics of predicate
logic as programming language.
Jour. Assoc. for Compu.t.
Ma.ch.,
1976, 733-743.
[La1] Lankford, D. This volume.
[LB1] Lankford, D.S. and A.M. Ballantyne. Decision procedures for
simple equational theories with commutative-associative
axioms: Complete sets of commutative-associative reduc-
tions. Univ. of Texas Math Dept. Report ATP-35, Austin,
1977.
[Le1] Lenat, D. AM: Discovery in mathematics.as heuristic search.
Knowledge-Based. Systems in Artiflcia.L In.tellV/ence
(Davis
and Lenat,
Eds~).
McGraw-Hill, 1982, 3-149.
[LM1] Lusk, E.L., W.W. McCune and R.H. Overbeek. Logic machine
architecture: (I) kernel functions (II) inference mechanisms.
Proc. Sizth Conf. on Auto . .Ded.ti.Ction
(Loveland, Ed.), Lecture
Notes in Comp. Sci. 138, Springer-Verlag, Berlin, June 1982,
70-108.
[Lo1] ·Loveland,
D.W~
Mechanical theorem proving by model elimi-
nation.
Jour. Assoc. for Comput . .Mach.,
1968, 236-251.
[Lo2] Loveland, D.W. A simPlified format for the model elimination
procedure.
Jour. Assoc. for Comput. Ma.ch.,
1969, 349-363.
[Lo3] Loveland, D.W. A linear format for resolution. Sym.p.
on
Automatic Demonstration.
Lecture Notes
in
Math. 125,
Springer-Verlag, Berlin, 1970, 147-162.
[Lo4] Loveland, D.W. A unifying view of some linear Herbrand pro-
cedures.
Jour. Assoc. for Comput. Jla.ch.,
1972, 366-384.
[Lo5] Loveland, D.W.
Automated. Theorem Proving: a.
bJgicaJ.
.Ba.sis.
North-Holland, Amsterdam, 1978.
Previous Page Next Page