Under consideration for publication in Theory and Practice of Logic Programming

1

arXiv:1405.3365v1 [cs.PL] 14 May 2014

A Well-Founded Semantics for FOL-Programs
Yi Bi1 , Jia-Huai You2 , Zhiyong Feng1
1 Tianjin
2 University

University, Tianjin China
of Alberta, Edmonton T6G 2E8, Canada

submitted 1 January 2003; revised 1 January 2003; accepted 1 January 2003

Abstract
An FOL-program consists of a background theory in a decidable fragment of first-order logic and a
collection of rules possibly containing first-order formulas. The formalism stems from recent approaches
to tight integrations of ASP with description logics. In this paper, we define a well-founded semantics for
FOL-programs based on a new notion of unfounded sets on consistent as well as inconsistent sets of literals,
and study some of its properties. The semantics is defined for all FOL-programs, including those where it
is necessary to represent inconsistencies explicitly. The semantics supports a form of combined reasoning
by rules under closed world as well as open world assumptions, and it is a generalization of the standard
well-founded semantics for normal logic programs. We also show that the well-founded semantics defined
here approximates the well-supported answer set semantics for normal DL programs.
To appear in Theory and Practice of Logic Programming (TPLP).
KEYWORDS: Logic Programs, Well-Founded Semantics, First-Order Logic.

1 Introduction
Recent literature has shown extensive interests in combining ASP with fragments of classical
logic, such as description logics (DLs) (see, e.g., (de Bruijn et al. 2008; de Bruijn et al. 2007;
Eiter et al. 2008; Lukasiewicz 2010; Motik and Rosati 2010; Rosati 2005; Rosati 2006; Shen and Wang 2011;
Yang et al. 2011)). A program in this context is a combined knowledge base KB = (L, Π), where
L is a knowledge base of a decidable fragment of first-order logic and Π a set of rules possibly
containing first-order formulas or interface facilities. In this paper, we use FOL-program as an
umbrella term for approaches that allow first-order formulas to appear in rules (the so-called tight
integration), for generality. The goal of this paper is to formulate a well-founded semantics for
these programs with the following features.
• The class of all FOL-programs are supported.
• Combined reasoning with closed world as well as open world assumptions is supported.
Under the first feature, we shall allow an atom with its predicate shared in the first-order
theory L to appear in a rule head. This can result in two-way flow of information and enable
inferences within each component automatically. For example, assume L contains a formula
that says students are entitled to educational discount, ∀x St(x) ⊃ EdDiscount(x). Using the
notation of DL, we would write St ⊑ EdDiscount. Suppose in an application anyone who is
not employed full time but registered for an evening class is given the benefit of a student. We
can write a rule
St(X) ← EveningClass(X), not HasJob(X).

2

Y. Bi. J. You. Z. Feng.

Thus, that such a person enjoys educational discount can be inferred directly from the underlying
knowledge base L.
To support all FOL-programs, we need to consider the possibility of inconsistencies arising
in the construction of the intended well-founded semantics. For example, consider an FOLprogram, KB = (L, Π), where L = {∀xA(x) ⊃ C(x), ¬C(a)} and Π = {A(a) ← not B(a);
B(a) ← B(a)}. Suppose the Herbrand base is {A(a), B(a)}. In an attempt to compute the wellfounded semantics of KB by an iterative process, we begin with the empty set; while L entails
¬A(a), since B(a) is false by closed world reasoning, we derive A(a) resulting in an inconsistency. This reasoning process suggests that during an iterative process a consistent set of literals
may be mapped to an inconsistent one and, in general, whether inconsistencies arise or not is not
known a priori without actually performing the computation.
That the well-founded semantics of an FOL-program is defined by an inconsistent set can be
useful on its own, or in the computation of (suitably defined) answer sets of the program. If we
have computed the well-founded semantics which is inconsistent, we need not pursue the task of
computing answer sets of the same program, because they do not exist.
In complex real world reasoning by rules, it is sometimes desirable that not all predicates are
reasoned with under the closed world assumption. Some conditions may need to be established
under the open world assumption. We call this combined reasoning. For example, we may write
a rule
P rescribeT o(X, Q) ← Effective(X, Z), Contract(Q, Z), ¬AllergicT o(Q, X)
to describe that an antibiotic is prescribed to a patient who contracted a bacterium, if the antibiotic against that bacterium is effective and patient is not allergic to it. Though Effective can be
reasoned with under the closed world assumption, it may be preferred to judge whether a patient
is not allergic to an antibiotic under the open world assumption, e.g., it holds if it can be proved
classically. This is in contrast with closed world reasoning whereas one may infer nonallergic
due to lack of evidence for allergy.
To our knowledge, there has been no well-founded semantics defined for all FOL-programs.
The closest that one can find is the definition for a subset of FOL-programs (Lukasiewicz 2010),
which relies on syntactic restrictions so that the least fixpoint is computed over consistent sets
of literals. To ensure that the construction is well-defined, it is assumed that DL axioms must
be, or can be converted to, tuple generating dependencies (which are essentially Horn rules)
plus constraints. Thus, the approach cannot be lifted to handle first-order formulas in general.
In addition, to the best of our knowledge, no combined reasoning is ever supported under any
well-founded semantics.
As motivated above, in this paper we first define a well-founded semantics for FOL-programs
based on a new notion of unfounded sets. We show that the semantics generalizes the wellfounded semantics for normal logic programs. Also, we prove that the well-founded semantics defined here approximates the well-supported answer set semantics for the language of
(Shen and Wang 2011); namely, all well-founded atoms (resp. unfounded atoms) of a program
remain to be true (resp. false) in any well-supported answer set. This makes it possible to use
the mechanism of constructing the well-founded semantics as constraint propagation in an implementation of computing well-supported answer sets.
The paper is organized as follows. The next section introduces the language and notations. In
Section 3 we define the well-founded semantics. Section 4 studies some properties and relates

Theory and Practice of Logic Programming

3

to the well-supported answer set semantics, followed by related work in Section 5. Section 6
concludes the paper and points to future directions.
2 Language and Notation
We assume a language of a decidable fragment of first-order logic, denoted LΣ , where Σ =
hF n ; P n i, called a signature, and F n and P n are disjoint countable sets of n-ary function and nary predicate symbols, respectively. Constants are 0-ary functions. Terms are variables, constants,
or functions in the form f (t1 , ..., tn ), where each ti is a term and f ∈ F n . First-order formulas,
or just formulas, are defined as usual, so are the notions of satisfaction, model, and entailment.
Let ΦP be a finite set of predicate symbols and ΦC a nonempty finite set of constants such that
ΦC ⊆ F n . An atom is of the form P (t1 , ..., tn ) where P ∈ ΦP and each ti is either a constant
from ΦC or a variable. A negated atom is of the form ¬A where A is an atom. We do not assume
any other restriction on the vocabularies, that is, ΦP and P n may have predicate symbols in
common.
An FOL-program is a combined knowledge base KB = (L, Π), where L is a first-order theory
of LΣ and Π a rule base, which is a finite collection of rules of the form
H ← A1 , . . . , Am , not B1 , . . . , not Bn

(1)

where H is an atom, and Ai and Bi are atoms or formulas. By abuse of terminology, each Ai is
called a positive literal and each not Bi is called a negative literal.
For any rule r, we denote by head(r) the head of the rule and body(r) its body, and we define
pos(r) = {A1 , ..., Am } and neg(r) = {B1 , ..., Bn }.
A ground instance of a rule r in Π is obtained by replacing every free variable with a constant
from ΦC . In this paper, we assume that a rule base Π is already grounded if not said otherwise.
When we refer to an atom/literal/formula, by default we mean it is a ground one.
Given an FOL-program KB = (L, Π), the Herbrand base of Π, denoted HBΠ , is the set of all
ground atoms P (t1 , ..., tn ), where P ∈ ΦP occurs in KB and ti ∈ ΦC .
We denote by Ω the set of all predicate symbols appearing in HBΠ such that Ω ⊆ P n . For
distinction, we call atoms whose predicate symbols are not in Ω ordinary, and all the other
formulas FOL-formulas. If L = ∅ and Π only contains rules of the form (1) where all H, Ai and
Bj are ordinary atoms, then KB is called a normal logic program.
Any subset I ⊆ HBΠ is called an interpretation of Π. It is also called a total interpretation or
a 2-valued interpretation. If I is an interpretation, we define I¯ = HBΠ \I.
Let Q be a set of atoms. We define ¬.Q = {¬A | A ∈ Q}. For a set of atoms and negated atoms
S, we define S + = {A | A ∈ S}, S − = {A | ¬A ∈ S}, and S|Ω = {A ∈ S | pred(A) ∈ Ω},
where pred(A) is the predicate symbol of A. Let LitΠ = HBΠ ∪ ¬.HBΠ . A subset S ⊆ LitΠ
is consistent if S + ∩ S − = ∅. For a first-order theory L, we say that S ⊆ LitΠ is consistent
with L if the first-order theory L ∪ S|Ω is consistent (i.e., the theory is satisfiable). Note that
when we say S is consistent with L, both S and L must be consistent. Similarly, a (2-valued)
¯ Ω is consistent. We denote by Litc the set
interpretation I is consistent with L if L ∪ I|Ω ∪ ¬.I|
Π
c
of all consistent subsets of LitΠ . For any S ∈ LitΠ , S ′ is called a consistent extension of S if
S ⊆ S ′ ∈ LitcΠ .
Definition 1
Let KB = (L, Π) be an FOL-program and I ⊆ HBΠ an interpretation. Define the satisfaction
relation under L, denoted |=L , as follows (the definition extends to conjunctions of literals):

4

Y. Bi. J. You. Z. Feng.
1. For any ordinary atom A ∈ HBΠ , I |=L A if A ∈ I and I |= not A if A 6∈ I.
¯ Ω |= A, and I |=L not A if I 6|=L A.
2. For any FOL-formula A, I |=L A if L ∪ I|Ω ∪ ¬.I|

Let KB = (L, Π) be an FOL-program. For any r ∈ Π and I ⊆ HBΠ , I |=L r if I 6|=L body(r)
or I |=L head(r). I is a model of KB if I is consistent with L and I satisfies all rules in Π.
Example 1
To illustrate the flexibility provided by the parameter Ω, suppose we have a program KB =
(L, Π) where Π contains a rule that says any unemployed with disability receives financial
assistance, with an FOL-formula in the body
Assist(X) ← Disabled(X), not Employed(X)
Assume Ω = ΦP = {Assist, Employed}. Then, Employed is interpreted under the closed
world assumption and Disabled under the open world assumption. Indeed, unemployment can
be established by closed world reasoning for lack of evidence of employment, but disability
requires a direct proof.
3 Well-Founded Semantics
We first define the notion of unfounded set. Intuitively, the atoms in an unfounded set can be
safely assigned to false, due to persistent inability to derive their positive counterparts.
Definition 2
(Unfounded set) Let KB = (L, Π) be an FOL-program and I ⊆ LitΠ . If I ∪ L is consistent,
then a set U ⊆ HBΠ is an unfounded set of KB relative to I iff for every H ∈ U and r ∈ Π, both
of the following conditions are satisfied
(a) If head(r) = H, then
(i) ¬A ∈ I ∪ ¬.U for some ordinary atom A ∈ pos(r), or
(ii) B ∈ I for some ordinary atom B ∈ neg(r), or
(iii) for some FOL-formula A ∈ pos(r), it holds that L ∪ S|Ω 6|= A, for all S ∈ LitcΠ
with I ∪ ¬.U ⊆ S, or
(iv) for some FOL-formula A ∈ neg(r), L ∪ I|Ω |= A.
(b) L ∪ S|Ω 6|= H for all S ∈ LitcΠ with I ∪ ¬.U ⊆ S.
If I ∪ L is inconsistent, the unfounded set of KB relative to I is HBΠ .
That H is unfounded relative to I if both conditions (a) and (b) are satisfied when I ∪ L is
consistent; in particular, condition (a.iii) ensures that a positive occurrence of an FOL-formula in
the rule body is not entailed, for all consistent extensions of I ∪ ¬.U ; and condition (b) ensures
the inability to infer its positive counterpart, independent of any rules.
An FOL-formula may contain shared predicates in Ω, and those not in Ω hence not shared.
The latter are supposed to be interpreted under open world assumption. Continuing with Example
1 above, let KB = (L, Π), where
L = {∀x Certif ied(x) ⊃ Disabled(x)}
Π = {Assist(a) ← Disabled(a), not Employed(a)}
Assume Assist, Employed ∈ Ω while Certif ied and Disabled are not. Let ΦC = {a}, and
thus HBΠ = {Assist(a), Employed(a)}. Clearly, {Assist(a), Employed(a)} is an unfounded

Theory and Practice of Logic Programming

5

set relative to I = ∅, in particular because Disabled(a) is not derivable under all consistent
extensions of I. Note that, since Disabled(a) is not in HBΠ , it is not part of an unfounded set.1
Lemma 1
Let KB = (L, Π) be an FOL-program and I ⊆ LitΠ . A set of unfounded sets of KB relative to
I is closed under union, and the greatest unfounded set of KB relative to I exists, which is the
union of all unfounded sets of KB relative to I.
Proof
If I is inconsistent, the claims hold trivially. For a consistent I, suppose U1 , U2 ⊆ HBΠ are
unfounded sets (of KB relative to I), we show that U1 ∪ U2 is also an unfounded set. Let A ∈ U1 .
Since both (a) and (b) in Definition 2 hold for U1 and U2 separately, in particular, each consistent
extension of I ∪¬.(U1 ∪U2 ) is a consistent extension of I ∪¬.U1 , (a) and (b) also hold for U1 ∪U2 .
Thus A ∈ U1 ∪ U2 . By symmetry, the same argument applies to U2 . Therefore, the union of all
unfounded sets is an unfounded set, which is the greatest among all unfounded sets.
We define the operators which will be used to define the well-founded semantics.
Definition 3
Let KB = (L, Π) be an FOL-program. Define TKB , UKB , ZKB as mappings of 2LitΠ → HBΠ ,
and WKB as a mapping of 2LitΠ → 2LitΠ , as follows:
(i) If I ∪ L is inconsistent, then TKB (I) = HBΠ ; otherwise, H ∈ TKB (I) iff H ∈ HBΠ and
either (a) or (b) below holds
(a) some r ∈ Π with head(r) = H exists such that
(1) for any ordinary atom A, A ∈ I if A ∈ pos(r) and ¬A ∈ I if A ∈ neg(r),
(2) for any FOL-formula A ∈ pos(r), L ∪ I|Ω |= A, and
(3) for any FOL-formula B ∈ neg(r), L ∪ S|Ω 6|= B, for all S ∈ LitcΠ with I ⊆ S.
(b) L ∪ I|Ω |= H.
(ii) UKB (I) is the greatest unfounded set of KB relative to I.
(iii) ZKB (I) = {A ∈ HBΠ | L ∪ I|Ω |= ¬A}.
(iv) WKB (I) = TKB (I) ∪ ¬.UKB (I) ∪ ¬.ZKB (I).
The operator TKB is a consequence operator. An atom is a consequence, either due to a derivation via a rule (case (i.a)), or because it is entailed by L, given I (case (i.b)). In the first case,
the body of such a rule should be satisfied not only by I, but by all consistent extensions of I. In
the case (i.a.1) or (i.a.2), it is sufficient that the body is satisfied by I only because the classical
entailment relation is monotonic. For the case (i.a.3) the condition needs to be stated explicitly.
There are two features in this definition that are non-conventional. The first is the operator ZKB
- interacting an FOL knowledge base with rules may result in direct negative consequences. In
the second, all operators here are defined on all subsets of LitΠ , including inconsistent ones.2
Lemma 2
The operators TKB , UKB , ZKB , and WKB are all monotonic.
1
2

Placed under the context of 2-valued logic, the reasoning here is analogue to parallel circumscription (McCarthy 1980),
where the predicates Employed and Assist are minimized with predicates Certif ied and Disabled varying.
When inconsistency arises, the fixpoint operator here leads to triviality. This is the most common treatment when the
underlying entailment relation is the classical one. However, we remark that this is only one possible choice.

6

Y. Bi. J. You. Z. Feng.

Proof
Let I1 ⊆ I2 ⊆ LitΠ and H ∈ TKB (I1 ). Since any condition in part (i) of Definition 3 that applies
under I1 applies under I2 (including the case where one of them, or both, are inconsistent with
L), thus the set of all consistent extensions of I2 is a subset of all consistent extensions of I1 ,
and therefore we have TKB (I1 ) ⊆ TKB (I2 ). The same argument applies to UKB and ZKB . Since
TKB , UKB , and ZKB are monotonic, it follows from the definition that the operator WKB is also
monotonic.
As WKB is monotone on the complete lattice h2LitΠ , ⊆i, according to the Knaster-Tarski fixpoint theorem (Tarski 1955), its least fixpoint, lfp(WKB ), exists.
Definition 4
Let KB = (L, Π) be an FOL-program. The well-founded semantics of KB (relative to Ω) is
defined by lfp(WKB ).
We allow the well-founded semantics of an FOL-program to be defined by an inconsistent
set, independent of how the semantics may be used. This may be utilized in the computation
of answer sets. Suppose under a suitable definition of answer sets for an FOL-program KB,
lfp(WKB ) approximates all answer sets of KB.3 If the computed lfp(WKB ) is inconsistent then we
know KB has no answer sets.
Example 2
Let KB = ({¬A(a)}, Π) where Π = {A(a) ← not B(a), B(a) ← B(a)}. Let Ω = ΦP =
i+1
0
{A, B} and ΦC = {a}. lfp(WKB ) is constructed as follows (where WKB
= ∅ and WKB
=
i
WKB (WKB ), for all i ≥ 0):
0
WKB
1
WKB
2
WKB
3
WKB
4
WKB

= ∅,
= {¬A(a), ¬B(a)},
= {¬A(a), ¬B(a), A(a)},
= LitΠ ,
3
= WKB
.

As a result, the well-founded semantics of KB is inconsistent. It is interesting to note that KB
has a model, {B(a)}. This means that we cannot determine whether the well-founded semantics
for an FOL-program is consistent or not, based on the existence of a model; when an iterative
process is carried out, we have to deal with the possibility that inconsistencies may arise.
Example 3
Consider KB = (L, Π) where L = {∀xB(x) ⊃ A(x), ¬A(a) ∨ C(a)} and Π consists of
B(a) ← B(a).
A(a) ← (¬C(a) ∧ B(a)).
R(a) ← not C(a), not A(a).
Let ΦP = {A, B, R}, Ω = {A, B}, and ΦC = {a}. Hence HBΠ = {A(a), B(a), R(a)}. For
I0 = ∅, we have TKB (I0 ) = ∅, UKB (I0 ) = {B(a), A(a)}, and ZKB = ∅. B(a) is in UKB (I0 )
because B(a) is not derivable by any rule based on I0 , and L ∪ S|Ω 6|= B(a) for all S ∈ LitcΠ
with I0 ∪ ¬.UKB (I0 ) ⊆ S (condition (b) in Definition 2). Similarly, A(a) is in UKB (I0 ). Since
3

We will show later in this paper that the well-supported answer sets of (Shen and Wang 2011) fall into this category.

Theory and Practice of Logic Programming

7

C(a) is not derivable under all consistent extensions, we derive R(a). Therefore, lfp(WKB ) =
{¬B(a), ¬A(a), R(a)}. Note that since C(a) 6∈ HBΠ its truth value is not part of the wellfounded semantics.
4 Properties and Relations
We first show that the well-founded semantics is a generalization of the well-founded semantics
for normal logic programs.
Theorem 1
Let KB = (∅, Π) be a normal logic program. Then, the WFS of KB coincides with the WFS of
Π.
Proof
The WFS of a normal program Π is defined by the least fixpoint of a monotone operator WΠ on
the set of consistent subsets of HBΠ ∪ ¬.HBΠ :
• TΠ (S) = {head(r) | r ∈ Π, pos(r) ∪ ¬.neg(r) ⊆ S}
• WΠ (S) = TΠ (S) ∪ ¬.UΠ (S)
where UΠ (S) is the greatest unfounded set of Π w.r.t. S. A set U ⊆ HBΠ is an unfounded set of
Π w.r.t. S, if for every a ∈ U and every rule r ∈ Π with head(r) = a, either (i) ¬b ∈ S ∪ ¬.U
for some b ∈ pos(r), or (ii) b ∈ S for some atom b ∈ neg(r).
Then, it is immediate that the notion of unfounded set and the greatest unfounded set for
normal logic program KB = (∅, Π) coincide with those for Π, respectively. Note that ZKB (I) ⊆
UKB (I) when L = ∅. It is easy to see that the operator TKB for normal program KB = (∅, Π)
reduces to TΠ for normal program Π.
The well-supported answer set semantics is defined for what are called normal DL logic programs (Shen and Wang 2011), which applies to FOL-programs. There is however a subtle difference: in the definition of the entailment relation, the WKB operator uses 3-valued evaluation
while the well-supported semantics is based on the notion of 2-valued up to satisfaction.
Definition 5
(Up to satisfaction) Let KB = (L, Π), l a literal, and E and I two interpretations with E ⊆ I ⊆
HBΠ . The relation E up to I satisfies l under L, denoted (E, I) |=L l, is defined as: (E, I) |=L l
if ∀F, E ⊆ F ⊆ I, F |=L l. The definition extends to conjunctions of literals.
The entailment relation, F |=L l, is based 2-valued satisfiability (cf. Def. 1), i.e., F |=L l is
L ∪ F |Ω ∪ ¬.F̄ |Ω |= l, while in 3-valued satisfiability, S |=L l is L ∪ S|Ω |= l.
Given an FOL-program KB = (L, Π), an immediate consequence operator is defined as:
TKB (E, I) = {head(r) | r ∈ Π, (E, I) |=L body(r)}.

(2)

The operator TKB is monotonic on its first argument E with I fixed (Shen and Wang 2011).
α
Thus, for any model I of KB, we can compute a fixpoint, denoted TKB
(∅, I).
Definition 6
Let KB = (L, Π) be an FOL-program and I a model of KB. I is an answer set of KB if for every
α
α
¯ Ω |= A.
A ∈ I, either A ∈ TKB
(∅, I) or L ∪ TKB
(∅, I)|Ω ∪ ¬.I|
The next theorem shows that the well-founded semantics of an FOL-program approximates its
well-supported answer set semantics.

8

Y. Bi. J. You. Z. Feng.

Theorem 2
Let KB = (L, Π) be an FOL-program. Then every well-supported answer set of KB includes all
atoms H ∈ HBΠ that are well-founded and no atoms H ∈ HBΠ that are unfounded or are in
ZKB (lfp(WKB )).
Proof
To prove the assertion, it is sufficient to show that if lfp(WKB ) is consistent, then for every wellsupported answer set I, all atoms in lfp(WKB ) are in I and all negated atoms in lfp(WKB ) are in
¯
¬.I.
We consider the fixpoint construction by the operators TKB (·, I) and WKB . Let us use a short
notation for the respective sequences by
k+1
k
0
TKB
= ∅, . . . , TKB
= TKB (TKB
, I), . . .
0
WKB

=

k+1
∅, . . . , WKB

=

k
W (WKB
), . . .

(3)
(4)

i−1
for all k ≥ 0. Define E0 = ∅ and Ei = {H | (TKB
, I) |=L H} for all i ≥ 1. We show that
i
i
¯
WKB ⊆ Ei ∪ TKB ∪ ¬.I, for all i ≥ 0. The base case is trivial. For the inductive step, assume for
any k ≥ 0 the subset relation holds and we show it holds for k + 1. The proof is conducted on
k+1
k+1
two cases: (I) Assume an atom H ∈ WKB
and show H ∈ Ek+1 ∪ TKB
, and (II) Assume a
k+1
¯
negated atom ¬H ∈ WKB and show ¬H ∈ ¬.I.
i
By definition and monotonicity of the operator TKB , (TKB
, I) |=L Ei , and it follows from the
first-order entailment that for any atom H ∈ HBΠ ,
i
i
(TKB
, I) |=L H iff (Ei ∪ TKB
, I) |=L H.

(5)

By definition,
k+1
k
k
k
WKB
= TKB (WKB
) ∪ ¬.UKB (WKB
) ∪ ¬.ZKB (WKB
)

By Proposition 1 of (Shen 2011), for any FOL-formula H,
¯ Ω |= H.
(E, I) |=L H iff L ∪ E|Ω ∪ ¬.I|

(6)

By Proposition 2 (Shen 2011), for any ordinary atom H,
(E, I) |=L H iff H ∈ E; (E, I) |=L not H iff H 6∈ I.

(7)

