Journal of the ACM Bibliography
S.
Fleisig, D.
Loveland, A. K. Smiley
III, and D. L.
Yarmush. An implementation of the model elimination proof procedure.
Journal of the ACM, 21(1):124-139, January 1974.
[BibTeX entry]
Additional Key Words and Phrases:
automatic theorem-proving, model elimination, resolution
Selected references
- Joyce Friedman. A
semi-decision procedure for the functional calculus. Journal
of the ACM, 10(1):1-24, January 1963.
- Donald W. Loveland. Mechanical theorem-proving by
model elimination. Journal of the ACM, 15(2):236-251,
April 1968.
- D. W. Loveland. A
simplified format for the model elimination theorem-proving
procedure. Journal of the ACM, 16(3):349-363, July
1969.
- D. W. Loveland. A
unifying view of some linear Herbrand procedures. Journal of
the ACM, 19(2):366-384, April 1972.
- J. A. Robinson. A
machine-oriented logic based on the resolution principle.
Journal of the ACM, 12(1):23-41, January 1965.
- 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: