# Recognizing Horn clauses

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?

• $(P \to Q) \to W$ is not a clause, so in particular it's not a Horn clause. – Yuval Filmus Feb 23 '14 at 14:30
• @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 – Mario Feb 23 '14 at 14:38
• 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. – Yuval Filmus Feb 23 '14 at 18:01
• @YuvalFilmus can't this be considered as a literal (P∧¬Q)? – Mario Feb 23 '14 at 18:03
• 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. – Yuval Filmus Feb 23 '14 at 18:10

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.