A Uniform Integration of Higher-Order Reasoning and External Evaluations in Answer-Set Programming

1 Introduction

Answer-Set Programming (ASP) [Gelfond and Lifschitz, 1991] has recently attracted increasing interest as a declarative problem solving paradigm. In this approach, a problem is encoded in terms of a nonmonotonic logic program such that the solutions of the former can be extracted from the answer sets of the latter. Due to the availability of ef�- cient answer-set solvers, like Smodels [Simons et al., 2002] or DLV [Leone et al., 2005], and various extensions of the basic language with features such as classical negation, weak constraints, or aggregates, ASP has become an important KR formalism for declaratively solving AI problems in areas including planning, diagnosis, information integration, and reasoning about inheritance. For the challenging area of Semantic Web reasoning, extensions of ASP have been proposed, facilitating interoperability with Description Logic reasoners [Rosati, 1999; Eiter et al., 2004] or aiming at handling in�- nite, tree-structured models [Heymans and Vermeir, 2003].

∗This work was partially supported by the Austrian Science Fund (FWF) under grant P17212-N04, and by the European Commission through the IST Networks of Excellence REWERSE (IST2003-506779) and CologNeT (IST-2001-33123), and the IST Working Group in Answer Set Programming (IST-2001-37004 WASP).

However, for important issues such as meta-reasoning in the context of the Semantic Web, no adequate support is available in ASP to date. Motivated by this fact and the observation that interoperability with other software is (not only in this context) an important issue, we extend in this paper the answer-set semantics to HEX programs, that is, higher-order logic programs (which accommodate meta-reasoning through higher-order atoms) with external atoms for software interoperability. Intuitively, a higher-order atom allows to quantify values over predicate names, and to freely exchange predicate symbols with constant symbols, like in the rule

An external atom facilitates to determine the truth value of an atom through an external source of computation. For instance, the rule

computes the predicate reached taking values from the predicate #reach, which computes via #reach[edge, a] all the reachable nodes in the graph edge from node a, delegating this task to an external computational source (e.g., an external deduction system, an execution library, etc.).

Our main contributions are summarized as follows.

1. We de�ne the syntax and answer-set semantics of HEX programs, extending ASP with higher-order features and powerful interfacing of external computation sources. While answer-set semantics for higher-order logic programs has been proposed earlier by Ross [1994], further extension of that proposal to accommodate external atoms is technically dif�cult since the approach of Ross is based on the notion of unfounded set, which cannot be easily generalized to this setting. Our approach, instead, is based on a recent notion of program reduct, due to Faber et al. [2004], which admits a natural de�nition of answer-set semantics.

(2) External atoms are a useful abstraction of several extensions to ASP including, among others, aggregates, description logic atoms, or agent programs. External atoms thus facilitate investigating common properties of such extensions, and can serve as a uniform framework for de�ning semantics of further similar extensions of ASP. Moreover, HEX programs are a basis for the ef�cient design of generic evaluation algorithms for such extensions in this framework.

(3) By means of HEX programs, powerful meta-reasoning becomes available in a decidable context, e.g., for Semantic Web applications, for meta-interpretation in ASP itself, or for de�ning policy languages. For example, advanced closed world reasoning or the de�nition of constructs for an extended ontology language (e.g., of RDF-Schema) is wellsupported. Due to the higher-order features, the representation is succinct.

(4) A simple prototype implementation of the language is available, based on a reduction to ordinary ASP.

Note that other logic-based formalisms, like TRIPLE [Sintek and Decker, 2002] or F-Logic [Kifer et al., 1995], feature also higher-order predicates for meta-reasoning in Semantic Web applications. However, TRIPLE is low-level oriented and lack precise semantics, while F-Logic in its implementations (Flora, Florid, Ontoweb) restricts its expressiveness to well-founded semantics for negation, in order to gain ef�- ciency. Our formalism, instead, is fully declarative and offers the possibility of nondeterministic predicate de�nition with higher complexity. This proved already useful and reasonably ef�cient for a range of applications with inherent nondeterminism, such as diagnosis, planning, or con�guration, and thus provides a rich basis for integrating these areas with meta-reasoning.

2 HEX Programs

2.1 Syntax

Let C, X , and G be mutually disjoint sets whose elements are called constant names, variable names, and external predicate names, respectively. Unless explicitly speci�ed, elements from X (resp., C) are denoted with �rst letter in upper case (resp., lower case), while elements from G are pre�xed with � # �. We note that constant names serve both as individual and predicate names.

Elements from C ∪ X are called terms. A higher-order atom (or atom) is a tuple (Y0, Y1, . . . , Yn), where Y0, . . . , Yn are terms; n ≥ 0 is the arity of the atom. Intuitively, Y0 is the predicate name, and we thus also use the more familiar notation Y0(Y1, . . . , Yn). The atom is ordinary, if Y0 is a constant.

For example, (x, rdf :type, c), node(X), and D(a, b), are atoms; the �rst two are ordinary atoms.

An external atom is of the form

where Y1, . . . , Yn and X1, . . . ,Xm are two lists of terms (called input and output lists, respectively), and #g ∈ G is an external predicate name. We assume that #g has �xed lengths in(#g) = n and out(#g) = m for input and output lists, respectively. Intuitively, an external atom provides a way for deciding the truth value of an output tuple depending on the extension of a set of input predicates.

Example 1 The external atom #reach[edge, a](X) may be devised for computing the nodes which are reachable in the graph edge from the node a. Here, we have that in(#reach) = 2 and out (#reach) = 1. ✷

A rule r is of the form

where m, k ≥ 0, α1, . . . , αk are atoms, and β1, . . . , βm are either atoms or external atoms. We de�ne H(r) = {α1, . . . , αk} and B(r) = B+(r) ∪B-(r), where B+(r) = {β1, . . . , βn} and B-(r) = {βn+1, . . . , βm}. If H(r) = ∅ and B(r) ̸= ∅, then r is a constraint, and if B(r) = ∅ and H(r) ̸= ∅, then r is a fact; r is ordinary, if it contains only ordinary atoms.

A HEX program is a �nite set P of rules. It is ordinary, if all rules are ordinary.

2.2 Semantics

We de�ne the semantics of HEX programs by generalizing the answer-set semantics [Gelfond and Lifschitz, 1991]. To this end, we use the recent notion of a reduct as de�ned by Faber et al. [2004] (referred to as FLP-reduct henceforth) instead of to the traditional reduct by Gelfond and Lifschitz [1991]. The FLP-reduct admits an elegant and natural de�nition of answer sets for programs with aggregate atoms, since it ensures answer-set minimality, while the de�nition based on the traditional reduct lacks this important feature.

In the sequel, let P be a HEX program. The Herbrand base of P , denoted HBP , is the set of all possible ground versions of atoms and external atoms occurring in P obtained by replacing variables with constants from C. The grounding of a rule r, grnd(r), is de�ned accordingly, and the grounding of program P is given by grnd(P) = ⋃r∈P grnd(r). Unless speci�ed otherwise, C, X , and G are implicitly given by P .

Example 2 Given C = {edge, arc, a, b}, ground instances of E(X, b) are edge(a, b), arc(a, b), and arc(arc, b); ground instances of #reach[edge, N](X) are #reach[edge, edge](a), #reach[edge, arc](b), and #reach[edge, edge](edge), etc.✷

An interpretation relative to P is any subset I ⊆ HBP containing only atoms. We say that I is a model of atom a∈HBP , denoted I |=a, if a∈I.

With every external predicate name #g ∈ G, we associate an (n+m+1)-ary Boolean function f#g assigning each tuple (I, y1 . . . , yn, x1, . . . , xm) either 0 or 1, where n = in(#g), m = out(#g), I ⊆ HBP , and xi, yj ∈ C.

We say that I ⊆ HBP is a model of a ground external atom a = #g[y1, . . . , yn](x1, . . . , xm), denoted I |=a, if and only if f#g(I, y1 . . ., yn, x1, . . . , xm)=1.

Example 3 Let us associate with #reach a function f#reach such that f#reach(I,E,A,B) = 1 iff B is reachable in the graph E from A. Let I = {e(b, c), e(c, d)}. Then, I is a model of #reach[e, b](d) since f#reach(I, e, b, d) = 1. ✷

Let r be a ground rule. We de�ne (i) I |=H(r) iff there is some a ∈ H(r) such that I |=a, (ii) I |=B(r) iff I |=a for all a∈B+(r) and I ̸|=a for all a∈B-(r), and (iii) I |=r iff I |=H(r) whenever I |=B(r). We say that I is a model of a HEX program P, denoted I |=P, iff I |=r for all r ∈grnd(P). We call P satis�able, if it has some model.

Given a HEX program P , the FLP-reduct of P with respect to I ⊆HBP , denoted fP I , is the set of all r ∈ grnd(P) such that I |= B(r). I ⊆HBP is an answer set of P iff I is a minimal model of fP I .

We next give an illustrative example.

Example 4 Consider the following HEX program P:

Informally, this program randomly selects a certain number of John's relatives for invitation. The �rst line states that brotherOf is a subrelation of relativeOf , and the next two lines give concrete facts. The disjunctive rule chooses relatives, employing the external predicate #reach from Example 3. The next rule declares a generic subrelation inclusion exploiting higher-order atoms.

The constraints ensure that the number of invitees is between 1 and 2, using (for illustration) an external predicate #degs from a graph library, where f#degs(I,E,Min,Max) is 1 iff Min and Max is the minimum and maximum vertex degree of the graph induced by the edges E, respectively. As John's relatives are determined to be Al, Joe, and Mick, P has six answer sets, each of which contains one or two of the facts invites(john, al), invites(john, joe), and invites (john , mick ). ✷

We now state some basic properties of the semantics.

Theorem 1 The answer-set semantics of HEX programs extends the answer-set semantics of ordinary programs as de�ned by Gelfond and Lifschitz [1991], as well as the answerset semantics of HiLog programs as de�ned by Ross [1994].

The next property, which is easily proved, expresses that answer sets adhere to the principle of minimality.

Theorem 2 Every answer set of a HEX program P is a minimal model of P .

A ground external atom a is called monotonic relative to P iff I ⊆I ′ ⊆HBP and I |=a imply I ′ |=a. For instance, the ground versions of #reach[edge, a](X) are all monotonic.

Theorem 3 Let P be a HEX program without �not� and constraints. If all external atoms in grnd(P) are monotonic relative to P, then P has some answer set. Moreover, if P is disjunction-free, it has a single answer set.

Notice that this property fails if external atoms can be nonmonotonic. Indeed, we can easily model default negation not p(a) by an external atom #not[p](a); the HEX program p(a) ← #not[p](a) amounts then to the ordinary program p(a) ← not p(a), which has no answer set.

3 Modeling ASP Extensions by External Atoms

By means of external atoms, different important extensions of ASP can be expressed in terms of HEX programs.

3.1 Programs with aggregates

Extending ASP with special aggregate atoms, through which the sum, maximum, etc. of a set of numbers can be referenced, is an important issue which has been considered in several recent works (cf., e.g., [Faber et al., 2004]). A nontrivial and challenging problem in this context is giving a natural semantics for aggregates involving recursion. The recent proposal of a semantics by Faber et al. [2004] is an elegant solution of this problem. We show here how it can be easily captured by HEX programs.

An aggregate atom a(Y, T) has the form f{S} ≺ T, where f is an aggregate function (sum, count, max, etc.), ≺∈ {=,<,≤,>,≥}, T is a term, and S is an expression X: ⃗E( ⃗X, ⃗Y , ⃗Z), where ⃗X and ⃗Y are lists of local variables, ⃗Z is a list of global variables, and ⃗E is a list of atoms whose variables are among ⃗X, ⃗Y , ⃗Z.

For example, #count{X : r(X,Z), s(Z, Y )} ≥ T is an aggregate atom which is intuitively true if, for given Y and T , at least T different values for X are such that the conjunction r(X, Z), s(Z, Y ) holds.

Given a(Y, T) = f{S} ≺ T as above, an interpretation I, and values y for Y and t for T, f is applied to the set S(I, y) of all values x for X such that I |= E(x, y, z) for some value z for Z. We then have I |= a(y, t) (i.e., I |= f{X:E(X, y, Z)} ≺ t) iff f(S(I, y)) ≺ t.

Using the above notion of truthhood for a(y, t), Faber et al. [2004] de�ne answer sets of an ordinary program plus aggregates using the reduct fP I .

We can model an aggregate atom a(Y, T) by an external atom#a[Y ](T) such that for any interpretation I and ground version #a[y](t) of it, f#a(I, y, t)=1 iff I |=a(y, t). Note that writing code for evaluating f#a(I, y, t) is easy.

For any ordinary program P with aggregates, let #agg(P ) be the HEX program which results from P by replacing each aggregate atom a(Y, T) with the respective external atom #a[Y ](T). The following result can then be shown:

Theorem 4 For any ordinary program P with aggregates, the answer sets of P and #agg(P) coincide.

3.2 Description logic programs

The aim of description logic programs (or dl-programs), due to Eiter et al. [2004], is to combine a rule language under the answer-set semantics with description logics. Informally, a dl-program consists of a description logic (DL) knowledge base L and a generalized normal program P which may contain queries to L, realized by means of special atoms, called dl-atoms, appearing in the body of rules. A dl-atom allows for specifying an input from P to L, and thus for a bidirectional �ow of information between P to L, and for querying whether a certain DL axiom or its negation logically follows from L. The DL knowledge bases in dl-programs are theories in the description logics SHIF(D) and SHOIN(D), which represent the logical underpinnings of the Web ontology languages OWL Lite and OWL DL, respectively [Bechhofer et al., 2004].

Formally, a dl-atom is an expression dl (X) of form

where each Si is a DL concept or role name, opi a change operator, pi a unary resp. binary predicate symbol, Q a unary resp. binary predicate, and X a list of terms matching the arity of Q. For space reasons, we con�ne here to opi = ⊎ and Q being a possibly negated unary predicate name, for which X is a single term. Intuitively, Si ⊎ pi increases Si in L by the extension of pi. For example, the dl-atom

queries a wine ontology if W is known to be a white wine, after augmenting the ontology about wine color (hasColor) with facts about color from a program P .

An interpretation I of P is a model of a ground instance dl (c) of dl-atom dl (X) with respect to DL knowledge base L, denoted I |=L dl(c), if L∪ ⋃mi=1 {Si(b) | pi(b)∈I} |=Q(c), where |= is the entailment operator of the given description logic. That is, I |=L dl(c) iff c belongs to concept Q after augmenting L.

Eiter et al. [2004] de�ne answer sets of an ordinary nondisjunctive program P relative to a DL knowledge base L through a reduct sP IL, which extends the traditional reduct of Gelfond and Lifschitz [1991]. Assuming that each ground dlatom dl(c) is monotonic (i.e., I |=dl(c) implies I ′ |=dl(c), for I ⊆ I ′ ; this is the predominant setting), sP IL treats negated dl-atoms like negated ordinary atoms. The resulting ground program sP IL has a least model, LM(sP IL). Then, I is a strong answer set of (L, P) iff I = LM(sP IL) holds.

We can simulate dl-atoms by external atoms in several ways. A simple one is to use external atoms #dl[ ](X) where f#dl(I, c)=1 iff I |=Ldl(c). Let #dlL(P) be the HEX program obtained from a dl-program (L, P) by replacing each dl-atom dl (X) with #dl[ ](X). We can then show:

Theorem 5 Let (L, P) be any dl-program for which all ground dl-atoms are monotonic. Then, the strong answer sets of (L, P) and #dlL(P) coincide.

Note that we can extend the strong answer-set semantics to disjunctive dl-programs by simply extending the embedding #dlL(P) to disjunctive programs. This illustrates the use of HEX programs as a framework for de�ning semantics.

3.3 Programs with monotone cardinality atoms

Marek et al. [2004] present an extension of ASP by monotone cardinality atoms (mc-atoms) kX, where X is a �nite set of ground atoms and k≥0. Such an atom is true in an interpretation I, if k ≥ |X∩I| holds. Note that an ordinary atom A amounts to 1{A}. An mca-program is a set of rules

where H and the Bi's are mc-atoms. Answer sets (stable models) for an mca-program P are interpretations I which are derivable models of an extended reduct P I (in the sense of Gelfond and Lifschitz [1991]), which treats negated mcatoms like negated ordinary atoms. Informally, a model of P I is derivable, if it can be created from the empty set by iterative rule applications in which the heads of �ring rules are nondeterministically satis�ed.

We can embed any mca-program P into a HEX program #mc(P) as follows. Each mc-atom kX is modeled by an external atom e(kX) = #k X[ ](), where f#k X(I)=1 iff k≥|X∩I|. In each rule of form (3), we replace H with a new atom tH and all Bi with e(Bi), and add the following rules (for H = k {A1, . . . , Am}):

where, globally, n A is a new atom for each atom A. Informally, these rules simulate the occurrence of the mc-atom in the head. Then, the following correspondence holds.

Theorem 6 For any �nite mca-program P over atoms At, the answer sets of P and #mc(P) projected to At coincide.

As shown by Marek et al. [2004], ASP extensions similar to mca-programs can be modeled as mca-programs. Hence, these extensions can be similarly embedded into HEX programs.

3.4 Agent programs

Eiter et al. [1999] describe logic-based agent programs, consisting of rules of the form

governing an agent's behavior. The Opi are deontic modalities, the αi are action atoms, and χ is a code-call condition. The latter is a conjunction of (i) code-call atoms of the form in(X, f(Y )) resp. notin(X, f(Y )), which access the data structures of the internal agent state through API functions f(Y ) and test whether X is in the result, and (ii) constraint atoms. For example, the rule

intuitively says that the agent should dial phone number N if she is obliged to call P .

A semantics of agent programs in terms of �reasonable status sets�, which are certain sets of ground formulas Opα, is de�ned by Eiter et al. [1999]. They show that the answer sets of a disjunction-free logic program P correspond naturally to the reasonable status sets of a straightforward agent program AG(P). Conversely, code-call atoms as above can be modeled by external atoms #inf [Y ](X) resp. #notinf [Y ](X), and deontic modalities by different propositions and suitable rules. In this way, a class of agent programs can be embedded into HEX programs as a host for evaluation.

4 Applications

In this section, we show the usage of HEX programs for different purposes, in which the joint availability of higher-order and external atoms is bene�cial. For space reasons, the exposition is necessarily super�cial and details will be omitted.

4.1 SemanticWeb applications

HEX programs are well-suited as a convenient tool for a variety of tasks related to ontology languages and for Semantic-Web applications in general, since, in contrast to other approaches, they keep decidability but do not lack the possibility of exploiting nondeterminism, performing metareasoning, or encoding aggregates and sophisticated constructs through external atoms.

An interesting application scenario where several features of HEX programs come into play is ontology alignment. Merging knowledge from different sources in the context of the Semantic Web is a very important task [Calvanese et al., 2001]. To avoid inconsistencies which arise in merging, it is important to diagnose the source of such inconsistencies and to propose a �repaired� version of the merged ontology. In general, given an entailment operator |= and two theories T1 and T2, we want to �nd some theory rep(T1 ∪ T2) which, if possible, is consistent (with respect to |=). Usually, rep is de�ned according to some customized criterion, so that to save as much knowledge as possible from T1 and T2. Also, rep can be nondeterministic and admit more than one possible solution.

HEX programs allow to de�ne |= according to a range of possibilities; in the same way, HEX programs are a useful tool for modeling and customizing the rep operator. In order to perform ontology alignment, HEX programs must be able to express tasks such as the following ones:

Importing external theories. This can be achieved, e.g., in the following way:

We assume here to deal with RDF theories. 1 We take advantage of an external predicate #RDF intended to extract knowledge from a given URI (Uniform Resource Identi�er), in form of a set of �rei�ed� ternary assertions.

Searching in the space of assertions. This task is required in order to choose nondeterministically which propositions have to be included in the merged theory and which not, with statements like

Translating and manipulating rei�ed assertions. E.g., for choosing how to put RDF triples (possibly including OWL assertions) in an easier manipulatable and readable format, and for making selected propositions true, the following rules can be employed:

