A Linear Format for Resolution With Merging and a New Technique for Establishing Completeness

ABSTRACT

A new technique is given for establishing the completeness of resolution-based deductive systems for first-order logic (with or without equality) and several new completeness results are proved using this technique. The technique leads to very simple and clear completeness proofs and can be used to establish the completeness of most resolution-based deductive systems reported in the literature. The main new result obtained by means of this technique is that a linear format for resolution with merging and set of support and with several further restrictions is a complete deductive system for the first-order predicate calculus.

REFERENCES

• 1: ANDERSON, R. Completeness results for E-resolution. Proc. AFIPS 1970 Spring Joint Comput. Conf., Vo}. 36, pp. 653-656 (AFIPS Press, Montvale, N. J.).
• 2: Peter B. Andrews, Resolution With Merging, Journal of the ACM (JACM), v.15 n.3, p.367-381, July 1968 [doi>10.1145/321466.321469]
• 3: LOVELAND, D.W. A linear format for resolution (submitted for publication).
• 4: LUCKHAM, D. Refinement theorems in resolution theory. A. I. Memo 81, Stanford Artif. Intel. Proj., Stanford, Calif., March 24, 1969; presented at IRIA Symp. on Automatic Deduction, Versailles, France, Dec. 16--21, 1968.
• 5: MORRIS, J. B. E-resolution: Extension of resolution to include the equality relation. Proc. Int. Joint Conf. on Artificial Intelligence, Washington, D. C., May 7-9, 1969 (D. E. Walker and L. M. Norton, Eds.), pp. 287-294 (Mitre Corp., Bedford, Mass., 1969).
• 6: RAPHAEL, BERTRAM. Some results about proof by resolution. SIGART Newsletter, No. 14 (Feb. 1969), 22-25.
• 7: ROBINSON, G. A., AND Wos, L. Paramodulation and theorem-proving in first-order theories with equality. In Machine Intelligence, Vol. IV, Meltzer, B., and Michie, D. (Eds.), American Elsevier, New York, 1969, pp. 135-150.
• 8: -- AND --. Completeness of paramodulation. Ass. for Symbolic Logic, Spring 1968 meeting (abstract in J. Symbolic Logic 34 (1969), 159-160).
• 9: J. A. Robinson, A Machine-Oriented Logic Based on the Resolution Principle, Journal of the ACM (JACM), v.12 n.1, p.23-41, Jan. 1965 [doi>10.1145/321250.321253]
• 10: --. A review of automatic theorem proving. Proc. Symposia in Appl. Math. (1966), Vol. 19 (Schwartz, J. T., Ed.), American Mathematical Society, Providence, R. I., 1967, pp. 1-19.
• 11: --. Automatic deduction with hyper-resolution. Int. J. Computer Math. 1 (1965)~ 227- 234.
• 12: Lawrence Wos , George A. Robinson , Daniel F. Carson, Efficiency and Completeness of the Set of Support Strategy in Theorem Proving, Journal of the ACM (JACM), v.12 n.4, p.536-541, Oct. 1965 [doi>10.1145/321296.321302]

INDEX TERMS

Primary Classification:
  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE

Additional Classification:
  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
      F.1.3 Complexity Measures and Classes
          Subjects: Reducibility and completeness

General Terms:
Theory, Verification