Decidable Reasoning in a Modified Situation Calculus

1 Introduction

The situation calculus is a popular and well understood predicate logic language for reasoning about actions and their effects [Reiter, 2001]. It is used to provide a well-defined semantics for Web services and a foundation for a high-level programming language Golog [Reiter, 2001; McIlraith and Son, 2002]. However, because the situation calculus is formulated in a general predicate logic, reasoning about effects of sequences of actions is undecidable (unless some restrictions are imposed on the theory that axiomatizes the initial state of the world). The first motivation for our paper is intention to overcome this difficulty. We propose to use a two-variable fragment FO2 of the first-order logic (FOL) as a foundation for a modified situation calculus. Because the satisfiability problem in this fragment is known to be decidable (it is in NEXPTIME), we demonstrate that by reducing reasoning about effects of actions to reasoning in this fragment, one can always guarantee decidability. The second motivation for our paper comes from description logics. Description Logics (DLs) [Baader et al., 2003] are a well-known family

Mikhail Soutchanski

Department of Computer Science Ryerson University

245 Church Street, ENG281 Toronto, ON, M5B 2K3, Canada

Email: mes@scs.ryerson.ca

of knowledge representation formalisms, which play an important role in providing the formal foundations of several widely used Web ontology languages including OWL in the area of the Semantic Web. Many expressive DLs can be translated to FO2 and offer considerable expressive power going far beyond propositional logic, while ensuring that reasoning is decidable [Borgida, 1996]. DLs have been mostly used to describe static knowledge bases. However, several research groups consider formalization of actions using DLs or extensions of DLs. Following the key observation that reasoning about complex actions can be carried in a fragment of the propositional situation calculus, [Giacomo et al., 1999] give an epistemic extension of DLs to provide a framework for the representation of dynamic systems. However, the representation and reasoning about actions in this framework are strictly propositional, which reduces the representation power of this framework. In [Baader et al., 2005], Baader et al. provide another proposal for integrating description logics and action formalisms. They take the well known description logic ALCQIO (and its sub-languages) as foundation and show that the complexity of executability and projection problems (two basic reasoning problems for possibly sequentially composed actions) coincides with the complexity of standard DL reasoning. However, actions (services) are represented in their paper meta-theoretically, not as first-order (FO) terms. This can potentially lead to some complications when specifications of other reasoning tasks (e.g., planning) will be considered because it is not possible to quantify over actions in their framework. In our paper, we take a different approach and represent actions as FO terms, but achieve integration of taxonomic reasoning and reasoning about actions by restricting the syntax of the situation calculus and by introducing additional axioms to represent a taxonomy.

Because after doing longer and longer sequences of actions, solving projection problems becomes increasingly more difficult, it is beneficial to progress the initial incomplete knowledge base (KB) to represent the current state of the world. Then, the subsequent projection problems can be solved with respect to a new progressed KB. The task of computing a progressed KB is called the progression problem. Our paper is structured as follows. In Section 2, we briefly review the Reiter's situation calculus and the extension of FO2 with counting quantifiers. In Section 3 we discuss details of our proposal: a modified situation calculus. In Section

4 we consider an extension of regression (the main reasoning mechanism in the situation calculus). Finally, in Section 5 we discuss the progression problem and in Section 6 we discuss briefly other related approaches to reasoning about actions.

2 Background

The situation calculus (SC) Lsc is a predicate language for axiomatizing dynamic systems. All dialects of the SC Lsc include three disjoint sorts: actions, situations and objects. Actions are FO terms consisting of an action function symbol and its arguments. Actions change the world. Situations are FO terms which denote world histories. A distinguished constant S0 is used to denote the initial situation, and function do(a, s) denotes the situation that results from performing action a in situation s. Every situation corresponds uniquely to a sequence of actions. Objects are FO terms other than actions and situations that depend on the domain of application. Fluents are relations or functions whose values may vary from one situation to the next. Normally, a fluent is denoted by a predicate or function symbol whose last argument has the sort situation. For example, F(⃗x, do([α1, · · · , αn], S0)) represents a relational fluent in the situation do(αn, do(· · · , do(α1, S0) · · · ) resulting from execution of ground action terms α1, · · · , αn in S0. We do not consider functional fluents in this paper.

The SC includes the distinguished predicate Poss(a, s) to characterize actions a that are possible to execute in s. For any SC formula φ and a term s of sort situation, we say φ is a formula uniform in s iff it does not mention the predicates Poss, it does not quantify over variables of sort situation, it does not mention equality on situations, and whenever it mentions a term of sort situation in the situation argument position of a fluent, then that term is s (see [Reiter, 2001]). If φ(s) is a uniform formula and the situation argument is clear from the context, sometimes we suppress the situation argument and write this formula simply as φ, and also introduce a notation φ[s] to represent the SC formula obtained by restoring situation s back to all the fluents and/or Poss predicates (if any) in φ. It is obvious that φ[s] is uniform in s.

A basic action theory (BAT) D in the SC is a set of axioms written in Lsc with the following five classes of axioms to model actions and their effects [Reiter, 2001]: action precondition axioms Dap, successor state axioms (SSAs) Dss, initial theory DS0 , unique name axioms Duna, domain independent foundational axioms for situations Σ.

Suppose that D = Duna ∪ DS0 ∪ Dap ∪ Dss ∪ Σ is a BAT, α1, · · · , αn is a sequence of ground action terms, and G(s) is a uniform formula with one free variable s. One of the most important reasoning tasks in the SC is the projection problem, that is, to determine whether D |= G(do([α1, · · · , αn], S0)). Another basic reasoning task is the executability problem. Let executable(do([α1, · · · , αn], S0)) be an abbreviation of the formula Poss(α1, S0) ∧ ∧ni=2 Poss(αi, do([α1, · · · , αi-1], S0)). Then, the executability problem is to determine whether D |= executable(do([α1, · · · , αn], S0)). Planning and high-level program execution are two important settings where the executability and projection problems arise naturally. Regression is a central computational mechanism that forms the basis for automated solution to the executability and projection tasks in the SC [Reiter, 2001]. A recursive definition of the regression operator R on any regressable formula φ is given in [Reiter, 2001]. We use notation R[φ] to denote the formula that results from eliminating Poss atoms in favor of their definitions as given by action precondition axioms and replacing fluent atoms about do(α, s) by logically equivalent expressions about s as given by SSAs repeatedly until it cannot make such replacement any further. The formula G(do([α1, · · · , αn], S0)) is a particularly simple example of a regressable formula because it is uniform in do([α1, · · · , αn], S0)), but generally, regressable formulas can mention several different ground situation terms. The regression theorem shows that one can reduce the evaluation of a regressable formula φ to a FOL theorem proving task in the initial theory together with unique names axioms for actions: D |= φ iff DS0 ∪ Duna |= R[φ].

This fact is the key result for our paper: it demonstrates that an executability or a projection task can be reduced to a FOL theorem proving task. However, because DS0 is an arbitrary FO theory, this type of reasoning is undecidable. Two of the most common ways to overcome this difficulty is to introduce the closed world assumption or introduce the domain closure assumption (i.e., assume the domain is finite). In many application domains these assumptions are unrealistic. Therefore, we consider a version of the SC formulated in FO2 , or in C2 .

Two-variable FO logic FO2 is the fragment of ordinary FO logic (with equality), whose formulas only use no more than two variable symbols x and y (free or bound). Twovariable FO logic with counting C2 extends FO2 by allowing FO counting quantifiers ∃≥m and ∃≤m for all m ≥ 1. [Pacholski et al., 1997] show that satisfiability problem for C2 is decidable and recently [Pratt-Hartmann, 2005] proves that this problem is in NEXPTIME even when counting quantifiers are coded succinctly. See additional background on DLs and discussion of connections between DLs with C2 in [Baader et al., 2003; Borgida, 1996; Gu and Soutchanski, 2006].

3 Modeling Dynamic Systems in aModified Situation Calculus

