Unit Refutations and Horn Sets
- 1 October 1974
- journal article
- Published by Association for Computing Machinery (ACM) in Journal of the ACM
- Vol. 21 (4), 590-605
- https://doi.org/10.1145/321850.321857
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.Keywords
This publication has 8 references indexed in Scilit:
- Finding resolution proofs and using duplicate goals in and/or treesInformation Sciences, 1971
- Completeness of Linear Refutation for Theories with EqualityJournal of the ACM, 1971
- The Unit Proof and the Input Proof in Theorem ProvingJournal of the ACM, 1970
- Heuristic Search ProgramsPublished by Springer Science and Business Media LLC ,1970
- Refinement theorems in resolution theoryPublished by Springer Science and Business Media LLC ,1970
- Theorem-Proving for Computers: Some Results on Resolution and RenamingThe Computer Journal, 1966
- Efficiency and Completeness of the Set of Support Strategy in Theorem ProvingJournal of the ACM, 1965
- On sentences which are true of direct unions of algebrasThe Journal of Symbolic Logic, 1951