## 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.**

[Previous Page]
[Next Page]
[Index]
© L. Allison, Dept. Computer Science, Monash University