Additional Key Words and Phrases: LISP, LISP 1.6, partial evaulation, artificial intelligence, heuristic procedure, compiler, semantic compiler, specialization, resolution, thoerem proving, compiling axioms, predicate calculus
- J. A. Robinson. A machine-oriented logic based on the resolution principle. Journal of the ACM, 12(1):23-41, January 1965.
- James R. Slagle. Automatic theorem proving with renamable and semantic resolution. Journal of the ACM, 14(4):687-697, October 1967.
- Lawrence Wos, George A. Robinson, and Daniel F. Carson. Efficiency and completeness of the set of support strategy in theorem proving. Journal of the ACM, 12(4):536-541, October 1965.
- Lawrence Wos, George A. Robinson, Daniel F. Carson, and Leon Shalla. The concept of demodulation in theorem proving. Journal of the ACM, 14(4):698-709, October 1967.