Which is the definition of a Horn formula being positive? 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.
 A: 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$.
