ABOUT HORN CLAUSE

Definition: A Horn clause is a clause with at most one positive literal.
Any Horn clause therefore belongs to one of four categories:
A rule: 1 positive literal, at least 1 negative literal. A rule has the form "~P1 V ~P2 V ... V ~Pk V Q". This is logically equivalent to "[P1^P2^ ... ^Pk] => Q"; thus, an if-then implication with any number of conditions but one conclusion. Examples: "~man(X) V mortal(X)" (All men are mortal); "~parent(X,Y) V ~ancestor(Y,Z) V ancestor(X,Z)" (If X is a parent of Y and Y is an ancestor of Z then X is an ancestor of Z.)
A fact or unit: 1 positive literal, 0 negative literals. Examples: "man(socrates)", "parent(elizabeth,charles)", "ancestor(X,X)" (Everyone is an ancestor of themselves (in the trivial sense).)
A negated goal : 0 positive literals, at least 1 negative literal. In virtually all implementations of Horn clause logic, the negated goal is the negation of the statement to be proved; the knowledge base consists entirely of facts and goals. The statement to be proven, therefore, called the goal, is therefore a single unit or the conjuction of units; an existentially quantified variable in the goal turns into a free variable in the negated goal. E.g. If the goal to be proven is "exists (X) male(X) ^ ancestor(elizabeth,X)" (show that there exists a male descendent of Elizabeth) the negated goal will be "~male(X) V ~ancestor(elizabeth,X)".
The null clause: 0 positive and 0 negative literals. Appears only as the end of a resolution proof

OR
A Horn clause is a clause with at most one expression on the left of the arrow. The expression on the left of the arrow (if there is one) is called the head of the clause. The expression(s) to the right of the arrow (if there are any) make up the body of the clause. The four possible types of Horn clause are conventionally named as follows.
1.Facts
Clauses of the form A¬ . (Facts have a head but no body.)
2.Rules
Clauses of the form A¬ B1,...,Bn. (Rules have both a head and a body.)
3Goals
Clauses of the form ¬ B1,...,Bn . (Goals have a body, but no head.)
4.Empty Clause
The clause \Box, with no head and no body.