Unit Refutations and Horn Sets

ABSTRACT

The key concepts for this automated theorem-proving paper are those of Horn set and strictly-unit refutation. A Horn set is a set of clauses such that none of its members contains more than one positive literal. A strictly-unit refutation is a proof by contradiction in which no step is justified by applying a rule of inference to a set of clauses all of which contain more than one literal. Horn sets occur in many fields of mathematics such as the theory of groups, rings, Moufang loops, and Henkin models. The usual translation into first-order predicate calculus of the axioms of these and many other fields yields a set of Horn clauses. The striking feature of the Horn property for finite sets of clauses is that its presence or absence can be determined by inspection. Thus, the determination of the applicability of the theorems and procedures of this paper is immediate. In Theorem 1 it is proved that, if S is an unsatisfiable Horn set, there exists a strictly-unit refutation of S employing binary resolution alone, thus eliminating the need for factoring; moreover, one of the immediate ancestors of each step of the refutation is in fact a positive unit clause. A theorem similar to Theorem 1 for paramodulation-based inference systems is proven in Theorem 3 but with the inclusion of factoring as an inference rule. In Section 3 two reduction procedures are discussed. For the first, Chang's splitting, a rule is provided to guide both the choice of clauses and the way in which to split. The second reduction procedure enables one to refute a Horn set by refuting but one of a corresponding family of simpler subproblems.

REFERENCES

• 1: ALLEN, J., AND LUCKHAM, D. An interactive theorem-proving program. In Machine Intelligence, Vol. 5, B. Meltzer and D. Michie, Eds., American Elsevier, New York, 1970, pp. 321-336.
• 2: C. L. Chang, The Unit Proof and the Input Proof in Theorem Proving, Journal of the ACM (JACM), v.17 n.4, p.698-707, Oct. 1970 [doi>10.1145/321607.321618]
• 3: CHANG, C.L. Theorem proving with variable-constrained resolution. Inform. Sci. 4 (1972). 217-231.
• 4: CHANG, C.L. The decomposition principle for theorem proving systems. Proc. Tenth Annual Allerton Conference on Circuit and System Theory, U. of Illinois, Oct. 1972, pp. 20-28.
• 5: C. L. Chang , J. R. Slagle, Completeness of Linear Refutation for Theories with Equality, Journal of the ACM (JACM), v.18 n.1, p.126-136, Jan. 1971 [doi>10.1145/321623.321636]
• 6: HER~S, H. Enumerability, Decidability, Countability. Springer-Verlag, New York, 1965.
• 7: HORN, A. On sentences which are true of direct unions of algebras. J. Symbolic Logic 16 (1951), 14-21.
• 8: KUEHNER, D. Some special purpose resolution systems. In Machine Intelligence, Vol. 7, B. Meltzer and D. Michie, Eds., American Elsevier, New York, 1972, pp. 117-128.
• 9: LUCKHAM, D. Refinement theorems in resolution theory. Proc. IRIA Symposium on Automatic Demonstration, Springer-Verlag, New York, 1970, pp. 163-190.
• 10: MELTZER, B. Theorem proving for computers: Some results on resolution and renaming. Computer J. 8 (1966), 341-343.
• 11: REYNOLDS, J.C. Transformational systems and the algebraic structure of atomic formulas. In Machine Intelligence, Vol. 5, B. Meltzer and D. Michie, Eds., American Elsevier, New York, 1970, pp. 135-152.
• 12: ROBINSON, G., AND WOS, L. Paramodulation in first-order theories with equality. In Machine Intelligence, Vol, 4, B. Meltzer and D. Michie, Eds., American Elsevier, New York, 1969, pp. 135-150.
• 13: ROBINSON, J. A. Automatic deduction with hyper-resolution. Internat. J. Computer Math. 1 (1965), 227-234.
• 14: SLAGLE, J.R. Heuristic search programs. In Theoretical Approaches ~o Non-Numerical Problem Solving, R. B. Banerji and M. D. Mesarovic, Eds., Springer-Verlag, New York, 1970, pp. 246-273.
• 15: SLAGLE, J. R., AND KONIVER, D. Finding resolution proofs using duplicate goals in AND/OR trees. Inform. Sci. $ (1971), 313-342.
• 16: WoN, L., CARSON, D. F., AND ROBINSON, G.A. The unit preference strategy in theorem proving. Proc. AFIPS 1964 FJCC, ~ol. 26, Pt. 1, Spartan Books, New York, pp. 615-621.
• 17: 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]
• 18: WoN, L., AND ROBINSON, G. Paramodulation and set of support. Proc. IRIA Symposium on Automatic Demonstration, Springer-Verlag, New York, 1968, pp. 276-310.

INDEX TERMS

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

Additional Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Logic and constraint programming

General Terms:
Theory, Verification