Journal of the ACM Bibliography

Additional Key Words and Phrases: theorem proving, built-in theories, theories with equality, partial ordering, set theory, resolution principle, paramodulation, refutation completeness, inference rules, artificial intelligence, deduction, mathematical logic

Selected papers that cite this one

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

• 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

• Martin Davis and Hilary Putnam. A computing procedure for quantification theory. Journal of the ACM, 7(3):201-215, July 1960.

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

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

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