1 See http://www.w3.org/tr/rdf-mt/ for information about RDF.

Filtering propositions. This way, it is possible to customize criteria for selecting which propositions can be dropped and which cannot. For instance, a proposition cannot be dropped if it is an RDFS axiomatic triple: 2

De�ning ontology semantics. The operator |= can be de�ned in terms of entailment rules and constraints expressed in the language itself, like in:

where the external atom #countr[R,X](M) expresses the aggregate atom#count{Y : R(X, Y )}=M. Also, semantics can be de�ned by means of external reasoners, using constraints like

where the external predicate #inconsistent takes for input a set of assertions and establishes through an external reasoner whether the underlying theory is inconsistent.

4.2 Closed world and default reasoning

Reiter's well-known closed-world assumption (CWA) 3 is acknowledged as an important reasoning principle for inferring negative information from a logical knowledge base KB: For a ground atom p(c), conclude ¬p(c) if KB ̸|= p(c). Description logic knowledge bases lack this possibility.

Using HEX programs, the CWA may be easily expressed on top of an external KB which can be queried through suitable external atoms. We show this here for a description logic knowledge base L. Assuming that a generic external atom #dl 0[C](X) for modeling a dl-atom DL[C](X) is available, the CWA principle can be stated as follows:

where concept (C) is a predicate which holds for all concepts, cwa(C,C ′ ) states that C ′ is the complement of C under the CWA, and o(X) is a predicate that holds for all individuals occurring in L. For example, given that

for concepts man and person, the CWA infers ¬man(lee).

As well known, the CWA can become inconsistent. If in the above example, L contains a further axiom

person = man ⊔ woman,

with the concept woman, then the CWA infers ¬man(lee) and ¬woman(lee); this is inconsistent with L.

2 In a language enriched with weak constraints, we could maximize the set of selected propositions using a constraint of form :∼drop(P ).

3 Throughout this section, we refer to �ukaszewicz [1990] for references to closed-world reasoning and circumscription.

We can check inconsistency of the CWA with further rules, though:

where #dl 1[N, C](X) effects a check whether L, augmented with all negated facts ¬c(a) such that N(c, a) holds, entails C(X), and ⊥ is the empty concept (entailment of ⊥(b), for any constant b, is tantamount to inconsistency).

Minimal-model reasoning, as under circumscription and the extended closed-world assumption (ECWA), for instance, avoids the problem of CWA inconsistency. We can foster the minimal Herbrand models of L with respect to all concepts and individuals in L elegantly with the following HEX rules:

Here, the �rst rule intuitively expresses that if C(X) is not included in an answer set M of P, then it should be set to false. The second rule states that C(X) is inM, if C(X) can be proved in L after setting all atoms in L to false according to M. By the minimality of answer sets, C(X) can only then be in M. Thus, in L no C(X) can be switched to ¬C(X) without raising inconsistency. Hence, M corresponds to a minimal model of L. Applied to our example, we obtain two answer sets (showing here only the interesting atoms):

corresponding to the minimal models of L.

Roles in L may be handled similarly. Furthermore, one can easily restrict minimization to a subset of concepts and roles, and accommodate the general setting of ECWA and circumscription, dividing the predicates into minimized, �xed, and varying predicates P , Q, and Z, respectively. On top of minimal models, e.g., reasoning tasks may then be performed.

By maximizing rather than minimizing extensions, default reasoning, as in the approach by Poole [1988], on top of a DL knowledge base L may be supported. For example, the rules

on top of a wine ontology L, express that sparkling wines are white by default, where #dl 2[C,U,Q](X) checks whether L, together with all facts C(a) such that a∈U, entails ¬Q(X). Given

we then can conclude white(veuveCliquot).

5 Computational Aspects

5.1 Complexity

It appears that higher-order atoms do not add complexity compared to ordinary atoms. Indeed, for �nite C, the grounding of an arbitrary HEX program P is, like for an ordinary program, at most exponential in the size of P and C. Since HEX programs with higher-order atoms subsume ordinary programs, we obtain by well-known complexity results for ordinary programs [Dantsin et al., 2001] the following result. Recall that NEXP denotes nondeterministic exponential time, and that for complexity classes C and D, C D denotes complexity in C with an oracle for a problem in D.

