Journal of the ACM Bibliography
John
K. Dixon. Z-resolution: Theorem-proving with compiled axioms.
Journal of the ACM, 20(1):127-147, January 1973.
[BibTeX entry]
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
Selected references
- 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.
Shortcuts: