MKNF-based Hybrid Knowledge Bases (HKBs) integrate Logic Programming (LP) and Description Logics (DLs) o ering the combined expressiveness of the two formalisms. In particular, HKB allow to make di erent closure assumptions for di erent predicates. HKBs have been given a well-founded semantics in terms of an alternate xpoint. In this paper we provide an alternative de nition of the semantics using an iterated xpoint. In this way the computation of the well-founded model proceeds uniformly bottom-up, making the semantics easier to understand, to reason with and to automate. We also present slightly di erent but equivalent versions of our de nition. We then discuss the relationships of HKBs with other formalisms. The results show that overall HKBs seem to be those that more tightly integrate LP and DL, even if there exist incomparable languages such as the recent FO(ID) formalism.
Logic Programming (LP) languages and Description Logic (DL) languages are successful tools for modeling complex domains. They are both based on rst order logic but di er for the domain closure assumption: LP makes the closedworld assumption while DLs make the open-world assumption.
In some domains, such as in legal reasoning [
Among the several integration approaches proposed in the last decades, one
of the most e ective is Hybrid Knowledge Bases (HKBs) [
Recently, HKBs have been given a well-founded semantics (WFS) [
The WFS for logic programs was given in [
The WFS for HKBs of [
We also discuss the relationships between HKBs and other formalisms for
combining DL and LP, concentrating on FO(ID) [
The paper is structured as follows: in Section 2 we provide some background notions. In Section 3 we introduce our iterated xpoint de nition of the semantics of HKB. Section 4 presents alternative but equivalent formulations. Section 5 discusses related work and Section 6 concludes the paper. 2
This section is devoted to introducing the background notions. We rst discuss
xpoints and LP in Sections 2.1 and 2.2 following [
A relation on a set S is a partial order if it is re exive, antisymmetric and transitive. In the following, let S be a set with a partial order . a 2 S is an upper bound of a subset X of S if x a for all x 2 X. Similarly, b 2 S is a lower bound of X if b x for all x 2 X.
An element a 2 S is the least upper bound of a subset X of S if a is an upper bound of X and, for all upper bounds a0 of X, we have a a0. Similarly, b 2 S is the greatest lower bound of a subset X of S if b is a lower bound of X and, for all lower bounds b0 of X, we have b0 b. The least upper bound of X is unique, if it exists, and is denoted by lub(X). Similarly, the greatest lower bound of X is unique, if it exists, and is denoted by glb(X).
A partially ordered set L is a complete lattice if lub(X) and glb(X) exist for every subset X of L. We let > denote the top element lub(L) and ? denote the bottom element glb(L) of the complete lattice L.
Let L be a complete lattice and T : L ! L be a mapping. We say T is monotonic if T (x) T (y), whenever x y. We say that a 2 L is a xpoint of T if T (a) = a. We say that a 2 L is the least xpoint of T if a is a xpoint and, for all xpoints b of T , we have a b. Similarly, we de ne greatest xpoint.
Let L be a complete lattice and T : L ! L be monotonic. Then we de ne T " 0 = ?; T " = T (T " ( 1)), if is a successor ordinal; T " = lub(fT " j < g), if is a limit ordinal; T # 0 = >; T # = T (T # ( 1)), if is a successor ordinal; T # = glb(fT # j < g), if is a limit ordinal.
T has a least xpoint lfp(T ) and a greatest xpoint gfp(T ). 2.2
A normal program P is a set of normal rules. A normal rule has the form r = h b1; : : : ; bn; :c1; : : : ; :cm (1) where h; b1; : : : ; bn; c1; : : : ; cm are atoms.
The set of ground atoms that can be built with the symbols of a program P is called the Herbrand base and is denoted as BP .
A two-valued interpretation I is a subset of BP . I is the set of true atoms, so a is true in I if a 2 I and is false if a 62 I. The set Int2 of two-valued interpretations for a program P forms a complete lattice where the partial order is given by the subset relation . The least upper bound and greatest lower bound are de ned as lub(X) = SI2X I and glb(X) = TI2X I. The bottom and top element are respectively ; and BP .
A three-valued interpretation I is a pair hIT ; IF i where IT and IF are subsets of BP and represent respectively the set of true and false atoms. So a is true in I if a 2 IT and is false in I if a 2 IF . A consistent three-valued interpretation I = hIT ; IF i is such that IT \ IF = ;. The union of two three-valued interpretations hIT ; IF i and hJT ; JF i is de ned as hIT ; IF i [ hJT ; JF i = hIT [ JT ; IF [ JF i. The intersection of two three-valued interpretations hIT ; IF i and hJT ; JF i is de ned as hIT ; IF i \ hJT ; JF i = hIT \ JT ; IF \ JF i. The set Int3 of three-valued interpretations for a program P forms a complete lattice where the partial order is de ned as hIT ; IF i hJT ; JF i if IT JT and IF JF . The least upper bound and greatest lower bound are de ned as lub(X) = SI2X I and glb(X) = TI2X I. The bottom and top element are respectively h;; ;i and hBP ; BP i.
The WFS assigns a three-valued model to a program, i.e., it identi es a
consistent three-valued interpretation as the meaning of the program. The WFS
was given in [
De nition 1. For a normal program P , sets Tr and Fa of ground atoms, and a 3-valued interpretation I we de ne the operators OpT rueIP : Int2 ! Int2 and OpFalseIP : Int2 ! Int2 as OpT rueIP (Tr ) = faja is not true in I; and there is a clause b l1; :::; ln in P , a grounding substitution such that a = b and for every 1 i n either li is true in I, or li 2 Tr g; OpFalseIP (Fa) = faja is not false in I; and for every clause b l1; :::; ln in P and grounding substitution such that a = b there is some i (1 i n) such that li is false in I or li 2 Fag.
In words, the operator OpT rueIP (Tr ) extends the interpretation I to add the
new true atoms that can be derived from P knowing I and true atoms Tr , while
OpFalseIP (Fa) computes new false atoms in P by knowing I and false atoms
Fa. OpT rueIP and OpFalseIP are both monotonic [
Description Logics (DLs) are a fragment of First Order Logic (FOL) used to
model ontologies [
Let us consider a set C of atomic concepts, a set R of atomic roles and a set I of individuals. A concept C is de ned by the syntax rule:
C ::=C1j?j>j(C u C)j(C t C)j:Cj9R:Cj8R:C where C1 2 C, R 2 R.
D are concepts. An ABox A is a nite set of concept membership axioms a : C and role membership axioms (a; b) : R, where C 2 C, R 2 R and a; b 2 I.
A ALC KB K = (T ; A) consists of a TBox T and an ABox A. It is usually assigned a semantics in terms of interpretations I = ( I ; I ), where I is a non-empty domain and I is the interpretation function. This function assigns an element in I to each a 2 I, a subset of I to each C 2 C and a subset of I I to each R 2 R.
DLs can be translated into FOL by de ning a function , which maps axioms to rst order formulas. 2.4
The logic of MKNF was introduced in [
The original MKNF semantics is two-valued; we now recap the three-valued
semantics for MKNF formulas proposed in [
A three-valued MKNF structure (I,M,N ) consists of a rst-order interpretation I and two pairs M = (M; M1) and N = (N; N1) of sets of rst-order interpretations where M1 M and N1 N . Satisfaction of a closed formula by a three-valued MKNF structure is de ned as follows (where p is an atom and is a formula and the values true, unde ned and false follow the order false < unde ned < true): An MKNF interpretation pair (M; N ) consists of two MKNF interpretations M , N with ; N M . An MKNF interpretation pair satis es a closed MKNF formula i (I; (M; N ); (M; N ))( ) = true for each I 2 M . If M = N , then the MKNF interpretation pair (M; N ) is called total. If there exists an MKNF interpretation pair satisfying , then is consistent. An MKNF interpretation pair (M; N ) is a three-valued MKNF model for a given closed MKNF formula if { (M; N ) satis es , and { for each MKNF interpretation pair (M 0; N 0) with M M 0 and N N 0, where at least one of the inclusions is proper and M 0 = N 0 if M = N , there is an I0 2 M 0 such that (I0; (M 0; N 0); (M; N ))( ) 6= true.
An MKNF HKB [
Given a HKB K = hO; Pi, an atom in P is a DL-atom if its predicate occurs in O, a non-DL-atom otherwise. An LP rule is DL-safe if each of its variables occurs in at least one positive non-DL-atom in the body; a HKB is DL-safe if all its LP-rules are DL-safe.
In the following, we recall the well-founded semantics for hybrid MKNF KBs
presented in [
Let K = hO; Pi be a ground HKB. The set of known atoms of K, KA(K), is the smallest set that contains all positive literals occurring in P, and a positive literal for each literal occurring in P. Given S KA(K), the objective knowledge of K with respect to S is the set OBK;S = f (O)g [ S. The operators RK, DK and TK derive atoms that are consequences of a positive HKB K and a set S of atoms. RK(S) is the set of consequences due to rules, i.e., the heads of rules in P whose bodies are composed of atoms that are a subset of S; DK(S) is the set of consequences due to axioms, i.e., the atoms from KA(K) entailed by OBK;S ; and TK(S) = RK(S) [ DK(S). Given a HKB K and a set of atoms S KA(K), the following transformations, yielding positive knowledge bases, are de ned: the MKNF transformation K=S is hO; P=Si where P=S is the set of rules h a1; : : : ; am such that there exists in P a rule a a1; : : : ; am; b1; : : : ; bn with fb1; : : : ; bng \ S = ;, and the MKNF-coherent transformation K==S is hO; P==Si where P==S is the set of rules h a1; : : : ; am such that there exists in P a rule h a1; : : : ; am; b1; : : : ; bn with fb1; : : : ; bmg \ S = ; and OBK;S 6j= :h.
The KBs transformations induce transformations of sets of positive atoms, respectively: K(S) = lfp(TK=S) and K0(S) = lfp(TK==S). Using these transformations, the sequences of positive atoms P and N are de ned as follows: P0 = ;, N0 = KA(K), Pn+1 = K(Nn) and Nn+1 = K0(Pn), P! = S Pi, N! = T Ni. P! contains everything that is necessarily true, while N! contains everything that is not false. A KB K is MKNF-inconsistent i O is inconsistent or K0(P!) K(P!) or K0(N!) K(N!).
The well-founded model of a MKNF-consistent K is MW F = P! [ (O) [ f
which establishes a property of all the MKNF models of the HKB: if a 2 P!, then K a is true in all three-valued models (so, a is true in all the interpretations that compose each model), while if a 2 N! then not a is true in all three-valued models (a is false in at least one of the interpretations that compose each model).
Example 1 shows the WFM of a simple HKB, according to the semantics recalled above and to the one presented in this paper.
In this section, we give the WFS for HKB in a bottom-up way, as in [
interpretation I = hIT ; IF i we de ne the operators OpT rueIK : Int2 ! Int2 and OpFalseIK : Int2 ! Int2 as OpT rueIK(Tr ) = faja is not true in I; and there is a clause a a1; :::; an; b1; : : : ; br in the grounding of P and for every 1 i n either ai is true in I or ai 2 Tr and for every 1 j r bj is false in Ig [ fa 2 KA(K)jOBK;IT [T r j= ag; OpFalseIK(Fa) = f j
a a is not false in I; and either OBK;IT j= :a, or for every clause a a1; :::; an; b1; : : : ; br in the grounding of P there is some i (1 i n) such that ai is false in I or ai 2 Fa, or there is some j (1 i r) such that bj is true in I g \ fa 2 KA(K)jOBK;KA(K)n(IF [Fa) 6j= ag In words, the operator OpT rueIK(Tr ) extends the interpretation I to add the new true atoms that can be derived from K knowing I and true atoms Tr , while OpFalseIK(Fa) computes new false atoms in P by knowing I and false atoms Fa. Theorem 1. OpT rueIK and OpFalseIK are both monotonic.
Proof. Proving monotonicity of OpT rueIK is the same of proving that if Tr Tr 0, then OpT rueIK(Tr ) OpT rueIK(Tr 0). Analogously, monotonicity of OpFalseIK means that if Fa Fa0, then OpF alseIK(Fa) OpFalseIK(Fa0).
Regarding OpT rueIK, if a 2 OpTrueK(Tr ), De nition 3 ensures that either I there is a clause a l1; :::; ln in P 's grounding and for every 1 i n either li is true in I, or li 2 Tr , or OBK;T r j= a, i.e., (O) [ T r j= a. Since Tr Tr 0, if li 2 Tr , then also li 2 Tr 0, and if (O) [ T r j= a, then also (O) [ T r0 j= a for the monotonicity of rst order logic. So a 2 OpTrueIK(Tr 0).
Regarding OpFalseIK, if a 2 OpFalseIK(Fa), then either { OBK;KA(K)nIF j= :a, or { for every clause a l1; :::; ln in P 's grounding there is some i (1 such that either li is a literal false in I, or li 2 Fa, and since Fa li 2 Fa0. i
n) Fa0, Also, OBK;KA(K)n(IF [Fa) 6j= a, so OBK;KA(K)n(IF [Fa0) 6j= a by the monotonicity of rst order logic. So a 2 OpFalseIK(Fa0).
Since OpT rueIK and OpFalseIK are monotonic, they both have least and greatest xpoints. An iterated xpoint operator builds up dynamic strata by constructing successive three-valued interpretations as follows.
Int3 ! Int3 be de ned as IFP K(I) = I [ hlfp(OpT rueIK); gfp(OpFalseIK)i. Theorem 2. IFP K is monotonic.
Proof. Let I = hIT ; IF i, I0 = hIT0 ; IF0 i, IT IT0 and IF IF0 . We now have to show that IT [ lfp(OpTrueIK) IT0 [ lfp(OpT rueIK0 ). We can do this by proving that OpTrueIK " n IT0 [ OpTrueIK0 " n for all n. For n = 0 OpTrueIK " 0 IT0 [ OpTrueIK0 " 0 because OpTrueIK " 0 = ;. Now, suppose it holds for some n and let a 2 OpTrueIK " (n + 1), then there is a clause a l1; :::; lm in P 's grounding such that for every 1 i m either li is true in I, or li 2 OpTrueIK " n, or OBK;OpTrueIK"n j= a. If li is true in I, it is also true in I0, if li 2 OpTrueIK " n then either li 2 OpTrueIK0 " n or l 2 IT0 , and if OBK;OpTrueIK"n j= a, it also holds that OBK;IT0 [OpTrueIK0 "n j= a, thanks to the monotonicity of rst order logic. Therefore, a 2 IT0 [ OpTrueIK0 " (n + 1).
We now have to show that IF [ gfp(OpFalseIK) IF0 [ gfp(OpF alseIK0 ). We prove that OpFalseIK # n OpFalseIK0 # n for all n. For n = 0 OpFalseIK # 0 = KA(K) = OpFalseIK0 # 0. Suppose it also holds for some n and let a 2 OpFalseIK # (n + 1); then either OBK;IT j= :a (and also OBK;IT0 j= :a, because IT IT0 and rst order logic is monotonic), or for every clause a l1; :::; ln in P 's grounding there is some i (1 i n) such that li is false in I, or li 2 OpFalseIK # n, or OBK;KA(K)nOpFalseIK#n 6j= a. If li is false in I, it is also false in I0, if li 2 OpFalseIK # n then either li 2 OpFalseIK0 # n or l 2 IF0 , and if OBK;KA(K)nOpFalseIK#n 6j= a, it also holds that OBK;KA(K)nOpFalseIK0 #n 6j= a for the inductive hypothesis and the monotonicity of rst order logic. Therefore, a 2 OpFalseIK0 # (n + 1).
So IFP K has a least xed point lfp(IFP K). The main result of the paper is the following theorem that our de nition of the well-founded model is equivalent to that of Section 2.4.
For m = 0 TK=KA(K)nIF " 0 = ; so TK=KA(K)nIF " 0 IT [ OpTrueIK " 0. For Proof. We prove this by double induction. We show by induction that IFP K " n = hPn; KA(K) n Nni. For n = 0, IFP K " 0 = h;; ;i, while P0 = ; and N0 = KA(K), thus hP0; KA(K) n N0i = h;; ;i = IFP K " 0.
For n + 1, let IFP K " n = hPn; KA(K) n Nni = I = hIT ; IF i.
We now prove that (1) IT [ lfp(OpTrueIK) = lfp(TK=KA(K)nIF ) and that (2) KA(K) n IF [ gfp(OpFalseIK) = lfp(TK==IT ).
To prove (1), we rst show by induction that TK=KA(K)nIF " m OpTrueIK " m.
IT [ m + 1, let T r be OpTrueIK " m = TK=KA(K)nIF " m.
If a 2 TK=KA(K)nIF (T r), suppose a 2 RK=KA(K)nIF (T r). Then there is a rule a l1; :::; ln in P=KA(K) n IF with each li a positive literal belonging to IT or T r. This means that the grounding of P contains a rule a l1; :::; ln; b1; : : : ; br with b1; : : : ; br in IF . So a 2 OpTrueIK " m + 1 for the de nition of OpTrueIK. If a 2 DK=KA(K)nIF (T r) then OBK;T r j= a so a 2 OpTrueIK(T r) for the de nition of OpTrueIK.
Since TK=KA(K)nIF " m IT [ OpTrueIK " m, for all m, lfp(TK=KA(K)nIF ) IT [lfp(OpTrueK), so to prove (1) it is su cient to show that IT [lfp(OpTrueK)
I I lfp(TK=KA(K)nIF ). Note that IT lfp(TK=KA(K)nIF ) because IT = Pn, Pn is the least xpoint of a TK0 operator where K0 is a subset of K=KA(K) n IF and positive programs are monotonic.
If a 2 lfp(OpTrueIK), suppose a 62 lfp(TK=KA(K)nIF ). Then for each rule a a1; :::; an; b1; : : : ; br in the grounding of P there exits an ai that is not in lfp(TK=KA(K)nIF ) or a bj 62 IF , and OBK;lfp(TK=KA(K)nIF ) 6j= a. Since lfp(TK=KA(K)nIF ) IT [ lfp(OpTrueIK) and IT lfp(TK=KA(K)nIF ), then ai 62 lfp(OpTrueK) or bj 62 IF . In both cases a 62 lfp(OpTrueIK) against the hypothe
I sis. So we have IT [ lfp(OpTrueIK) = lfp(TK=KA(K)nIF ).
We prove (2) by proving that, for all m, TK==IT " m = KA(K) n (IF [ OpFalseIK # m).
For m = 0 TK==IT " 0 = ; and OpFalseIK # 0 = KA(K), so TK==IT " 0 = KA(K) n (IF [ OpFalseIK # 0). For m + 1, let S be TK==IT " m and let Fa be OpFalseIK # m; by the inductive hypothesis, S = KA(K)n(IF [Fa). We now show that, for all a 2 KA(K), a 2 TK==IT (S) if and only if a 62 (IF [ OpFalseIK(Fa)). If a 2 TK==IT (S), then a 62 IF , because otherwise a 2 Nn+1 and, since Nn+1 Nn, a 2 Nn, but by the external inductive hypotheses IF and Nn are disjoint. So we need to prove a 62 OpFalseIK(Fa). As just proved, a 62 IF ; if OBK;S j= a, this means that OBK;KA(K)n(IF [Fa) j= a, so a 62 OpFalseK(Fa); otherwise I OBK;IT 6j= :a and there exists a rule a a1; : : : ; am; b1; : : : ; bn in P's grounding such that OBK;IT 6j= :a, fa1; : : : ; amg S and fb1; : : : ; bng \ IT = ;, which, by De Morgan's laws and because S = KA(K) n (IF [ Fa), is the negation of the fact that OBK;IT j= :a or, for each rule a a1; : : : ; am; b1; : : : ; bn in P's grounding, fa1; : : : ; amg [ (IF \ Fa) 6= ; or fb1; : : : ; bng \ IT 6= ;; so again a 62 OpFalseK(Fa). On the other hand, if a 62 IF [ OpFalseK(Fa), then a 62
I I OpFalseIK(Fa), so either (i) OBK;KA(K)n(IF [Fa) j= a (and, since KA(K) n (IF [ Fa) = S, OBK;S j= a, so a 2 TK==IT (S)), or (ii) OBK;IT 6j= :a and there exists a rule a a1; : : : ; am; b1; : : : ; bn in P's grounding such that fa1; : : : ; amg [ (IF \ Fa) = ; (i.e., fa1; : : : ; amg S) and fb1; : : : ; bng \ IT = ;, so again a 2 TK==IT (S).
Let be the smallest ordinal such that WFM (P ) = IFP K " . We refer to as the depth of K. The stratum of atom a is the least ordinal such that a 2 IFP K " (where a may be either in the true or false component of IFP K " ). Unde ned atoms of the well-founded model do not belong to any stratum { i.e. they are not added to IFP K " for any ordinal .
Ig \ fa 2 KA(K)jOBK;KA(K)n(IF [Fa) 6j= ag De nition 5. De ne OpTrue0K : Int2 ! Int2 and OpFalse0K : Int2 ! Int2 as
I I OpT rue0IK(Tr ) = fajthere is a clause a a1; :::; an; b1; : : : ; br in the grounding of P and for every 1 i n either ai is true in I or ai 2 Tr and for every 1 j r bj is false in Ig [ fa 2 KA(K)jOBK;IT [T r j= ag; OpFalse0IK(Fa) = fajeither OBK;IT j= :a or for every clause a a1; :::; an; b1; : : : ; br in the grounding of P there is some i (1 i n) such that ai is false in I or ai 2 Fa, or there is some j (1 i r) such that bj is true in Let IFP 0K : Int3 ! Int3 be IFP 0K(I) = hlfp(OpT rue0IK); gfp(OpFalse0IK)i. IFP 0K di ers from De nition 3 because OpT rue0IK and OpFalse0IK do not check whether the atoms are already true or false in I. As a consequence, in each iteration of IFP 0K the set of true and false atoms is rebuilt and includes I. Therefore, we do not need to add I to hlfp(OpT rue0IK); gfp(OpFalse0IK)i. It is possible to prove the equivalence of IFP 0K with De nition 3.
It is even possible to check the truth of positive literals in OpT rueIK and the falsity of positive literals in OpFalseIK only with respect to the set of atoms that is changing in the inner xpoint, without referring to interpretation I, obtaining the following de nition that can be proved to lead to the same semantics for HKBs.
De nition 6. De ne OpTrue00IK : Int2 ! Int2 and OpFalse00IK : Int2 ! Int2 as OpT rue0I0K(Tr ) = fajthere is a clause a a1; :::; an; b1; : : : ; br in the grounding of P and for every 1 i n ai 2 Tr and for every 1 j r bj is false in Ig [ fa 2 KA(K)jOBK;IT [T r j= ag;
KA(K)jOBK;KA(K)n(IF [Fa) 6j= ag OpFalse00IK(Fa) = fajeither OBK;IT j= :a or for every clause a a1; :::; an; b1; : : : ; br in the grounding of P there is some i (1 i n) such that ai 2 Fa, or there is some j (1 i r) such that bj is true in Ig \ fa 2 Let IFP 00K : Int3 ! Int3 be IFP 00K(I) = hlfp(OpT rue0I0K); gfp(OpFalse00IK)i. In this case it is possible to prove that TK=KA(K)nIF " m = OpTrue00IK " m and KA(K) n gfp(OpFalse00K) = lfp(TK==IT ), obtaining operators that are closer to
I
those of Knorr et al. [
In [
Along this line, an extension of DL with rules is FO(ID) [
While the FO(ID) language bears an obvious similarity with MKNF-based HKBs, in that both combine rst-order formulas and rules, in order to compare their semantics one must rst observe that FO(ID) models are two-valued interpretations, while MKNF models are sets of interpretations, so a comparison directly involving the MKNF semantics is not possible. However, one may try to establish a connection between the two semantics by giving a di erent understanding of an HKB K = hO; Pi's well-founded partition: the two-valued interpretation built by adding to the positive atoms in the well-founded partition some of the DL-atoms is a model (let us call it, for the present discussion, an HKB model) if it entails, in the classical logic sense, the HKB. The question is then whether the models so de ned are the same as the FO(ID) models of the FO(ID) KB obtained from K by adding to O one de nition composed of all the clauses in P. In general, this is not the case. For instance, consider K = h;; fp(a) q(a)gi: the only model is ;, while fp(a); q(a)g is a FO(ID) model, so there is a FO(ID) model that is not a HKB model. The opposite can also occur: for K = hfp v qg; fp(a); p(a) q(a)gi has the HKB model fp(a); q(a)g which is not a FO(ID) model. In conclusion, there is no obvious mapping between HKBs and FO(ID) KBs.
Another similar approach is represented by SWRL [
Other proposals combines DLs with Answer Set Programming [
We think that HKBs provide a powerful tool for modeling real world domains, allowing the use of the closed world and open world assumptions for di erent predicates in the same theory. When compared with other approaches for combining LP and DL, they have several advantages, the most important of which is the tighter integration of the two components. As such, it is important to study HKBs and develop in-depth analysis of their semantics. In this paper we provide an alternative formulation of the well-founded semantics of HKBs that is based on iterating xpoints in a fully bottom-up way. In this way we aim at presenting a new viewpoint for the semantics that can highlight new relationships with other formalisms together with proposing an approach for computing the semantics that is possibly easier to implement.