Embedding Non-Ground Logic Programs into Autoepistemic Logic for Knowledge-Base Combination

1 Introduction

In the context of the ongoing discussion around combinations of rules and ontologies for the Semantic Web, there have been several proposals for integrating classical knowledge bases (ontologies) and rule bases (logic programs). Generally speaking, all these approaches try to define a reasonable semantics for a combined knowledge base consisting of a classical component and a rules component.

Two trends are currently observable. On the one hand, approaches such as SWRL [Horrocks and Patel-Schneider, 2004] extend the ontology with Horn formulas in a classical framework. This approach is straightforward, but prohibits nonmonotonic rules. On the other hand, existing approaches which do allow nonmonotonic rules either (a) distinguish between "classical" and "rules" predicates and limit the domain of interpretation (e.g., [Rosati, 2006]) or (b) restrict the interaction to ground entailment (e.g., [Eiter et al., 2004]). The main distinction between these approaches is the type of interaction between the classical knowledge base on the one hand and the rule base on the other (cf. de Bruijn et al. [2006] for an examination of this issue).

∗This work was funded by the European Commission projects KnowledgeWeb (IST 507482), DIP (IST 507483), and REWERSE (IST 506779), by the Austrian Science Fund (FWF) project P17212N04, and by the CICyT of Spain project TIC-2003-9001.

As for combination, a classical theory and a logic program should be viewed as complementary descriptions of the same domain. Therefore, a syntactic separation between predicates defined in these two components should not be enforced. Furthermore, it is desirable to neither restrict the interaction between the classical and the rules components nor impose any syntactic or semantic restrictions on the individual components. That is, the classical component may be an arbitrary theory Φ of some first-order language with equality, and the rules component may be an arbitrary non-ground normal or disjunctive logic programP, interpreted using, e.g., the common stable-model semantics [Gelfond and Lifschitz, 1988].

The goal is a combined theory, ι(Φ, P), in a uniform logical formalism. Naturally, this theory should amount to Φ if P is empty, and to P if Φ is empty. Therefore, such a combination must provide faithful embeddings σ(Φ) and τ(P) of Φ and P, respectively, in this formalism, given by σ(Φ) = ι(Φ, ∅) and τ(P) = ι(∅, P), respectively. In turn, knowledge combination may be carried out on top of such embeddings σ(·) and τ (·), where in the simplest case one may choose ι(Φ, P ) = σ(Φ) ∪ τ (P ).

This raises the questions (a) which uniform formalism is suitable and (b) which embeddings are suitable and, furthermore, how do embeddings relate to each other and how do they behave under knowledge combination?

Autoepistemic logic (AEL) [Moore, 1985], which extends classical logic with a modal belief operator, is an attractive candidate for a uniform formalism. In fact, embedding a classical theory in AEL is trivial, and several embeddings of logic programs in AEL have been described [Gelfond and Lifschitz, 1988; Marek and Truszczy´nski, 1993; Lifschitz and Schwarz, 1993; Chen, 1993; Przymusinski, 1991]. However, all these embeddings have been developed for the propositional case only, whereas we need to deal with nonground theories and programs. This requires us to consider first-order autoepistemic logic (FO-AEL) [Konolige, 1991; Kaminski and Rey, 2002; Levesque and Lakemeyer, 2000], and non-ground versions of these embeddings. Our main contributions are as follows.

We define several embeddings of non-ground logic programs into FO-AEL, taking into account subtle issues of quantification in FO-AEL. We show that these embeddings are faithful in the sense that the stable models of the program and the sets of objective ground atoms in the stable expansions of the embeddings are in a one-to-one correspondence. However, the embeddings behave differently on formulas beyond ground atoms, and when combined with classical theories, even when considering propositional formulas.

Motivated by these differences, we compare the embeddings along two dimensions:

1. We determine correspondences between the stable expansions of different possible embeddings, with respect to various classes of formulas. This is done for the embeddings themselves, as well as for combinations with theories from different fragments of classical logic which are important in ontology representation.
2. We present inclusion relations between the sets of autoepistemic consequences of the embeddings.

Compared to other well-known nonmonotonic formalisms like Reiter's default logic, FO-AEL offers a uniform language in which (nonmonotonic) rules themselves can be expressed at the object level. This conforms with the idea of treating an ontology and a logic program together as a unified theory.

Arguably, none of the embeddings can a priori be considered to be superior to the others. Our results give useful insight into the properties of the different embeddings, both on its own right and for knowledge combination. They provide a helpful guidance for the selection of an embedding for a particular scenario.

Proofs of all results are available in an extended version of this paper.

2 Preliminaries

First-Order Logic A first-order (FO) language L consists of all formulas over a signature Σ = (F, P), where F and P are countable sets of function and predicate symbols, respectively. Function symbols with arity 0 are called constants. V is a countably infinite set of variable symbols. Terms and atomic formulas (atoms) are constructed as usual for first-order logic with equality. Ground terms are also called names; NΣ is the set of names of a given signature Σ. Complex formulas are constructed as usual using the symbols ¬, ∧, ∨, ⊃, ∃, ∀,(, and ). A sentence is a formula with no free variables. The universal closure of a formula φ is denoted by ∀φ. Lg is the restriction of L to ground formulas; Lga is the restriction of Lg to atomic formulas. An FO theory Φ ⊆ L is a set of sentences.

An interpretation of a language L is a tuple w = 〈U, ·I 〉, where U is a nonempty set, called the domain, and ·I is a mapping which assigns a function f I : U n → U to every nary function symbol f ∈ F and a relation pI ⊆ U n to every n-ary predicate symbol p ∈ P. A variable assignment B for w is a mapping which assigns an element xB ∈ U to every variable x ∈ V. The interpretation of a term t, denoted tw,B , is defined as usual; if t is ground, we write tw instead of tw,B .

An individual k with at least one name t ∈ N such that tw = k is called a named individual, and unnamed otherwise.

In case names are interpreted distinctly, the unique-names assumption applies. If, additionally, every individual is named, the standard-names assumption applies.

A variable substitution β is a set {x1/t1, ..., xk/tk}, where x1, ..., xk are distinct variables and t1, ..., tk are names. β is total if it contains some x/n for every variable x ∈ V. Given variable assignment B and substitution β, if β = {x/t | x ∈ V, tw = xB , for some name t}, then β is associated with B. The application of a variable substitution β to some term, formula, or theory, denoted by appending β to it, is defined as syntactical replacement, as usual. Clearly, if the uniquenames assumption applies, each variable assignment has a unique associated substitution; if the standard-names assumption applies, each associated substitution is total.

Example 1. Consider a language L with constants F = {a, b, c}, and an interpretation w = 〈U, ·I 〉 with U = {k, l,m} such that aw = k, bw = l, and cw = l, and the variable assignment B: xB = k, yB = l, and zB = m. B has two associated variable substitutions, β1 = {x/a, y/b} and β2 = {x/a, y/c}, which are not total.

Logic Programs A disjunctive logic programP consists of rules of the form

where h1, . . . , hl, b1, . . . , bm, c1, . . . , cn are (equality-free) atoms. H(r) = {h1, . . . , hl} is the set of head atoms of r, B+(r) = {b1, . . . , bm} is the set of positive body atoms of r, and B-(r) = {c1, . . . , cn} is the set of negative body atoms of r. If l = 1, then r is normal. If B-(r) = ∅, then r is positive. If every variable in r occurs in B+(r), then r is safe. If every rule r ∈ P is normal (resp., positive, safe), then P is normal (resp., positive, safe).

By a first-order signature, ΣP , we understand a superset of the function and predicate symbols which occur in P . Let LP denote the first-order language based on ΣP . We assume that ΣP contains at least one 0-ary function symbol or only 0-ary predicate symbols. The Herbrand base, BH, of LP is the set of ground atomic formulas of LP . Subsets of BH are called Herbrand interpretations.

The grounding of a logic programP , denoted gr(P), is the union of all possible ground instantiations of P, obtained by replacing each variable in a rule r with a name in NΣP , for each rule r ∈ P .

Let P be a positive program. A Herbrand interpretation M of P is a model of P if, for every rule r ∈ gr(P), B+(r) ⊆ M implies H(r) ∩M ̸= ∅. A Herbrand model M is minimal iff for every model M ′ such that M ′ ⊆M, M ′ = M.

Following Gelfond and Lifschitz [1991], the reduct of a logic programP with respect to an interpretationM, denoted P M , is obtained from gr(P) by deleting (i) each rule r with B-(r) ∩M ̸= ∅, and (ii) not c from the body of every remaining rule r with c ∈ B-(r). If M is a minimal Herbrand model of P M , then M is a stable model of P .

3 First-order Autoepistemic Logic

We adopt the definition of first-order autoepistemic logic (FO-AEL) under the any- and all-name semantics following Konolige [1991], using a novel characterization with associated variable substitutions. The benefit of these semantics is that they allow quantification over arbitrary domains and generalize classical first-order logic with equality, thereby allowing a trivial embedding of first-order theories. Other approaches [Kaminski and Rey, 2002; Levesque and Lakemeyer, 2000] restrict the domains of interpretations to unique or standard names and therefore do not allow such direct embeddings.

An FO-AEL language LL is defined relative to a first-order language L: (i) any atomic formula in L is a formula in LL; (ii) if φ is a formula in LL, then Lφ, called a modal atom, 1 is a formula in LL; and (iii) complex formulas are constructed as in first-order logic. A formula without modal atoms is an objective formula. Standard autoepistemic logic is FO-AEL without variables.

An autoepistemic interpretation is a pair 〈w, Γ〉, where w = 〈U, ·I 〉 is a first-order interpretation and Γ ⊆ LL is a set of sentences, called the belief set. Satisfaction of objective atomic formulas in w is as in first-order logic.

Satisfaction of a formula Lφ in an interpretation 〈w, Γ〉 with respect to a variable assignment B under the any-name semantics (resp., all-name semantics) is defined as follows:

w,B |=Γ Lφ iff, for some (resp., all) variable substitution(s) β, associated with B, φβ is closed and φβ ∈ Γ.

This extends to complex formulas in the usual way. Notice that in case the unique-names assumption applies, the anyand all-name semantics coincide.

〈w, Γ〉 is a model of φ, denoted w |=Γ φ, if w,B |=Γ φ for every variable assignment B of w. This extends to sets of formulas in the usual way. A set A ⊆ LL of formulas entails a sentence φ with respect to a belief set Γ, denoted A |=Γ φ, if for every interpretation w such that w |=Γ A, w |=Γ φ.

Example 2. Consider a language with constant symbols a, b and unary predicate symbol p, and an interpretation 〈w, Γ〉 with w = 〈{k}, ·I 〉 and Γ = {p(a)}. Under the any-name semantics, w |=Γ ∃x.Lp(x); under the all-name semantics, w ̸|=Γ ∃x.Lp(x), because bw = aw = k, but p(b) /∈ Γ.

We deem this behavior of the all-name semantics counterintuitive; so, following Konolige [1991], we use the any-name semantics in what follows, unless stated otherwise.

Example 3. Consider the formula φ = ∀x(p(x) ⊃ Lp(x)) and some interpretation 〈w, Γ〉. Then: w |=Γ φ iff for every variable assignment B, w, B |=Γ p(x) ⊃ Lp(x) iff w, B ̸|=Γ p(x) or w,B |=Γ Lp(x). Now, w,B |=Γ Lp(x), with xB = k, iff for some t ∈ NΣ, tw = k, and p(t) ∈ Γ. Thus, φ is false in any interpretation where pI contains unnamed individuals.

A belief set T ⊆ LL is a stable expansion of a base set A ⊆ LL iff T = {φ | A |=T φ}. We use the following notation in the remainder: To = T ∩ L, Tog = T ∩ Lg, and Toga = T ∩ Lga.

A formula φ is an autoepistemic consequence of A if φ is included in every stable expansion of A. Cons(A) denotes the set of all autoepistemic consequences of A. Conso(A) denotes the restriction of Cons(A) to objective formulas.

1 Lφ is usually read as "φ is known" or "φ is believed."

Every stable expansion T fulfills the following properties: (a) T is closed under first-order entailment, (b) if φ ∈ T then Lφ ∈ T , and (c) if φ /∈ T then ¬Lφ ∈ T . If T is consistent, the converses of (b) and (c) also hold.

Konolige [1991] shows that a stable expansion T of a base set A is determined by its objective subset To, called the kernel of T . If A does not have nested modal operators, then, additionally, To = {φ ∈ L | A |=To φ} iff To is the kernel of a stable expansion T of A. We extend this result as follows:

Proposition 1. Given a base set A ⊆ LL with only objective atomic formulas in the context of modal atoms, and a set of objective formulas Γo ⊆ L, with Γga = Γo ∩ Lga, then Γo = {φ ∈ L | A |=Γga φ} iff Γo = T ∩ L for some stable expansion T of A.

4 Embedding Non-Ground Logic Programs

We define an embedding as a function which takes a logic program P as its argument and returns a set of sentences in the FO-AEL language obtained from ΣP .

Since the unique-names assumption does not hold in FOAEL in general, it is necessary to axiomatize default uniqueness of names (as introduced by Konolige [1991]). By UNAΣ we denote the set of axioms

¬L(t1 = t2) ⊃ t1 ̸= t2, for all distinct t1, t2 ∈ NΣ.

4.1 Embedding Normal Logic Programs

The first embedding we consider is an extension of the one which originally led Gelfond and Lifschitz to the discovery of the stable model semantics [Gelfond and Lifschitz, 1988]. The second and third embedding are extensions of the embeddings due to Marek and Truszczy´nski [1993]. The third was independently developed by Lifschitz and Schwarz [1993], and Chen [1993]. The original motivation for the second and third embedding was the possibility to directly embed programs with strong negation and disjunctive programs.

Definition 1. Let r be a rule of form (1) with l = 1. Then:

For a normal logic program P , we define:

In the above embeddings, "HP" stands for "Horn for positive rules" (positive rules are translated to objective Horn clauses); "EB" stands for "epistemic rule bodies" (the body of a rule can only become true if it is known to be true); and "EH" stands for "epistemic rule heads" (if the body of a rule is true, the head is known to be true). For all three embeddings, we assume Στx(P) = ΣP (here and henceforth we use "x" as a meta-variable to range over HP, EB, and EH ). Furthermore, by τ - x we denote the embedding τx without the UNA axioms. In the examples of embeddings in the remainder of the paper, we do not write the UNA axioms explicitly.

A notable distinction between the embedding τHP on the one hand and the embeddings τEB, τEH on the other is that the contrapositive of the rules in P is included in stable expansions of τHP , but not in stable expansions of τEB , τEH :

Example 4. Consider P = {p ← q}. The stable expansion of τHP(P) = {p ⊃ q} includes ¬q ⊃ ¬p; the expansion of τEB(P) = {p ∧ Lp ⊃ q} includes ¬q ⊃ ¬Lp ∨ ¬p, but not ¬q ⊃ ¬p, and neither does τEH (P ).

For the case of standard autoepistemic logic and ground logic programs, the following correspondence result holds:

Proposition 2 ([Gelfond and Lifschitz, 1988; Marek and Truszczy ´nski, 1993]). A Herbrand interpretation M is a stable model of a ground normal logic program P iff there is a consistent stable expansion T of τ - x (P) in standard autoepistemic logic such that M = T ∩ Lga.

Now consider the case of non-ground programs. The following example illustrates the embeddings:

Example 5. Consider P = {q(a); p(x); r(x) ← not s(x), p(x)}, having a single stable model M = {q(a), p(a), r(a)}. Likewise, each of the embeddings τHP(P), τEB(P), and τEH (P) has a single consistent stable expansion:

The stable expansions in Example 5 agree on objective ground atoms, but not on arbitrary formulas. We now extend Proposition 2 to the non-ground case.

Lemma 1. Given a set A ⊆ Lga of objective ground atoms, there exists a stable expansion T of τx(P) under the any- or all-name semantics with Toga = A iff there exists a stable expansion T ′ of τx(gr(P)) with T ′oga = A. Moreover, the same result holds for τ - HP under the all-name semantics.

Theorem 1. A Herbrand interpretation M of a normal logic program P is a stable model of P iff there is a consistent stable expansion T of τx(P) under the any- or all-name semantics such that M = T ∩ Lga. Moreover, the same result holds for τ - HP under the all-name semantics.

Note that this result does not hold for τ - HP under the any-name semantics. Consider P = {p(n1); r(n2); q ← not p(x)} such that ΣP has only two names, n1 and n2. P has one stable model, M = {p(n1), r(n2), q}. τ - HP (P) = {p(n1); r(n2); ∀x(¬Lp(x) ⊃ q)} has one stable expansion, T = {p(n1), r(n2), Lp(n1), Lr(n2), ¬Lp(n2), ...}. T does not include q. To see this, consider an interpretation w with only one individual k. Lp(x) is trivially true under the anyname semantics, because there is some name for k such that p(t) ∈ T (viz. t = n1). In the all-name semantics, this situation does not occur, because for Lp(x) to be true, p(t) must be included in T for every name (t = n1 and t = n2) for k. One can similarly verify that the result does not apply to the embeddings τ - EB and τ - EH under the all-name semantics, by the positive modal atoms in the antecedents.

4.2 Embedding Disjunctive Logic Programs

The embeddings τHP and τEB cannot be straightforwardly extended to disjunctive logic programs, even in the propositional case. Consider the program P = {a | b ←}. P has two stable models: M1 = {a} and M2 = {b}. However, a straightforward extension of τHP, τ ∨HP (P) = {a ∨ b}, has one stable expansion T = {a ∨ b, L(a ∨ b), ¬La, ¬Lb, ...}. In contrast, τEH can be straightforwardly extended because of the modal atoms in the consequent of the implication: τ ∨ EH (P ) = {(a ∧ La) ∨ (b ∧ Lb)} has two stable expansions T1 = {a ∨ b, a, La, ¬Lb, ...} and T2 = {a ∨ b, b, Lb, ¬La, ...}.

The so-called positive introspection axioms (PIAs) [Przymusinski, 1991] remedy this situation for τ ∨HP and τ ∨ EB . Let PIAΣ be the set of axioms

• α ⊃ Lα, for every objective ground atom α of Σ.

The PIA α ⊃ Lα ensures that every consistent stable expansion contains either α or ¬α.

It would have been possible to define the PIAs in a different way: ∀φ ⊃ Lφ for any objective atomic formula φ. This would, however, effectively close the domain of the predicates in Σ (see Example 3). We deem this aspect undesirable in combinations with FO theories.

Definition 2. Let r be a rule of form (1). Then:

For a disjunctive logic program P , we define:

As before, by τ ∨- x we denote the embedding τ ∨ x without the UNA part. We do not write the UNA and PIA parts explicitly in the examples below.

For the case of standard autoepistemic logic and ground disjunctive logic programs, the correspondence between the stable expansions of the embeddings τ ∨HP (P) and τ ∨ EH (P ) and the stable models of P is known:

Proposition 3 ([Przymusinski, 1991; Marek and Truszczy´nski, 1993]). A Herbrand interpretationM of a ground disjunctive logic program P is a stable model of P iff there is a consistent stable expansion T of τ ∨- HP (P) (resp., τ ∨- EH (P )) in standard autoepistemic logic such that M = T ∩ Lga.

We generalize this result to the case of FO-AEL and nonground programs, and additionally for τ ∨ :

EB

Theorem 2. A Herbrand interpretation M of a disjunctive logic program P is a stable model of P iff there is a consistent stable expansion T of τ ∨ x (P) under the any- or all-name semantics such that M = T ∩Lga. Moreover, the same result holds for τ - HP under the all-name semantics.

A notable distinction between the embeddings τ ∨HP and τ ∨ EB on the one hand and τ ∨ EH on the other is the presence and absence of the PIAs, respectively:

Example 6. Consider P = {p | q ←}, τ ∨HP (P ) = {p ∨ q} ∪ PIAΣP , and τ ∨ EH (P) = {(p ∧ Lp) ∨ (q ∧ Lq)}. The stable expansions of τ ∨HP (P) are T HP 1 = {p, ¬q, Lp, ¬Lq, ...} and T HP 2 = {q, ¬p, Lp, ¬Lp, ...}; the expansions of τ ∨ EH (P) are T EH 1 = {p, Lp, ¬Lq, ...} and T EH 2 = {q, Lp, ¬Lp, ...}. The expansions T EH 1 and T EH 2 include neither ¬q nor ¬p.

5 Relations between the Embeddings

In this section, we explore correspondences between the embeddings presented in the previous section in combinations with FO theories. In our simple setting, we define the combination of a program P and an FO theory Φ as

where ΣLL is the union of the signatures ΣΦ and ΣP . Recall that we consider the any-name semantics, because of its more intuitive behavior (cf. 3).

In the following, we compare (i) the stable expansions of such combinations and (ii) the sets of autoepistemic consequences of the individual embeddings. To this end, we introduce the following notation:

Let A1 and A2 be FO-AEL theories. We write A1 ≡ A2 iff A1 and A2 have the same stable expansions. Moreover, for α ∈ {g, ga}, we write A1 ≡α A2 iff

Note that, by definition, A1 ≡ A2 implies A1 ≡g A2, and A1 ≡g A2 implies A1 ≡ga A2.

In our analysis, we furthermore use the following classes of programs and theories:

• the classes Prg, Safe, and Grnd of arbitrary, safe, and ground logic programs, respectively; and
• the classes Thr, Uni, gHorn, Horn, Prop, and {∅} of arbitrary, universal, generalized Horn, 3 Horn, propositional, and empty FO theories.

Observe the following inclusions:

Theorem 3. Let P be a normal (disjunctive, resp.) logic program and Φ be a first-order theory. Then, the relations depicted in Table 1 (with the respective provisos) hold, providing P and Φ belong to the classes listed there.

2 One could imagine other, non-trivial, embeddings of the classical theory. Such embeddings are a topic for future investigations.

3 Generalized Horn formulas are Horn formulas which additionally allow existentially quantified variables in the consequent of the material implication.

Consider the logic program P from Example 5. P is neither safe nor ground: to determine correspondence between embeddings, we need to use the first column of Table 1. Since P is normal, all equations in this column are applicable. We have that τEB(P) ≡g τEH(P) and τ ∨HP (P) ≡g τ ∨ EB (P). Let Φ be a Horn theory, then ιHP(Φ, P) ≡ga ιEH(Φ, P) ≡ga ιEB (Φ, P ) and ιEH (Φ, P ) ≡ ι∨EH (Φ, P ).

Additionally, since autoepistemic consequence is defined through the intersection of all stable expansions, we can conclude that τEB(P) and τEH(P), and also τ ∨HP (P) and τ ∨ EB (P), agree on objective ground autoepistemic consequence and that ιHP (Φ, P ), ιEH (Φ, P ), and ιEB (Φ, P ) agree on objective ground atomic autoepistemic consequence.

We now consider the relative behavior of the embeddings with respect to autoepistemic consequences.

Theorem 4. Let P be a (safe) normal (disjunctive, resp.) logic program, and let τ (∨) x and τ (∨) y be embedding functions, for x, y ∈ {HP, EB, EH}. Then, relations Conso(τ (∨) x (P)) ⊆ Conso(τ (∨) y (P)) hold as depicted in Figure 1 (with the respective provisos).

Most of the relations given in Figure 1 do not hold for combinations with FO theories. Consider, e.g., P = {r ← not p, not q} and Φ = {p ∨ q}. Then, τHP(P) = {¬Lp ∧ ¬Lq ⊃ r} and τ ∨HP (P) = {¬Lp ∧ ¬Lq ⊃ r} ∪ PIAΣP both have one stable expansion, each containing ¬Lp, ¬Lq, and r. The combination τHP(P) ∪ Φ has one stable expansion which includes ¬Lp, ¬Lq, and r; τ ∨HP (P) ∪ Φ has two stable expansions {p, Lp, ¬Lq, ...} and {q, Lq, ¬Lp, ...}, neither of which includes r. Thus, r is an autoepistemic consequence of ιHP(Φ, P), but not of ι∨HP (Φ, P). Therefore, Conso(ιHP (Φ, P )) ̸⊆ Conso(ι∨HP (Φ, P )).

Using the results in this section, we can make a number of observations about the embeddings:

1. Few correspondences between embeddings with PIAs and those without hold. However, we can note that the former are stronger in terms of the number of objective autoepistemic consequences (cf. Figure 1 and Example 6).
2. The embeddings τHP and τ ∨HP are generally the strongest in terms of consequences (see Figure 1). They allow to derive the contrapositive of rules (cf. Example 4) and the bodies of rules are applicable to unnamed individuals, whereas the antecedents of the axioms in the other embeddings are only applicable to named individuals, because of the positive modal atoms in the bodies.
3. For unsafe programs, the embeddings τEH and τ ∨ EH are generally not comparable with the others; embeddings of un-

safe rules result in axioms of form ∀xLp(x) (cf. Example 5), which require all individuals to be named.

1. In case the programs are safe, or one assumes that all individuals are named, τEB and τEH coincide.

We conclude this section with an example which demonstrates possibly unexpected effects of the UNA axioms in their interaction with an FO theory.

Example 7. Consider P = {p(a); p(b)} and Φ = {a ̸= b ⊃ r}. Then, r is included in any stable expansion of Φ∪ τx(P), for any τx, in view of the UNA axioms.

6 Related and Future Work

In this paper, we have studied the combination of logic programs and ontologies (FO theories) using embeddings in a unifying formalism (FO-AEL). One could imagine, in contrast, extensions of semantics for logic programs or ontologies to incorporate (parts of) the other formalism. One such extension of logic programming semantics is that of open domains [Gelfond and Przymusinska, 1993; Van Belleghem et al., 1997; Heymans et al., 2005]. Such extended semantics can be used to accommodate incomplete knowledge, an important aspect of ontology languages. Nonmonotonic extensions of description logics (an FO-based formalism suitable for ontologies) have been presented in the literature [Baader and Hollunder, 1995; Donini et al., 2002; Bonatti et al., 2006]. Such approaches might be extended to accommodate logic programs.

We have investigated basic correspondences between different embeddings of non-ground programs in FO-AEL, and simple combinations with FO theories. Choosing different embeddings for logic programs, but also possibly different embeddings for first-order theories, will give rise to different properties of such combinations [de Bruijn et al., 2006]. In future work, we will investigate these properties, as well as the relationship with existing approaches to combine logic programs and classical theories [Horrocks and PatelSchneider, 2004; Eiter et al., 2004; Rosati, 2006].

So far, we have only considered equality-free logic programs. We conjecture that equality in rule bodies poses no problems, since still only the trivial equalities are derivable. Allowing equality in rule heads is a topic for further research.

We expect that the proposed combinations of rules and ontologies based on FO-AEL will give rise to the definition of novel decidable fragments and for sound (but possibly incomplete) algorithms for specific reasoning tasks for such combinations. Additionally, we will consider other nonmonotonic logics (e.g., default logic and circumscription) as formalisms for combining logic programs and classical knowledge bases.