Is "~A=>B" a horn clause?

Question

I just get confused for the definition of horn clause. Is "~A=>B" a horn clause? If we convert it into disjunction forms, it will be "AvB" which is not a horn clause.

So I wonder whether it is a horn clause. Thanks.

Answer 1

~AvB would be a horn clause. Which is equivalent to A=>B. (At most one positive literal)

Answer 2

A Horn clause is a disjunction of literals with at most one positive literal, i.e.

~p1(...) \/ ~p2(...) \/ ... \/ ~pn(...) [ \/ p(...) ]

This can be, just for facilitating readability, written as

p(...) <= p1(...), p2(...), ..., pn(...).

So, if A and B are atoms, B <= ~A is not a Horn clause since this corresponds to the logical form A \/ B which has two positive literals.

The other way round, there are only positive literals allowed in the form written with "=>" and commas, and at most one literal / atom in the head of the implication. If there is no atom in the head, the clause is a query clause which is also legal.