Journal of the ACM Bibliography
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.
[BibTeX entry]
Additional Key Words and Phrases:
automatic theorem proving, logic, first-order predicate calculus,
completeness, resolution, ground clause, set of support, merge, linear
format, complete deductive system
Selected papers that cite this one
- W. Bibel and E. Eder. Decomposition of tautologies into
regular formulas and strong completeness of connection-graph
resolution. Journal of the ACM, 44(2):320-344, March
1997.
- 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.
- 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.
- Michael Kifer, Georg Lausen, and James Wu. Logical foundations of
object-oriented and frame-based languages. Journal of the
ACM, 42(4):741-843, July 1995.
- D. W. Loveland. A
unifying view of some linear Herbrand procedures. Journal of
the ACM, 19(2):366-384, April 1972.
- H. J. Ohlbach. Semantics-based
translation methods for modal logics. Journal of Logic and
Computation, 1(5):691-746, October 1990.
- 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. An
approach for finding C-linear complete inference systems.
Journal of the ACM, 19(3):496-516, July 1972.
Selected references
Shortcuts: