Horn Clause Form.

<Exp>      ::= <rule> |
               <query>
<rule>     ::= <atom> |                       eg.     parents(fred, anne, bill)
               <atom> <= <literals>           eg. parent(C,M) <= parents(C,M,D)
<query>    ::= ? <literals>                   eg.    ? grandparent(william,Who)
<literal>  ::= atom | not <atom>
<literals> ::= <literal> [and <literals>]
<atom>     ::= <predicate_ident> [ ( <terms> ) ]              eg. diff(X, X, 1)
<term>     ::= <ident> ( <terms> )  | <constant> | <variable>
<terms>    ::= <term> [, <terms>]

 --- Horn Clause Form. ---

Horn clause form permits the statement of simple atomic facts and of simple implications. These restricted forms are in fact sufficient to express any first-order predicate logic expression although several Horn clause expressions may be needed to do so.

All variables are implicitly quantified and quantifiers are omitted.

implicit:
   p(X) <= q(X,Y)    is equivalent to    p(X) or not q(X,Y)
   ? p(X)                                ? not p(X)

explicit:
   forAll X p(X) <= eXists Y q(X,Y)                  forAll X forAll Y p(X) or not q(X,Y)
   ? eXists X p(X)                             ? forAll X not p(X)

 --- Quantification. ---

A variable which appears to the left of `<=' is universally quantified. A variable which appears in a query or only to the right of '<=' is existentially quantified. The proof of a query is equivalent to a proof by contradiction that the negated query fails.

  forAll C forAll GP grandparent(C,GP) <= eXists P parent(C,P) and parent(P,GP)
= forAll C forAll GP grandparent(C,GP) or not(eXists P parent(C,P) and parent(P,GP))
= forAll C forAll GP forAll P grandparent(C,GP) or not parent(C,P) or not parent(P,GP)

Example with Explicit Quantification.