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

1 Answer 1

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 and acknowledge that you have read and understand our privacy policy and code of conduct.

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