Journal of the ACM Bibliography

Selected papers that cite this one

• Robert Anderson and W. W. Bledsoe. A linear format for resolution with merging and a new technique for establishing completeness. Journal of the ACM, 17(3):525-534, July 1970.

• Peter B. Andrews. A correction concerning resolution. Journal of the ACM, 15(4):720, October 1968.

• Peter B. Andrews. Resolution with merging. Journal of the ACM, 15(3):367-381, July 1968.

• C. L. Chang. The unit proof and the input proof in theorem proving. Journal of the ACM, 17(4):698-707, October 1970.

• John K. Dixon. Z-resolution: Theorem-proving with compiled axioms. Journal of the ACM, 20(1):127-147, January 1973.

• 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.

• L. Henschen and L. Wos. Unit refutations and Horn sets. Journal of the ACM, 21(4):590-605, October 1974.

• Jieh Hsiang and Michaël Rusinowitch. Proving refutational completeness of theorem-proving strategies: The transfinite semantic tree method. Journal of the ACM, 38(3):559-587, July 1991.

• Richard B. Kieburtz and David Luckham. Compatibility and complexity of refinements of the resolution principle. SIAM Journal on Computing, 1(4):313-332, December 1972.

• Donald W. Loveland. Mechanical theorem-proving by model elimination. Journal of the ACM, 15(2):236-251, April 1968.

• D. Michie and E. E. Sibert. Some binary derivation systems. Journal of the ACM, 21(2):175-190, April 1974.

• Arthur J. Nevins. A human oriented logic for automatic theorem-proving. Journal of the ACM, 21(4):606-621, October 1974.

• Ross A. Overbeek. A new class of automated theorem-proving algorithms. Journal of the ACM, 21(2):191-200, April 1974.

• Raymond Reiter. Two results on ordering for resolution with merging and linear format. Journal of the ACM, 18(4):630-646, October 1971.

• James R. Slagle. Automated theorem-proving for theories with simplifiers, commutativity, and associativity. Journal of the ACM, 21(4):622-642, October 1974.

• James R. Slagle. Interpolation theorems for resolution in lower predicate calculus. Journal of the ACM, 17(3):535-542, July 1970.

• James R. Slagle. Automatic theorem proving with built-in theories including equality, partial ordering, and sets. Journal of the ACM, 19(1):120-135, January 1972.

• James R. Slagle. Automatic theorem proving with renamable and semantic resolution. Journal of the ACM, 14(4):687-697, October 1967.

• James R. Slagle. An approach for finding C-linear complete inference systems. Journal of the ACM, 19(3):496-516, July 1972.

• 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.

Selected references

• J. A. Robinson. A machine-oriented logic based on the resolution principle. Journal of the ACM, 12(1):23-41, January 1965.

Shortcuts: