The Unit Proof and the Input Proof in Theorem Proving

ABSTRACT

A resolution in which one of the two parent clauses is a unit clause is called a unit resolution, whereas a resolution in which one of the two parent clauses is an original input clause is called an input resolution. A unit (input) proof is a deduction of the empty clause □ such that every resolution in the deduction is a unit (input) resolution. It is proved in the paper that a set S of clauses containing its unit factors has a unit proof if and only if S has an input proof. A LISP program implementing unit resolution is described and results of experiments are given.

REFERENCES

• 1: 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]
• 2: Martin Davis , Hilary Putnam, A Computing Procedure for Quantification Theory, Journal of the ACM (JACM), v.7 n.3, p.201-215, July 1960 [doi>10.1145/321033.321034]
• 3: Char-Tung Lee, A completeness theorem and a computer program for finding theorems derivable from given axioms, 1967
• 4: LOVELAND, D.W. A linear format for resolution. Carnegie-Mellon U., Pittsburgh, Pa., Dec. 1968.
• 5: LUCKHA.M, D. Some tree-paring strategies for theorem-proving. In Machine Intelligence, Vol. 3 (Dale, E., and Michie, D., eds.), Oliver & Boyd, Edinburgh, 1968, pp. 95-112.
• 6: --.. Refinement theorems in resolution theory. A-I Menlo 81, Stanford Artificial Intelligence Project, Stanford U., Stanford, Calif., March 24, 1969.
• 7: MELTZER, B. Theorem proving for computers: Some results on resolution and renaming. Computer J. 8 (1966), 341-343.
• 8: James R. Slagle, Automatic Theorem Proving With Renamable and Semantic Resolution, Journal of the ACM (JACM), v.14 n.4, p.687-697, Oct. 1967 [doi>10.1145/321420.321428]
• 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. Proe. Symp. in Appl. Math, Amer. Math. Soc., Providence, R. I., 1967.
• 11: The generalized resolution principle. In Machine Intelligence, Vol. 3 (Dale, E., and Michie, D., eds.), Oliver & Boyd, Edinburgh, 1968, pp. 77-94.
• 12: J. R. Quinlan , E. B. Hunt, A Formal Deductive Problem-Solving System, Journal of the ACM (JACM), v.15 n.4, p.625-646, Oct. 1968 [doi>10.1145/321479.321487]
• 13: An experience-gathering problem-solving system. Teeh. Rep. 68-1-03, Computer Sci. Group, U. of Washington, Seattle, Wash., May 16, 1968.
• 14: Wos, L., CARSON, D. F., XND ROmNSON, G.A. The unit preference strategy in theorem proving. Proc. AFIPS 1964 Fall Joint Comput. Conf., Vol. 26, Pt. 1, pp. 615-621 (Spartan Books, Washington, D. C.).
• 15: 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]
• 16: Lawrence Wos , George A. Robinson , Daniel F. Carson , Leon Shalla, The Concept of Demodulation in Theorem Proving, Journal of the ACM (JACM), v.14 n.4, p.698-709, Oct. 1967 [doi>10.1145/321420.321429]

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS

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

General Terms:
Experimentation, Measurement, Performance, Theory, Verification