### Unit Refutations and Horn SetsUnit Refutations and Horn Sets

Access Restriction
Subscribed

 Author Henschen, L. ♦ Wos, L. Source ACM Digital Library Content type Text Publisher Association for Computing Machinery (ACM) File Format PDF Copyright Year ©1974 Language English
 Subject Domain (in DDC) Computer science, information & general works ♦ Data processing & computer science 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 $\textit{S}$ is an unsatisfiable Horn set, there exists a strictly-unit refutation of $\textit{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 $\textit{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. ISSN 00045411 Age Range 18 to 22 years ♦ above 22 year Educational Use Research Education Level UG and PG Learning Resource Type Article Publisher Date 1974-10-01 Publisher Place New York e-ISSN 1557735X Journal Journal of the ACM (JACM) Volume Number 21 Issue Number 4 Page Count 16 Starting Page 590 Ending Page 605

#### Open content in new tab

Source: ACM Digital Library