In this section, we consider dynamic systems formulated in a modification of the language of the SC so that it can be considered as an extension to C2 (with an additional situation argument). 1 The key idea is to consider a syntactic modification of the SC such that the executability and projection problems are guaranteed to be decidable as a consequence of the decidability of the satisfiability problem in C2 . Moreover, since the modified SC has strong connections with description logics, which will be explained in detail below, we will denote this language as LDL sc .

First of all, the three sorts in LDL sc (i.e., actions, situations and objects) are the same as those in Lsc, except that they obey the following restrictions: (1) all terms of sort object are variables (x and y) or constants, i.e., object functional symbols are not allowed; (2) all action functions include no more than two arguments. Each argument of any term of sort action is either a constant or an object variable (x or y); (3) variable s of sort situation and/or variable a of sort action are the only additional variables being allowed in D-Σ-Duna in addition to variables x, y.

1 The reason that we call it a "modified" SC rather than a "restricted" SC is that we extend the SC with other features, such as adding acyclic TBox axioms to basic action theories.

Second, any fluent in LDL sc is a predicate either with two or with three arguments (including the one of sort situation). We call fluents with two arguments (dynamic) concepts, and call fluents with three arguments (dynamic) roles. In LDL sc , (static) concepts (i.e., unary predicates with no situation argument) and (static) roles (i.e., binary predicates with no situation argument), if any, are considered as unchangeable taxonomic properties and unchangeable classes of an application domain. Moreover, each concept (static or dynamic) can be either primitive or defined.

Third, apart from the standard FO logical symbols ∧, ∨ and ∃, with the usual definition of a full set of connectives and quantifiers, LDL sc also includes counting quantifiers ∃≥m and ∃≤m for all m ≥ 1. Equality = is allowed in LDL sc .

The dynamic systems we are dealing with here satisfy the open world assumption (OWA): what is not stated explicitly is currently unknown rather than false. In this paper, the dynamic systems we are interested in can be formalized as a basic action theory (BAT) D using the following seven groups of axioms in LDL sc : D = Σ ∪ Dap ∪ Dss ∪ DT ∪ DR ∪ Duna ∪ DS0 . Five of them (Σ,Dap,Dss,Duna,DS0 ) are similar to those groups in a BAT in Lsc, and the other two (DT ,DR) are introduced to axiomatize description logic related facts and properties (see below). However, because LDL sc allows only two object variables, all axioms must conform to the following additional requirements.

Action precondition axioms Dap: For each action A in LDL sc , there is one axiom of the form Poss(A, s) ≡ ΠA[s] (or Poss(A(x), s) ≡ ΠA(x)[s], or Poss(A(x, y), s) ≡ ΠA(x, y)[s], respectively), if A is an action constant (or unary, or binary action term, respectively), where ΠA (or ΠA(x), or ΠA(x, y), respectively) is a C2 formula with no free variables ( or with at most x, or with at most x, y as the only free variables, respectively). This set of axioms characterize the preconditions of all actions.

Successor state axioms Dss: There are two types of fluents in LDL sc : primitive dynamic concepts of the form F(x, s) (fluents with exactly one non-situation argument) and primitive dynamic roles of the form F(x, y, s) (fluents with exactly two non-situation arguments). Let variable vector ⃗x to be x, or y, or 〈x, y〉; a SSA is specified for each fluent F(⃗x, do(a, s)). According to the general syntactic form of the SSAs provided in [Reiter, 2001], without loss of generality, we can assume that the axiom has the form

where the general structure of ψF (⃗x, a, s) is as follows:

where each variable vector ⃗x(i,n,b) (or ⃗x(j,n,b) respectively) (i = 1..m0, j = 1..m1, n ∈ {0, 1}, b ∈ {+, -}) represents a vector of object variables, which can be empty, x, y, 〈x, y〉 or 〈y, x〉. Moreover, [∃x] or [∃y] represents that the quantifier included in [ ] is optional; and each φ+i (⃗x(i,1,+)), i = 1..m0 (φ-i (⃗x(j,1,-)), j = 1..m1, respectively), is a C2 formula with variables (both free and quantified) among x and y. Note that when m0 (or m1 respectively) is equal to 0, the corresponding disjunctive subformula is equivalent to false. Acyclic TBox axioms DT : Similar to the TBox axioms in DL, we may define new concepts using TBox axioms. Any group of TBox axioms DT may include two sub-classes: static TBox DT,st and dynamic TBox DT,dyn. Every formula in static TBox is a concept definition formula of the form

where G is a unary predicate symbol and φG(x) is a C2 formula in the domain with free variable x, and there is no fluent in it. Every formula in dynamic TBox is a concept definition formula of the form G(x, s) ≡ φG(x)[s],

where φG(x) is a C2 formula with free variable x, and there is at least one fluent in it. All the concepts appeared in the left-hand side of TBox axioms are called defined concepts. We also require that the set of TBox axioms must be acyclic (acyclicity in DT is defined exactly as it is defined for TBox ). RBox axioms DR: Similar to the idea of RBox in DL, we may also specify a group of axioms, called RBox axioms below, to support a role taxonomy. Each role inclusion axiom is represented as R1(x, y)[s] ⊃ R2(x, y)[s],

where R1 and R2 are primitive roles (either static or dynamic). If these axioms are included in the BAT D, then it is assumed that D is specified correctly in the sense that the meaning of any RBox axiom included in the theory is correctly compiled into SSAs. That is, one can prove by induction that (D - DR) |= ∀s.R1(x, y)[s] ⊃ R2(x, y)[s]. Although RBox axioms are not used by the regression operator, they are used for taxonomic reasoning in the initial theory.

Initial theory DS0 : It is a finite set of C2 sentences (assuming that we suppress the only situation term S0 in all fluents). It specifies the incomplete information about the initial problem state and also describes all the facts that are not changeable over time in the domain of an application. In particular, it includes static TBox axioms DT,st as well as RBox axioms in the initial situation S0 (if any). In addition, DS0 also includes all unique name axioms for object constants.

The remaining two classes (foundational axioms for situations Σ and unique name axioms for actions Duna) are the same as those in the BATs of the usual SC. Note that these axioms (as well as Dap and Dss) use more than two variables (e.g., Dss use action and situation variables in addition to object variables), but we will see in the next section, that these axioms will be eliminated in the process of regressing a regressable formula to a sentence that will use no more than two object variables and no other variables.

4 Modified Regression with Lazy Unfolding

After giving the definition of what the BAT in LDL sc is, we turn our attention to the reasoning tasks.

