Journal of the ACM Bibliography
James R. Slagle. An approach for
finding C-linear complete inference systems. Journal of
the ACM, 19(3):496-516, July 1972.
[BibTeX entry]
Additional Key Words and Phrases:
theorem-proving, completeness theorems, inference systems, linear
deduction, linear refutation, inference rules, resolution principle,
paramodulation, transitivity axiom, set membership axiom, artificial
intelligence, deduction, refutation, mathematical logic, predicate
calculus
Selected papers that cite this one
Selected references
- 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.
- C. L. Chang and J. R. Slagle. Completeness of linear refutation
for theories with equality. Journal of the ACM,
18(1):126-136, January 1971.
- 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. 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: