1
$\begingroup$

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.

$\endgroup$
2
  • $\begingroup$ I would have guessed that a positive Horn formula was a Horn formula which is also a positive formula, which would mean that each conjunct has the form PH1, since PH2 and PH3 are not positive formulas. I seem to recall seeing "strict Horn formula" used for a Horn formula where each conjunct is PH1 or PH2 but I could be remembering wrong, that would have been in a bygone millennium. $\endgroup$
    – bof
    Commented Sep 5, 2020 at 2:09
  • $\begingroup$ I deleted my answer after realizing I had not properly read Ebbinghaus' definition and your question. The notion of positivity makes sense for Horn clauses, i.e. members of the conjunction, which is what I was elaborating on in my answer; but I have nowhere seen it applied, nor do I see how it can be applied according to this definition, to entire Horn formulas. $\endgroup$ Commented Sep 6, 2020 at 22:20

1 Answer 1

1
$\begingroup$

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$.

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .