To introduce logic programs, consider the following two logic programs grandparent and nat:
| parent(jef,paul). parent(paul,ann). grandparent(X,Y) :- parent(X,Z), parent(Z,Y). |
|
nat(0). nat(s(X)) :- nat(X). |
Formally speaking, we have that grandparent/2, parent/2,
and nat/1 are predicates (with their arity, i.e., number of arguments listed explicitly).
Furthermore, jef, paul and ann are constants and X, Y and Z are variables.
All constants and variables are also terms . In addition, there exist structured terms such
as s(X), which contains the functor s/1 of arity 1 and the term X.
Constants are often
considered as functors of arity 0. A first order alphabet is a set of predicate symbols,
constant symbols and functor symbols. Atoms are predicate symbols followed
by the necessary number of terms, e.g., parent(jef, paul), nat(s(X)), parent(X, Z),
etc. Literals are atoms (s(X)) (positive literal) and their negations not nat(s(X))
(negative literals). We are now able to define the key concept of a definite clause.
Definite clauses are formulas of the form,
A :- B1,...,Bm |
where A and the Bi are logical atoms and all variables are understood to be universally
quantified. For instance, the clause c
grandparent(X,Y) :- parent(X,Z), parent(Z,Y) |
can be read as X is the grandparent of Y if X is a parent of Z and Z is a parent of Y. We call grandparent(X,Y) the head(c) of this clause, and parent(X,Z), parent(Z,Y) the body(c). Definite clauses are often simply called clauses. Clauses with an empty body such as parent(jef, paul) are facts. A (definite) clause program (or logic program for short) consists of a set of clauses. Thus, above, there are thus two logic programs, one defining grandparent/2 and one defining nat/1. The set of variables in a term, atom, conjunction or clause E, is denoted as Var(E), e.g., Var(c) = {X, Y, Z}. A term, atom or clause E is ground when there is no variable occurring in E, i.e. Var(E) is the empty set. A clause c is range-restricted when all variables in the head of the clause also appear in the body of the clause.
A substitution s = {V1/t1,..., Vn/tn}, e.g. {Y/ann}, is an assignment
of terms ti to variables Vi. Applying a substitution to a term, atom or clause e yields the
instantiated term, atom, or clause e where all occurrences of the variables Vi are
simultaneously replaced by the term ti, e.g. cs is
| grandparent(X, ann) :- parent(X, Z), parent(Z, ann). |
A substitution is the most general unifier mgu(a,b) of atoms a and b if and only if a = b and for each substitution t such that a = bt, there exists a substitution u such that t = su.
A clause c1 theta-subsumes a clause c2 if and only if there exists a
substituion s such that all atoms in c1s consitute a subset of the atoms in c2.
For instance,
| p(X) :- q(X) subsumes p(X) :- q(X), r(Y). |
Theta-subsumption is reflexive and transitive, but
not antisymmetric as
| p(X) :- q(X) and p(X) :- q(X), q(Y) |
show. Thus, theta-subsumption defines a pre-order on the set of clauses, i.e., a partially ordered set of equivalence classes. We say that a clause is reduced if it does not theta-subsume any of its subclauses. Every equivalence class contains a reduced clause that is unique up to variable renaming. The set of equivalence classes forms a lattice, i.e., two clauses have a unique least upper bound and a greater lower bound under Theta-subsumption. The least general generalization (least upper bound) of two conjunctions (clauses) under (theta-)subsumption is called lgg and is the least general conjunction (clause) that is subsumed by both conjunctions (clauses). The greatest lower bound (glb) of two conjunctions (clauses) A and B is the most general conjunction (clause) that is subsumed by both A and B.
The Herbrand base of a logic program P, denoted as hb(P), is the set of all
ground atoms constructed with the predicate, constant and function symbols in the
alphabet of P.
Example
The Herbrand bases of the nat and grandparent logic programs are
hb(nat) = {nat(0), nat(s(0)), nat(s(s(0))), ...}
and
hb(grandparent) = {parent(ann, ann), parent(jef, jef),
parent(paul, paul), parent(ann, jef),parent(jef, ann), ...,
grandparent(ann, ann), grandparent(jef, jef), ...}.
|
A Herbrand interpretation for a logic program P is a subset of hb(P). A Herbrand interpretation I is a model of a clause c if and only if for all substitutions s such that body(c)s is a subset of I, head(c)s is also an element of I. The interpretation I is a model of a logic program P if I is a model of all clauses in P. A clause c (logic program P) entails another clause c0 (logic program P0), denoted as c |= c0 (P |= P0), if and only if, each model of c (P) is also a model of c0 (P0). Clearly, if clause c (program P) theta-subsumes clause c0 (program P0) then c (P) entails c0 (P0), but the reverse is not true.
The least Herbrand model LH(P), which constitutes the semantics of the logic
program P, consists of all facts f of hb(P) such that P logically entails f, i.e. P |= f.
Various methods exist to compute the least Herbrand model. We merely sketch its
computation through the use of the immediate consequence operator TP . The
operator TP is the function on the set of all Herbrand interpretations of P such that
for any such interpretation I we have
| TP(I) = {A |there is a substitution and a clause A :- A1,..., An in P such that A :- A1,..., An is ground and for i = 1,..., n Ai is an element of I}. |
Now, it can be shown that the least Herbrand model of a logic program P is the least fixpoint of TP . That is, let I(0) be the empty set; and I(n+1) = TP(I(n)) for n = 0,1,2,..., then the least Herbrand model of P is the I(m) with smallest m greater than 0 such that I(m+1) = I(m). In case of functor-free, range-restricted clauses, the least Herbrand model can be obtained using the following procedure:
That is, initialize LH to the empty set, and then add all ground facts head(c) to LH
for which there exists a clause c in P and a substitution s such that body(c)s is a
subset of LH. Such ground facts are called immediate consequences of body(c). Repeat this
last step until a fixpoint is reached (i.e.LH does not change any more).
Example
At this point, you may want to verify that
LH(grandparent) = {parent(jef,paul), parent(paul,ann), grandparent(jef,ann)}
and
LH(nat) = hb(nat). |
All ground atoms in the least Herbrand model are provable. Proofs are typically constructed using the SLD-resolution procedure: given a goal :- G1, G2,...,Gn and a clause G :- L1,...,Lm such that G1s = Gs, applying SLD resolution yields the new goal :- L1,...,Lm, G2,...,Gn. A successful refutation, i.e., a proof of a goal is then a sequence of resolution steps yielding the empty goal, i.e. :- . Failed proofs do not end in the empty goal.