First order definite clause

A first order definite clause is a Horn clause with exactly one positive atom (and 0 or more negative atoms). It is of the form:

$$\forall x_1\dots \forall x_n\neg A_1\vee \dots \neg A_m\vee A$$

Where $m\ge 0$, $A_1,\dots ,A_m,A$ are atoms, and $x_1,\dots ,x_n$ are all the variables appearing in the atoms.