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_1and … andA_nimpliesB.

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.