Which is the definition of a Horn formula being positive?

Question

On p208 of Ebbinghaus' Mathematical Logic

Every Horn formula is a formula in conjunctive normal form, ..., every member of the conjunction has the form (PHI), (PH2) or (PH3):

(PH1) $q$

(PH2) $(q_0 \land ... \land q_n \to q)$

(PH3) $(\neg q_0 \lor ... \lor \neg q_n). $

Horn formulas of the form (PH1) or (PH2) are called positive, those of the form (PH3) negative.

Which is the definition of a Horn formula being positive:

• a formula in CNF, whose members are either PH1 or PH2? (My guess)

• a formula which is either PH1 or PH2? (By the last sentence in the quote) (My guess, after reading the remaining of p208 and p209)

Thanks.

Answer 1

Compare with a different source: Horn Formulas.

Definition: A formula $F$ in CNF is a Horn formula if every disjunction in $F$ contains at most one positive literal.

A disjunction in a Horn formula can equivalently be viewed as an implication $K \to B$ where $K$ is a conjunction of atoms.

According to the above definition, (PH1), (PH2) and (PH3) are all examples of Horn formulas, because (PH2) : $(q_0 \land \ldots \land q_n \to q)$, when written in CNF, will be:

$(\lnot q_0 \lor \ldots \lor \lnot q_n \lor q)$

and we have only one (and thus: at most one) positive literal: $q$.

In conclusion, according to Ebbinghaus definition, an Horn formula is a formula:

$(\lnot q_0 \lor \ldots \lor \lnot q_n \lor q) \land \ldots \land (\lnot r_0 \lor \ldots \lor \lnot r_m)$

where $n$ can be $0$.

---

Why in the following discussion regarding the satisfiability algorithm for Horn formulas the author consider only the negative and positive ones ?

Simply because, being an Horn formula $\alpha$ a conjunction, it will be satisfiable iff every conjunct is, and thus the author consider equivalently the set $\Delta$ of members of the conjunction $\alpha$.