At most one positive literal
The clause ¬p∨¬q∨r has one positive literal and can be written (p∧q)→r. If both premises hold, r must hold. A Horn clause with one positive literal is definite, and a unit fact r requires r without substantive premises.
The all-negative clause ¬p∨¬q is Horn too: (p∧q)→false forbids p and q from holding together. At most one positive literal is not the same as exactly one, and negative literals do not disqualify a clause.
References: [1]
Propagating only forced truth
For a finite propositional Horn formula, begin with every variable false. When an implication has a true body but a false variable head, make that head true; if its head is false itself, report unsatisfiable. A fact p and rule p→q force q, which conflicts with an additional q→false.
Each variable changes from false to true at most once. The current valuation stays below every satisfying valuation because only forced truths are added. If all rules become satisfied without a contradiction, the result is the least model in the componentwise false-before-true ordering.
References: [1]
Scope of the propositional result
Even the straightforward repeated-scan algorithm has a polynomial bound. Tracking unmet premises and variable occurrences can avoid redundant checks. The efficiency depends on Horn structure; an arbitrary CNF cannot be solved merely by moving upward from the all-false assignment.
Prolog and Datalog use first-order Horn rules for parameterized relations, introducing substitution and search. Terms, function symbols and evaluation strategy affect the problem. The rule shape alone does not prove program termination or make the finite propositional procedure a universal logic-program executor.