2
$\begingroup$

I am currently studying model theory and I am trying to decide if a clause is a Horn Clause. I know that a Horn Clause is a clause with at most one positive literal, but there are some clauses that it is not easy to decide whether they are Horn or not.

E.g.,

(P->Q)->W

Is there any way to decide whether this clause is Horn or not, or do I have to make further calculations in order to bring it to a Disjunction form?

$\endgroup$
  • 1
    $\begingroup$ $(P \to Q) \to W$ is not a clause, so in particular it's not a Horn clause. $\endgroup$ – Yuval Filmus Feb 23 '14 at 14:30
  • $\begingroup$ @YuvalFilmus What I meant is that this can be transformed to a clause.. And then it may be a Horn clause. How can you know that by transforming this into CNF won't be a Horn Clause $\endgroup$ – Mario Feb 23 '14 at 14:38
  • 1
    $\begingroup$ If you eliminate the implies, you get $\lnot(\lnot P \vee Q) \vee W = (P \wedge \lnot Q) \vee W$, which is not a clause. $\endgroup$ – Yuval Filmus Feb 23 '14 at 18:01
  • $\begingroup$ @YuvalFilmus can't this be considered as a literal (P∧¬Q)? $\endgroup$ – Mario Feb 23 '14 at 18:03
  • 1
    $\begingroup$ No, a literal is either a variable or a negation of a variable. A clause is a disjunction of literals. Your formula $(P\to Q)\to W$ is not a clause, and moreover it is not even equivalent to a clause. A formula is a Horn clause if it is equivalent to a clause in which at most one variable appears positively. $\endgroup$ – Yuval Filmus Feb 23 '14 at 18:10
5
$\begingroup$

Let's start with some definitions:

  1. A literal is either a variable (a positive literal) or the negation of a variable (a negative literal).

  2. A clause is a formula which is equivalent to a disjunction of literals.

  3. A Horn clause is a formula which is equivalent to a disjunction of literals, at most one of which is positive.

Your formula $(P \to Q) \to W$ is not equivalent to a disjunction of literals. Indeed, if it were, since it depends on all variables $P,Q,W$, it would have exactly one falsifying assignment (with respect to $P,Q,W$). Yet it has three: $(P,Q,W)=(F,F,F),(F,T,F),(T,T,F)$. So it is not a clause, and in particular not a Horn clause.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.