Theorem 7 Deciding whether a given HEX program P without external atoms has some answer set is NEXP NP -complete in general, and NEXP-complete if P is disjunction-free.

Classes of programs with lower complexity can be identi�ed under syntactic restrictions, e.g., on predicate arities. Furthermore, if from the customary ASP perspective, P is �xed except for ground facts representing ad-hoc input, the complexity exponentially drops to NP NP resp. NP.

On the other hand, external atoms clearly may be a source of complexity, and without further assumptions even incur undecidability. Viewing the function f#g associated with an external predicate #g ∈ G as an oracle with complexity in C, we have the following result:

Theorem 8 Let P be a HEX program, and suppose that for every #g ∈ G the function f#g has complexity in C. Then, deciding whether P has some answer set is in NEXP NP C , and is in NEXPC if P is disjunction-free.

However, there is no complexity increase by external atoms under the following condition on the cardinality of C:

Theorem 9 Let P be a HEX program. Suppose that for every #g ∈ G, the function f#g is decidable in exponential time in |C|. Then, deciding whether P has some answer set is NEXP NP -complete, and NEXP-complete if P is disjunctionfree.

Informally, the reason is that a possibly exponential-size grounding compensates the exponentiality of external atoms, whose evaluation then becomes polynomial in the size of grnd(P). The hypothesis of Theorem 9 applies to external atoms modeling aggregate atoms and, under small adjustments, to dl-atoms, if |= is decidable in exponential time. Some complexity results by Faber et al. [2004] on ASP with aggregates and by Eiter et al. [2004] on interfacing logic programs with the description logic SHIF(D) therefore follow easily from Theorems 4, 5, and 9.

5.2 Implementation

An experimental working prototype for evaluating HEX programs is available. Several technical issues in an implementation arise, and we can only brie�y address them here. In particular, higher-order and external atoms must be handled.

As for higher-order atoms, a polynomial reduction Λ from HEX programs P to ordinary programs Λ(P) is possible if P has no external atoms. Indeed, each higher-order atom Y0(Y1, . . . , Yn) in P can be substituted with an ordinary atom an(Y0, Y1, . . . , Yn). Since HEX programs conservatively extend ordinary programs (cf. Theorem 1), the answer sets of any HEX program P without external atoms then correspond one-to-one with the answer sets of Λ(P). Thus, HEX programs without external atoms can be ef�ciently evaluated by using an existing ASP solver.

The presence of external atoms makes matters more complex. Λ can still be applied to eliminate higher-order atoms from a HEX program P , and a similar correspondence holds. We may further replace external atoms #g[ ⃗X](⃗Y ) in Λ(P) by ordinary atoms p#g( ⃗X, ⃗Y ). In the absence of negation as failure and for monotone external atoms, the answer sets of Λ(P) can be computed by a bottom-up �xpoint computation (which in case of disjunction is nondeterministic), in which ground atoms p#g(⃗a,⃗b) are evaluated with the external function f#g.

In the presence of negation as failure, a notion of e-strati�cation, which generalizes the usual notion of strati�cation and exploits further dependency information supplied for external atoms, can be used to identify a substantial fragment of HEX programs evaluable on the basis of a suitable operational semantics. In the unstrati�ed case, guessing clauses

may be added for generating candidate answer sets of P . For monotone external atoms, the candidates can be veri�ed by a �xpoint computation. For the general case, however, ef�cient checking methods are needed.

6 Conclusion and FurtherWork

HEX programs are a natural and powerful evolution of Answer-Set Programming (ASP), which ful�lls interoperability needs with other software and supports at the same time abstract problem modeling by higher-order features. These features are needed for a wide range of applications but missing in ASP systems today. In particular, user-de�ned libraries can be integrated, and thus customization to speci�c applications is enabled. Our further and ongoing work includes implementation beyond the working prototype, for which suitable algorithms and techniques are currently under development. This and the prototype will be discussed in detail elsewhere. Furthermore, an application in the context of an ongoing project for a personalized Web information system is targeted.