% Draft of a self-contained writeup on the standard
% (least fixed point / least Herbrand model) semantics of Horn logic programs.
% That semantics is normative for the Horn logic programs sublanguage of RuleML.
% The corresponding current RuleML DTD is
% http://www.ruleml.org/dtd/0.8/ruleml-urhornlog-monolith.dtd ;
% that also includes some extra syntactic features (e.g., URI constant names,
% unordered argument collections)
Horn Logic Program Semantics for RuleML
Benjamin Grosof
MIT Sloan School of Management
bgrosof@mit.edu http://ebusiness.mit.edu/bgrosof
Draft of May 9, 2003
The language of a Horn logic program, like a first-order language
signature, is determined by its individual constants,
(logical-)function constants, and predicate constants -- these
together are called its *signature*. A (logical-)function is also
known as a constructor. An individual constant is sometimes also
known as an object constant. A function has arity greater than 0.
(Note that this is easy to generalize; one can view an individual
constant as a function constant with arity zero.) Terms are built as
in the corresponding first-order language. Atoms have the form
p(t_1,...,t_n), where the t's are terms and p is a predicate symbol of
arity n. "LP" abbreviates "logic program".
A Horn rule (a.k.a. definite rule) is an expression of the form
H <- B_1 /\ ... /\ B_m . (1)
where B_i's are atoms, m is greater-than-or-equal to zero (i.e., m >=
0), and "/\" stands for logical conjunction. ("/\" is sometimes
written as "and".) The left-hand side of the rule is called the
rule's head or consequent; the right-hand is called the rule's body or
antecedent. "<-" is called implication, and intuitively can be read
as "if". (Note that "<-" is similar to, but not quite the same as,
material implication in classical logic.) A collection of Horn rules
is called a Horn logic program. It is also referred to as a definite
logic program. A logic program is also called a rulebase. Formulas
and rules not containing variables are called ground. Unless
otherwise stated, the notational convention is that logical variable
are prefixed with a "?". If m=0 and H is ground, then the rule is
called a *fact*. More generally, if m=0, the "<-" may be omitted
notationally. In this case, the body is empty and is defined to be
equivalent logically to True. E.g., a fact H (where H is ground) can
be written simply as:
H .
In Prologs, the usual notational convention is that variables begin with a
capital letter, "<-" is replaced by ":-", and "/\" is replaced by ",".
For a FOL formula E[?x1,...,?xm] whose free variables are ?X=(?x1,...,?xm),
we say that (for all ?X. E[?X]) (respectively, (there exists ?X. E[?X]))
is the *universal closure* (respectively, *existential closure*) of E.
Another way we speak of this is to say that E is universally
(respectively, existentially) quantified at outermost scope.
Notationally, in writing a universal or existential closure, sometimes
we simply omit the variables immediately after the quantifier.
We define the *classical version* of the rule (1)
to be the Horn FOL axiom to be the universal closure of rule (1),
where "<-" is treated as material implication.
Likewise, we define the classical version of a Horn LP rulebase R to
consist of the classical versions of every rule in R.
In Horn *LP*, each rule of form (1) can be viewed as universally
quantified at outermost scope, with the notation simply leaving this
quantification implicit. However, note that the usual definition of
the semantics of Horn LP (i.e., the one we give below, called the
least fixed point semantics) does not use the formal notion of a
universal quantifier *within* the language.
The set of all ground terms in the language of a rulebase R will be
denoted by HU(R) (Herbrand universe of R) with R omitted notationally
whenever possible. The set of all ground atoms in the language of a
rulebase R will be denoted by HB(R) (Herbrand base of R) with R
omitted notationally whenever possible. For a predicate p, atoms (p)
will denote the subset of HB(R) formed with predicate p. For a set of
predicates Q, atoms(Q) will denote the subset of HB(R) formed with the
predicates in Q.
Unless stated otherwise, a rule with variables stands for the set of
all its ground instantiations; and thus, likewise, a rulebase (where
some rules contain variables) stands for the set of all its ground
instantiations. Note that a rule without variables trivially stands
for the set of all its ground instantiations. Note also that the
ground instantiations of a rulebase consist of all the ground
instantiations of all of its rules. Thus we can restate the previous
three sentences more simply as: a rulebase stands for the set of all
its ground instantiations.
The form of a *normal* logic program, a.k.a. "ordinary" logic program
(also sometimes known as a "general" [sic] logic program -- but
there are actually several further generalizations), generalizes
that of a Horn logic program, so as to permit body literals to
be negated by negation-as-failure. A rule in a normal logic program
is an expression of the form:
H <- B_1 /\ ... /\ B_m /\ ~B_m+1 /\ ... /\ ~B_n . (2)
where "~"stands for negation-as-failure (NAF).
The *model* of a Horn logic program R is the smallest subset S of HB
such that for any rule of form (1) in R, if B_1, ..., B_m are each
in S, then H is also in S. Notationally, this model is denoted by mod(R).
A way to view this definition is that the model of R is the least fixed
point of a certain operator T_R, which we define below.
This definition is thus also known as the "least fixed point" semantics.
The model of R is also known as the "least Herbrand model" or
"least fixed point model".
Definition of Operator T_R:
Let R_1 be a ground rule of form (1).
We define an operator T_R1 which takes as input any subset V of HB,
and which generates as output a subset W of HB, where W is a superset of V.
The operator T_R1 adds the head of R1 to W if the body of R1 is satisfied
in V; if not, W is just the same as V.
I.e.,
T_R1 : 2^HB -> 2^HB
if B_1, ..., B_m are each in V, then W = (V union {H}),
else W=V.
Intuitively, the operator T_R1 represents the effect of a
single iteration of applying the rule R_1 to a working fact set V
(e.g., intermediate conclusions in the course of inferencing).
If the rule's body is satisfied, i.e., if the rule fires,
then the rule's head is added to the new working fact set W.
More generally, we extend this operator concept to sets of rules.
Let R be a Horn logic program, consisting of rules R_1, ..., R_k.
We define an operator T_R which takes as input any subset V of HB,
and which generates as output a subset X of HB, where X is a superset of V.
X = T_R(V) = the union of T_R1(V), ..., T_Rk(V).
Intuitively, the operator T_R represents the effect of a
single iteration of applying all the rules R_1,...,R_k to a working fact set V
(e.g., intermediate conclusions in the course of inferencing).
For each rule, if the rule's body is satisfied, i.e., if the rule fires,
then the rule's head is added to the new working fact set X.
Another way to view this intuitively is that T_R is the
"constructive implication operator" for R.
In the least fixed point semantics for Horn logic programs,
the model of R is defined to be the least fixed point of T_R,
i.e., the smallest subset S of HB such that S = T_R(S).
(End of definition of T_R.)
There are several different semantics for normal logic programs that
have been defined in the literature; we recommend the well-founded
semantics [Van Gelder et al 1991].
For the case of definite logic programs, most (if not all) of these
different semantics, including in particular the well-founded
semantics, coincide with (i.e., are equivalent to) the
least-fixed-point semantics. More generally, most (if not all) of
these different semantics coincide with the well-founded semantics,
for the case of stratified logic programs.
The various semantics for normal logic programs defined in the literature
differ primarily in their treatment of certain non-stratified cases involving
the interaction of negation-as-failure with cyclic dependencies
among predicates or atoms.
In this short paper, however, we will not be defining or discussing
the detailed semantics of normal logic programs that do contain NAF.
Entailment:
A ground atom A is *True* in S iff A is in S (i.e., if A is a member of S).
Thus A is True in mod(R) iff A is in mod(R). Iff A is True in mod(R),
then A is said to be *entailed* by R, i.e., a *conclusion* of R,
and to have *truth value* True.
If A is not True in mod(R), then A is said to be not entailed by R, i.e.,
not a conclusion of R.
If A is not True in mod(R), A is also sometimes said to have truth
value *Fail* or *NAF*. Fail also often known as "*False*". Note that
in this context "False", however, does *not* correspond to classical falsity,
i.e., to classical negation! Rather it corresponds to negation-as-failure.
Intuitively: if A has truth value Fail, then A is not believed;
whereas, in *classical* logic, if A has truth value (classical-)false,
then A is believed to be false, i.e., not-A is believed to be true.
In *normal* logic programs, iff A has truth value *Fail*, then ~A is
said to be True in mod(R). Intuitively, *Fail* corresponds roughly to
"either classically false or unknown". The general semantics of NAF in normal
LP's has subtleties, however. E.g., the well-founded semantics in
general may assign a third truth value "*undefined*" to some atoms.
The definition of entailment is extended to conjunctive
formulas via the following truth recursion.
A conjunction of ground atoms A_1 /\ ... /\ A_m is True
iff each conjunct A_i (for i=1,...,k) is True.
More generally, a conjunction is true iff one of its conjuncts is true.
We call the above definition of entailment: "*basic*" entailment.
Query-answering in which bindings are returned is then straightforwardly
defined. Let the query formula be the existential closure of a
conjunction of atoms. Then entailed bindings correspond to the entailed
ground instances of that conjunction of atoms.
Relationship to Horn FOL:
The model of R is the least Herbrand model, in the sense that
it is the greatest lower bound w.r.t. inclusion. That is,
the model of R is exactly the set of ground atoms that are entailed
in classical FOL semantics by the classical version of the Horn LP.
Terminologically, "Horn clause" in FOL also permits the clause to
havfe an empty head, i.e., for the clause to have no positive literal.
A "Horn LP rule" as defined here does *not* permit the head to be
empty. In the LP literature an empty-head clause is often known as a
"goal", or sometimes as an "integrity constraint" [sic].
Classically Sound but Incomplete:
Basic entailment is conservative in that it is "*classically sound*",
by which we mean sound w.r.t. the classical (FOL) entailments of the
classical version of the rulebase R (i.e., viewing R as a set of Horn
FOL axioms). In general, it is weaker than (i.e., incomplete w.r.t.)
the classical entailment of the classical version of the rulebase R.
Example: Friendliness.
For example, consider the following Horn LP rulebase G:
friendly(?x) <- good(?x) .
attractive(?x) <- friendly(?x) /\ bouncy(?x).
good(fred).
friendly(sue).
bouncy(fred).
This entails exactly the conclusions
{good(fred), friendly(sue), bouncy(fred), friendly(fred), attractive(fred)}
The classical version of G also entails various formulas which the
Horn LP G does not; some of these are:
friendly(sue) \/ friendly(fred).
forall ?x. attractive(?x) <- good(?x).
attractive(sue) <- bouncy(sue).
bouncy(fred) <- bouncy(fred).
forall ?x. friendly(?x) \/ bouncy(?x) <- friendly(?x).
bouncy(sue) <-> attractive(sue).
attractive(sue) \/ not attractive(sue).
where "not" is classical negation and "<->" is classical equivalence.
We call this list of non-entailed formulas "more-G-stuff", for
later reference.
Extensions of the definition of entailment:
There is also a sizable LP KR literature that addresses *extensions* to
this basic concept of entailment so as to answer queries in more
general form. These extensions can usually be viewed as reducing
inferencing w.r.t. the extended entailment concept to inferencing w.r.t.
the basic entailment concept. For example, most or all
of the formulas in more-G-stuff could be inferred by systems that
use extended concepts of entailment. However, we do not have
space or focus to address these entailments in detail in this paper.
Sources:
Parts of this were adapted from [Baral and Gelfond 1994] and [Lloyd 1987].
[Lloyd 1987] gives a good treatment of the semantic foundations of Horn LP
(which is called "definite LP" there).
References:
[Baral and Gelfond 1994]
Chitta Baral and Michael Gelfond, "Logic Programming and Knowledge
Representation", J. Logic Programming, 1994.
[Lloyd 1987]
John W. Lloyd, Foundations of Logic Programming, Second, Extended
edition, Springer, Berlin, 1987.
[Van Gelder et al 1991]
Allen Van Gelder, Kenneth A. Ross, and John S. Schlipf,
"The Well-Founded Semantics for General Logic Programs," J. ACM, 38:3,
pp. 620-650, July 1991. http://www.cs.columbia.edu/~kar/pubsk/wfjacm.ps.