k+1
k
(I) For any atom H ∈ WKB
, we have H ∈ TKB (WKB
). If condition (i.b) in Definition 3 holds,
k
k
¯ Ω |= H. Then by (6)
we have L ∪WKB |Ω |= H. By induction hypothesis, L ∪(Ek ∪TKB
)|Ω ∪¬.I|
k
and (5), (TKB , I) |=L H. Thus H ∈ Ek+1 . If condition (i.a) in Definition 3 holds, we consider
the following four cases:

1.
2.
3.
4.

k
k
For any ordinary atom A ∈ pos(r), A ∈ WKB
, thus (TKB
, I) |=L A by (7) and (5).
k
k
For any ordinary atom A ∈ neg(r), ¬A ∈ WKB , thus (TKB
, I) |=L not A.
k
k
, I) |=L A.
For any FOL-formula A ∈ pos(r), L ∪ WKB |Ω |= A, then (TKB
k ′
k ′
k
For any FOL-formula A ∈ neg(r), L ∪ (WKB ) |Ω 6|= A for every (WKB
) such that WKB
⊆
k
k ′
c
(WKB ) ∈ LitΠ , we have (TKB , I) 6|=L A, since every total interpretation is a partial one.
k+1
.
Hence H ∈ TKB
k+1
k
k
(II) For any negated atom ¬H ∈ WKB
, either H ∈ UKB (WKB
) or H ∈ ZKB (WKB
). For the
k
k
case H ∈ UKB (WKB ), if condition (b) in Definition 2 holds, we have (TKB , I) 6|=L H by (5),
(6) and induction hypothesis, in addition to the fact that every total interpretation is a partial one.
Then H 6∈ Ek+1 . For condition (a) in Definition 2, we also consider the following four situations:

Theory and Practice of Logic Programming

9

k
k
1. For any ordinary atom A ∈ pos(r), ¬A ∈ WKB
∪ ¬.U , thus (TKB
, I) 6|=L A, by a similar
argument above.
k
k
2. For any ordinary atom A ∈ neg(r), A ∈ WKB
, thus (TKB
, I) |=L A.
k ′
k
k ′
3. For any FOL-formula A ∈ pos(r), L ∪ (WKB ) |Ω 6|= A, for every WKB
⊆ (WKB
) ∈ LitcΠ , then
k
(TKB
, I) 6|=L A, since every total interpretation is a partial one.
k
k
4. For any FOL-formula A ∈ neg(r), L ∪ WKB
|Ω |= A, we have (TKB
, I) |=L A.
k+1
k+1
We have H 6∈ TKB
. Hence H 6∈ Ek+1 ∪ TKB
k
¯ since the operator E and TKB only generate positive atoms.
For any ¬H ∈ WKB , ¬H ∈ ¬.I,
k
α
We then have H 6∈ Ek ∪ TKB . As k is arbitrary, we have H ∈ UKB (lfp(WKB )) and H 6∈ Eα ∪ TKB
,
α
α
where Eα and TKB are the respective fixpoints. Since Eα ∪ TKB = I (By definition 6), we
¯ Similarly, if H ∈ ZKB (W k ), then H ∈ I.
¯ We thus have proved that W k+1 ⊆
get H ∈ I.
KB
KB
k+1
¯
Ek+1 ∪ T
∪ ¬.I.
KB

5 Related Work
The most relevant work in defining well-founded semantics for combing rules with DLs are
(Eiter et al. 2011; Lukasiewicz 2010). The former embeds dl-atoms in rule bodies to serve as
queries to the underlying ontology, and it does not allow the predicate in a rule head to be shared
in the ontology. In both approaches, syntactic restrictions are posted so that the least fixpoint is
always constructed over sets of consistent literals. It is also a unique feature in our approach that
combined reasoning with closed world and open world is supported.
A program in FO(ID) has a clear knowledge representation “task” - the rule component is used
to define concepts, whereas the FO component may assert additional properties of the defined
concepts. All formulas in FO(ID) are interpreted under closed world assumption. Thus, FOLprograms and FO(ID) have fundamental differences in basic ideas. On semantics, FOL-formulas
can be interpreted under open world and closed world flexibly. On modeling, the rule set in
FO(ID) is built on ontologies, thus information can only flow from a first order theory to rules.
But in FOL-programs, the first order theory and rules are tightly integrated, and thus information
can flow from each other bilaterally.

6 Conclusion and Future Directions
In this paper we have defined a new well-founded semantics for FOL-programs, where arbitrary
FOL-formulas are allowed to appear in rule bodies and an atom with its predicate shared with
first-order theory to appear in a rule head. Combined reasoning with closed world as well as
open world is supported. Moreover, inconsistencies are dealt with explicitly, and thus the task of
computing answer sets can be prejudged in case that the well-founded semantics is an inconsistent set. We have shown that the well-founded semantics is an appropriate approximation of the
well-supported answer set semantics defined in (Shen and Wang 2011).
As future work, we will study the approximation fixpoint theory (AFT) (Denecker et al. 2000;
Denecker et al. 2004), and investigate whether and how well-founded and stable semantics of
FOL-programs can be defined uniformly under an extended approximation fixpoint theory. We
are also interested in possible different approximating operators for alternative semantics of
FOL-programs. In (Denecker et al. 2004) the authors show that the theory of consistent approximations can be applied to the entire bilattice L2 (including inconsistent elements), under the

10

Y. Bi. J. You. Z. Feng.

assumption that an approximating operator A is symmetric. This symmetry assumption guarantees that no transition from a consistent state to an inconsistent one may take place. As argued at
the outset of this paper, this is precisely what we cannot assume for a definition of well-founded
semantics for all FOL-programs.
Acknowledgements
This work is supported by the National Natural Science Foundation of China (NSFC) grants
61373035 and 61373165, and by National High-tech R&D Program of China (863 Program)
grant 2013AA013204.
References
B RUIJN , J., E ITER , T., AND T OMPITS , H. 2008. Embedding approaches to combining rules and
ontologies into autoepistemic logic. In Proc. KR 2008. 485–495.
DE B RUIJN , J., P EARCE , D., P OLLERES , A., AND VALVERDE , A. 2007. Quantified equilibrium logic and
hybrid rules. In Proc. RR 2007. 58–72.
D ENECKER , M., M AREK , V., AND T RUSZCZY ŃSKI , M. 2000. Approximations, stable operators, wellfounded fixpoints and applications in nonmonotonic reasoning. In Logic-based Artificial Intelligence.
127–144.
D ENECKER , M., M AREK , V., AND T RUSZCZYNSKI , M. 2004. Ultimate approximation and its application
in nonmonotonic knowledge representation systems. Information and Computation 192, 1, 84–121.
E ITER , T., I ANNI , G., L UKASIEWICZ , T., S CHINDLAUER , R., AND T OMPITS , H. 2008. Combining
answer set programming with description logics for the semantic web. Artifical Intelligence 172, 12-13,
1495–1539.
E ITER , T., L UKASIEWICZ , T., I ANNI , G., AND S CHINDLAUER , R. 2011. Well-founded semantics for
description logic programs in the semantic web. ACM Transactions on Computational Logic 12, 2.
Article 3.
L UKASIEWICZ , T. 2010. A novel combination of answer set programming with description logics for the
semantic web. IEEE TKDE 22, 11, 1577–1592.
M C C ARTHY, J. 1980. Circumscription - a form of non-monotonic reasoning. Artifical Intelligence 13, 2739, 171–172.
M OTIK , B. AND ROSATI , R. 2010. Reconciling description logics and rules. Journal of the ACM 57, 5,
1–62.
ROSATI , R. 2005. On the decidability and complexity of integrating ontologies and rules. Journal of Web
Semantics 3, 1, 61–73.
ROSATI , R. 2006. DL+log: Tight integration of description logics and disjunctive datalog. In Proc. KR’06.
68–78.
S HEN , Y.-D. 2011. Well-supported semantics for description logic programs. In Proc. IJCAI-11. 1081–
1086.
S HEN , Y.-D. AND WANG , K. 2011. Extending logic programs with description logic expressions for the
semantic web. In Proc. International Semantic Web Conference. 633–648.
TARSKI , A. 1955. A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics 5:2, 285–309.
YANG , Q., YOU , J.-H., AND F ENG , Z. 2011. Integrating rules and description logics by circumscription.
In Proc. AAAI-11.

DE

