Journal of the ACM Bibliography

Selected papers that cite this one

• Leo Bachmair and Harald Ganzinger. Rewrite-based equational theorem proving with selection and simplification. Journal of Logic and Computation, 4(3):217-247, June 1994.

• Leo Bachmair, Harald Ganzinger, Christopher Lynch, and Wayne Snyder. Basic paramodulation. Information and Computation, 121(2):172-192, September 1995.

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

• Christopher Lynch. Local simplification. Information and Computation, 142(1):102-126, 10 April 1998.

• J. R. Quinlan and E. B. Hunt. A formal deductive problem-solving system. Journal of the ACM, 15(4):625-646, October 1968.

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

• Tie-Cheng Wang. Z-module reasoning: An equality-oriented proving method with built-in ring axioms. Journal of the ACM, 40(3):558-606, July 1993.

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.

Shortcuts: