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