Now to the actual definition of Horn clause. First, some standard logical terminology. A term is simply an expression built out of variables and function symbols. For example, x y-1 z is a term in the language of groups. An atomic formula is a formula that consists of relation symbols (including equality) applied to terms. So xy = yx is an example of an atomic formula in the language of groups. What makes an atomic formula atomic is that it’s not built out of smaller logical formulas.
A Horn clause is built out of atomic formulas in a particular way. Let A_1, … A_n and B
be atomic formulas. Then a Horn clause is a logical formula of the form
A_1 and … and A_n implies B.
As a degenerate special case, the left-hand side of the implication can be empty, which is the same as asserting formula B holds unconditionally.