Given a formula W of LDL sc in the domain D, the definition of W being regressable (called LDL sc regressable below) is slightly different from the definition of W being regressable in Lsc (see [Reiter, 2001]) by adding the following two conditions: (i) any variable (free or bounded) in W is either x or y; (ii) every term of sort situation in W is ground. Moreover, inLDL sc we have to bemore careful with the definition of the regression operator R for two main reasons. First, to deal with TBox we have to extend regression. For a LDL sc regressable formula W, we extend below the regression operator defined in [Reiter, 2001] with the lazy unfolding technique (see [Baader et al., 2003]) to expand defined dynamic concepts. We still denote such operator as R. Second, LDL sc uses only two object variables and we have to make sure that after regressing a fluent atom we still get a LDL sc formula, i.e., that we never need to introduce new (free or bound) object variables. To deal with the two-variable restriction, we modify our regression operator R in comparison to the conventional operator defined in [Reiter, 2001]. For example, when replacing Poss atom or fluent atoms about do(α, σ), the definition of the conventional regression operator in [Reiter, 2001] has the assumption that the quantified variables in the right-hand side of the corresponding axioms should be renamed to new variables different from the free variables in the atoms that to be replaced. This assumption of using new variables for renaming assures equivalence of original formula and the formula after regression. To avoid introducing new variables (as required by the Reiter's regression operator) and to assure defined dynamic concepts being handled, we modify the regression operator for each LDL sc regressable formula. Possibility of reusing variables is guaranteed by the general format of the SSAs given in the previous section and the additional condition (ii) in the definition of the LDL sc regressable formula.

The complete formal definition of our R is as follows, where σ denotes the term of sort situation, and α denotes the term of sort action.

• If W is not atomic, i.e. W is of the form W1 ∨ W2, W1 ∧W2, ¬W ′ , Qv.W ′ where Q represents a quantifier (including counting quantifiers) and v represents a variable symbol, then

• Otherwise, W is atom. There are several cases.
• If W is of the form A1(⃗t) = A2(⃗t′ ) for some action function symbols A1 and A2, then by using axioms in Duna, 2 we define the regression of W as

Otherwise, if W is situation independent atom (including equality between object constants or variables), or W is a concept or role uniform in S0, then

1. If W is a regressable Poss atom, so it has the form

2 Notice that the action functions with different number of arguments always use different function symbols (i.e., different names).

Poss(A(⃗t), σ), for terms of sort action and situation respectively in LDL sc . Then there must be an action precondition axiom for A of the form Poss(A(⃗x), s) ≡ ΠA(⃗x, s), where the argument ⃗x of sort object can either be empty (i.e., A is an action constant), a single variable x or two-variable vector 〈x, y〉. Because of the syntactic restrictions of LDL sc , each term in ⃗t can only be a variable x, y or a constant C. Then,

˜

where C is a constant and φ denotes a dual formula for formula φ obtained by replacing every variable symbol x (free or quantified) with variable symbol y and replacing every variable symbol y (free or quantified) with variable symbol x in φ, i.e., ˜ φ = φ[x/y, y/x].

1. If W is a defined dynamic concept, so it has the form G(t, σ) for some object term t and situation term σ, and there must be a TBox axiom for G of the form G(x, s) ≡ φG(x, s). Because of the restrictions of the language LDL sc , term t can only be a variable x, y or a constant. Then, we use lazy unfolding technique as follows:

1. If W is a primitive concept (a primitive role, respectively), so it has the form F(t1, do(α, σ)) or F(t1, t2, do(α, σ)) for some terms t1 (and t2) of sort object, term α of sort action and term σ of sort situation. There must be a SSA for fluent F such as Eq. (1). Because of the restriction of the language LDL sc , the term t1 and t2 can only be a variable x, y or a constant C and α can only be an action function with no more than two arguments of sort object. Then, when W is a concept,

and, when W is a role,

Based on the above definition, we are able to prove the following theorems.

Theorem 1 Suppose W is a LDL sc regressable formula, then the regression R[W ] defined above terminates in a finite number of steps.

• Proof: Immediately follows from conditions (i) and (ii) of the definition of LDL sc regressable formula, acyclicity of the TBox axioms, and from the assumption that RBox axioms are compiled into the SSAs and consequently do not participate in regression. □

Theorem 2 Suppose W is a LDL sc regressable formula with the background basic action theory D. Then, R[W] is a LDL sc formula uniform in S0 with no more than two variables (x

Proof: According to the definition of the modified regression operator, prove by induction over the structure of W. The first statement holds because all replacements done by R transform W to logically equivalent formula. The second statement follows from the regression theorem in [Reiter, 2001]. □

Theorem 3 Suppose W is a LDL sc regressable formula with the background basic action theory D. Then, the problem whether D |= W is decidable.

Proof: According to Theorem 2, D |= W iff DS0 |= R[W], where R[W] and the axioms in DS0 are C2 formulas. Therefore, the problem whether D |= W is equivalent to whether DS0 ∧ ¬R[W] is unsatisfiable or not, which is a decidable problem, according to the fact that the satisfiability problem in C2 is decidable. □

This theorem is important because it guarantees that the projection and executability problems in LDL sc are decidable even if the initial KB DS0 is incomplete. [Gu and Soutchanski, 2006] give some detailed examples that illustrate the basic reasoning tasks described above and reduction techniques for dealing with properties that need more than two variables, and show that using LDL sc , one can model realistic dynamic domains such as school enrollment services and on-line shopping services.

We say that the SSA for a fluent F is context-free if the SSA for F has the form

Then, we have the following theorem about the complexity analysis for reasoning about projection problem.

Theorem 4 Given a basic action theory D in LDL sc , suppose that the SSA for a fluent F is context-free, then the computational complexity of answering the queries of the form F( ⃗X, σ) is co-NEXPTIME, where ⃗X is a vector of object constants and σ is a ground situation term.

Proof: The result follows from the complexity analysis of projection problem in [Reiter, 2001] (Chapter 4), Theorem 3, and the theorem in [Pratt-Hartmann, 2005] that the satisfiability problem in C2 is decidable in NEXPTIME. □

5 Progression of CNF-based KBs

The progression problem (also known as filtering and update) is how to compute the new theory in response to a given sequence of actions. In this section, we consider the progression problem for KBs in language LDL sc . In this section, let D = Dss ∪ Dap ∪ Σ ∪ Duna.

A formal definition of (classical) progression is given in [Reiter, 2001]. A set of sentences DSα is the (classical) progression of the initial KB DS0 (wrt basic action theory D) after performing a ground action α in the situation S0 iff DSα is uniform in do(α, S0), D |= DSα , and for every model Mα of D∪DSα , there is a model M of D such that M and Mα have the same domain and interpret situation independent predicates, function symbols, Poss and all fluents about the future of do(α, S0) identically (in the sequel, we say that M and Mα

have a progression relationship). The progression can be iteratively repeated if the progressed KB has the same format as the initial KB and we can consider the computed progression as the new initial KB at the next iteration. [Lin and Reiter, 1997] shows that the (classical) progression of a finite FO KB is not always FOL definable (but it is always definable in the second-order logic). By using an example similar to [Lin and Reiter, 1997], one can prove

Theorem 5 Progression of a theory in LDL sc is not always FO definable, therefore it is definitely not definable in LDL sc .

Proof: We consider the theory D1 obtained by modifying the theory D given in [Lin and Reiter, 1997] as follows: (1) replace one constant symbol 0 in D by an infinite set of constant symbols {0, 1, 2, · · · }; (2) replace function symbol succ(x) = y in D by predicate succ(x, y) which will be true iff y is the successor of x; (3) replace the empty initial KB by the new DS0 which includes infinitely many axioms of the form c1 ̸= c2 for any non-identical constant symbols c1 and c2 given above and of the form succ(c, c′ ) where constant c′ is the successor of constant c in the sense of natural numbers. The rest of the proof is exactly the same as the proof given in [Lin and Reiter, 1997]. □

Notice that the proof assumes that an LDL sc theory D1 is infinite. The problem whether progression of a finite theory in LDL sc is always FO definable remains open.

Now, we consider a (weaker than classical) modified progression for certain type of incomplete KBs only. For this special case of incomplete KBs, we show below that a modified progression of a KB is in LDL sc and it is sound wrt a classical progression of this KB.

First, we restrict the syntactic form of the KBs that are allowed. We use e to range over ewffs, that is, quantifier-free boolean formulas with equalities and inequalities only. For any vector ⃗x that is 〈x, y〉 (or a variable x, or y) and any vector of object constants ⃗B that is 〈B1, B2〉 (or a single constant B), we write ⃗x= ⃗B as an abbreviation for x=B1 ∧ y =B2 (or x=B, respectively). We use l(⃗x, S) to range over fluent literals, where S is a ground situation term. We call formulas of the form ∀⃗x.e(⃗x) ⊃ l(⃗x, S) equality-based formulas. We define a CNF-based KB DS =KBI ∪ KBS, where KBI is a set of situation-independent formulas (including unique name axioms for object constants, i.e., KBI is a subset of DS0 ), and KBS is a finite set of sentences uniform in S, where each sentence (also called clause below) is a disjunction of finitely many equality-based formulas. In particular, DS0 =KBI ∪KBS0 . A CNF formula composed from ground fluent literals uniform in S is a simple example of KBS.

Secondly, we consider an action theory D that is localeffect. Let a SSA of a fluent F have the syntactic form F (⃗x, do(a, s)) ≡ γ+ F (⃗x, a, s) ∨ F (⃗x, s) ∧ ¬γF (⃗x, a, s). This SSA is local-effect if γ+ F (⃗x, a, s) and γF (⃗x, a, s) are disjunctions of formulas of the form ∃⃗z[a = A(⃗y) ∧ φ(⃗y, s)], where A is a action function, ⃗y contains ⃗x, ⃗z = ⃗y - ⃗x, and φ is quantifier-free. An action theory D is local-effect if each SSA in D is local-effect. Let ∗ be + or -. Consider a ground action α and a fluent Fi in a local-effect action theory D of language LDL sc , then it is easy to see that the right-hand side (RHS) of SSA for Fi(⃗x, do(α, s)) has the following syntactic form: ∨m+i k=1 (⃗x= ⃗B+ ik ∧ φ+ik (s)) ∨ Fi(⃗x, s) ∧ ¬ ∨m-i k=1 (⃗x= ⃗Bik ∧ φ-ik (s)), where each m∗i is a natural number, the variables in ⃗x are among x and y, and for each k, φ∗ik (s) is a propositional formula. This SSA is a special case of the generic SSA (1) from Section 3. Moreover, according to Theorem 3 the problem whether D |= φ∗ik (S) is decidable for each k and any ground situation S. We define the following abbreviations.

When there is no disjunct satisfying the condition on the context formula φ∗ik , the corresponding disjunction is equivalent to ⊥. It is easy to see that all formulas above are ewffs.

The intuition behind these abbreviations is simple. For instance, Add(Fi, α, S) is a collection of all those cases when Fi will become true in every model if the context φ+ik (S) holds in S. Therefore, these cases provide support for adding the fluent Fi to the new KB. If one takes all those cases ⃗x = ⃗Bik when Fi ceases to be true in some models (where contexts might or might not be entailed) and removes from them those cases when negations of contexts are known to be entailed (i.e., remove models where it is guaranteed that Fi will not cease to be true), then as a result one gets Delete(Fi, α, S) that represents the collections of all those objects for which Fi has to be deleted from the current KB.

Now consider a ground action α and a CNF-based KB DS = KBI ∪ KBS as the current KB of a local-effect BAT D=D ∪DS. Assume that D |= Poss(α, S), otherwise there is no need in progression. We provide an algorithm to compute a variant of progression, called a modified progression of DS wrt D and the ground action α executed in S, and denote the resulting KB as P(α, DS).

Let P(α,DS) be the following set of sentences:

1. Initialize P(α,DS) to

KBI ∪

1. For each clause in KBS of the form Cj = p1 ∨ · · · ∨ ph ∨ · · · , where each ph is an equality-based formula (∀⃗x)ejh (⃗x) ⊃ ljh (⃗x, S) and ljh is either Fi or its negation ¬Fi, we update this clause as follows.
2. (a) Initialize a temporary set T = ∅.
3. (b) For each ph, if

• (c) If T ̸= ∅, add a new clause C ′j = Wp∈T p to P(α,DS); otherwise, do nothing (i.e., replace Cj with ⊤).

It is easy to see that the resulting KB P(α,DS) remains to be a CNF-based KB in LDL sc . Therefore, such progression can be repeated for the next ground action, say α′ .

The intuition behind this algorithm is simple. The successor model of the KB after performing a ground action at the current situation should keep all the situation-independent information, add truth values for each fluent for those objects where it will definitely become true (or false), and also keep the remaining consistent information by removing conflicting knowledge for objects from the current KB. Note that we detect conflicts between cases supported by ejh and cases included in the Delete(ljh , α, S) condition by using unique name axioms for constants in KBI, if necessary, to solve the entailment problem in (b).

For any given BAT D = D ∪ DS and a ground action α, we say that a modified progression P(α,DS) is (classically) sound if any model of the classical progression of DS (wrt α and D) is a model of the modified progression. Also, we say that P(α,DS) is (classically) complete if every model of D ∪ P(α,DS) is a model of the classical progression of DS (wrt α and D). The modified progression has the following nice properties.

Theorem 6 Given a BAT D with the current KB DS and a ground action α then

1. If D is consistent and RHS of SSAs are consistent, then the modified progression P(α, DS) is also consistent.
2. The modified progression P(α, DS) is (classically) sound.

Proof: (1) Prove by cases using the definition of P(α, DS). (2) According to the definition of P(α, DS), prove that D |= P(α,DS) using the RHS of the SSAs for Fi(⃗x, do(α, S)). Let Mα be any model of the (classical) progression of DS. Then, there is a model M of D such that M and Mα have a progression relationship. Then M is also a model of P(α,DS) by D |= P(α,DS), and then since M and Mα have a progression relationship we can prove that Mα is a model of any sentence uniform in do(α, S) iff M is a model of any sentence uniform in do(α, S). Therefore, we conclude that Mα is a model of P(α, DS) because P(α, DS) is a set of sentences uniform in do(α, S). □

6 Discussion and FutureWork

The major consequence of the results proved above for the problem of service composition is the following. If both atomic services and properties of the world that can be affected by these services have no more than two parameters, then we are guaranteed that even in the state of incomplete information about the world, one can always determine whether a sequentially composed service is executable and whether this composite service will achieve a desired effect. The previously proposed approaches made different assumptions: [McIlraith and Son, 2002] assumes that the complete information is available about the world when effects of a composite service are computed, and [Giacomo et al., 1999] considers the propositional fragment of the SC.

As we mentioned in Introduction, [McIlraith and Son, 2002] propose to use Golog for composition of Semantic Web services. It is surprisingly straightforward to define almost all Golog operators starting from our C2 based SC. The only restriction in comparison with the original Golog [Reiter, 2001] is that we cannot define the operator (πx)δ(x), non-deterministic choice of an action argument, because LDL sc regressable formulas cannot have occurrences of non-ground action terms in situation terms.

The recent paper [Baader et al., 2005] proposes integration of description logics ALCQIO (and its sub-languages) with an action formalism for reasoning about Web services. We discuss that paper in [Gu and Soutchanski, 2006].

An interesting paper [Liu and Levesque, 2005] aims to achieve computational tractability of solving projection and progression problems. The theory of the initial KB is assumed to be in the so-called proper form (i.e., conjunctions of equality-based formulas) and the query used in the projection problem is expected to be in a certain normal form. They consider a weaker type of progression defined for proper KBs with local effect actions only and show that their progression is sound (and sometimes complete) wrt the classical progression. We also consider local effect action theories, but our CNF-based KB is a set of disjunctions of equality-based formulas. However, [Liu and Levesque, 2005] considers a SC formulated in a general FOL (where the entailment problem is undecidable) and impose no restrictions on arity of fluents. Because of these significant differences in our approaches, it is not possible to compare them.

It is obvious that all cases from [Lin and Reiter, 1997; Shirazi and Amir, 2005; Liu and Levesque, 2005] when the progression is FOL definable also can be applied to our case simply because we restrict the language to two object variables only. However, we do the disjunctive case that nobody did before. Also, [Liu et al., 2006] considers update of an ABox in a DL following [Winslett, 1990] and also mentions that update can be applied to a boolean ABox formulated in C 2 , but their update is defined in terms of a conjunction of primitive fluent literals, i.e., it is different from our progression because our update is defined in terms of changes in the theory due to a ground action. [Giacomo et al., 2006] generalized the update approach of [Liu et al., 2006] fromALC to a more expressive DL language DL-Lite which allows general inclusion assertions in TBox , showed that the result of an update is always expressible by a DL-Lite ABox and provided a polynomial-time algorithm that computes the update over a DL-Lite KB.

The most important direction for future research is efficient implementation of practical scenarios of reasoning in LDL sc . Although in general, the worst-case computational complexity for the reasoning problems in LDL sc is high, some practical scenarios may facilitate empirically efficient solutions to the projection and executability problems. We are planning to consider also the progression problem for a more general class of incomplete KBs and conditions when the modified progressions is (classically) complete.

Acknowledgments

Thanks to the Natural Sciences and Engineering Research Council of Canada and to the Department of Computer Science of the University of Toronto for partial financial support.