Horn Clauses

A clause is defined as a sum (logical OR) of Literals. A Literal is either:

1. an atomic formula (denoted as $p(A_1,\ldots,A_n)$), or
2. a negated atomic formula (denoted as $\bar{p}(A_1,\ldots,A_n)$ or $\neg{p}(A_1,\ldots,A_n)$).

A negated atomic formula is a Negative Literal. A not negated formula is a Positive Literal.

A Horn Clause is a clause with at most one positive literal, it is thus either:

1. A single positive literal, which is regarded as a fact,
2. One or more negative literals, with no positive literal, or
3. A positive literal and one or more negative literals which is a rule.

A subset of Horn Clauses, generated by groups 1 and 3, expresses knowledge in Datalog.

Horn Clauses of group 3 are considered rules [22]. The following Horn Clause:

$$\bar{p}_1 \vee \cdots \vee \bar{p}_n \vee q$$ (4.1)

is logically equivalent to:

$$p_1 \wedge \cdots \wedge p_n \rightarrow q$$ (4.2)

where $q$ is called the head of the rule, and $p_1 \wedge \cdots \wedge p_n$ is called the body. Each of the $p_i$ is called a subgoal; $q$ can also be called the conclusion, and $p_i$ can be called the preconditions.