=Paper=
{{Paper
|id=None
|storemode=property
|title=Towards an Expressive Decidable Logical Action Theory
|pdfUrl=https://ceur-ws.org/Vol-846/paper_9.pdf
|volume=Vol-846
|dblpUrl=https://dblp.org/rec/conf/dlog/YehiaS12
}}
==Towards an Expressive Decidable Logical Action Theory==
https://ceur-ws.org/Vol-846/paper_9.pdf
Towards an Expressive Decidable Logical Action Theory
Wael Yehia1 and Mikhail Soutchanski2
1
Department of Computer Science and Engineering York University, 4700 Keele Street,
Toronto, ON, M3J 1P3, Canada
w2yehia@cse.yorku.ca
2
Department of Computer Science, Ryerson University, 245 Church Street, ENG281, Toronto,
ON, M5B 2K3, Canada mes@scs.ryerson.ca
Introduction
The projection problem is an important reasoning task in AI. It is a prerequisite to
solving other computational problems including planning and high-level program ex-
ecution. Informally, the projection problem consists in finding whether a given logical
formula is true in a state that results from a sequence of transitions, when knowledge
about an initial state is incomplete. In description logics (DLs) and earlier termino-
logical systems, this problem was formulated using roles to represent transitions and
concept expressions to represent states. This line of research as well as earlier applica-
tions of DLs to planning and plan recognition are discussed and reviewed in [5, 11] to
mention a few only. Using a somewhat related approach, the projection problem and a
solution to the related frame problem (i.e., how to provide a concise axiomatization of
non-effects of actions) have been explored using propositional dynamic logic, e.g., see
[10, 9]. These papers discuss relations with the propositional fragment of the situation
calculus and review previous work. A more recent work explores decidable combina-
tions of several modal logics, or combining description logics with a modal logic of
time or with a propositional dynamic logic [1, 23, 7]. The resulting logics are somewhat
limited in terms of expressivity because to guarantee the decidability of the satisfiability
problem in the combined logic, only atomic actions can be allowed. In applications, it
is sometimes convenient to consider actions with arbitrary many arguments.
On the other hand, there are several proposals regarding the integration of DLs and
reasoning about actions [19, 4, 17, 6, 13]. In [13], it is shown that the projection problem
is decidable in a proposed fragment of the situation calculus (SC). However, the logical
languages developed in these papers are not expressive enough to represent some of
the action theories popular in AI or to solve the projection problem in a general case.
For example, Gu& Soutchanski propose a DL based situation calculus [13], where the
projection problem is reduced to the satisfiability problem in ALCO(U), a DL that adds
nominals O and the universal (global) role U to the well known description logic ALC.
(The universal role is interpreted as the binary relation that links any two domain ele-
ments.) They consider Reiter’s basic action theories (BATs) [22], but impose syntactic
constraints on the formulas that can appear in axioms by concentrating on a subset
F ODL of FO2 formulas, where FO2 is a fragment of first order logic (FOL) with only
two variables. In the fragment of SC that they consider, action functions may have at
most two object arguments, the formulas in the precondition axioms (PA) and context
formulas in the successor state axioms (SSA) should be F ODL formulas (if the situa-
tion argument is suppressed), where F ODL formulas are those FO2 formulas, which
can be translated into a concept in ALCO(U) using the standard translation between DLs
and fragments of FOL. They illustrate their proposal with several realistic examples of
dynamic domains, but it turns out that some of the well-known examples, e.g., the Lo-
gistics domain from the first International Planning Competition (IPC) [20], cannot be
represented due to syntactic restrictions on the language they consider. Here and sub-
sequently, when we mention planning domain specifications, we consider them as FOL
theories without making the Domain Closure Assumption (DCA) common in planning,
i.e., without reducing them to purely propositional level. Later, [12] introduces a pos-
sible extension, where the syntactic restrictions on the class of formulas F ODL are
relaxed, but stipulates SSAs for dynamic roles (fluents with two object arguments and
one situational argument) to be context-free. She conjectures, but does not prove, that
the projection problem in her extension can be reduced to satisfiability in ALCO(U).
In our paper, we consider an even more expressive fragment of SC, called P, where
all SSAs can be context dependent with context conditions formulated in a language
L that includes F ODL as a proper fragment. Manual translations of planning specifi-
cations (from IPC) into our fragment P show that P has expressive power sufficient
to represent not only Blocks World and Logistics, but also many other domains. In
any case, reducing projection to satisfiability in ALCO(U) is justified by the fact that
there are several off-the-shelf OWL2 reasoners that can be employed to solve the latter
problem, since a DL SROIQ underlying the Web Ontology Language (OWL2) includes
ALCO(U) as a fragment [8]. In our paper, we concentrate on foundational work and ex-
plore the logical properties of P. Our paper contributes by formulating an expressive
fragment of SC where the projection problem is decidable without DCA and closed
world assumption (CWA), i.e., when an initial theory is incomplete and is not purely
propositional. We hope that research outlined in our paper will attract the description
logic community to interesting research issues on the boundary between DLs and rea-
soning about actions.
Definition of P
We assume that the reader is familiar with SC from [21, 22] and knows that a BAT
D = DAP ∪ DSS ∪ UNA ∪ DS0 ∪ Σ consists of the precondition axioms (PAs) DAP
that use the binary predicate symbol P oss, successor state axioms (SSAs) DSS , a set
of unique name axioms UNA, an initial theory DS0 that specifies an incomplete theory
of the initial situation S0 , and Σ - a set of domain independent foundational axioms
about the relation s1 s2 of precedence between situations s1 and s2 . In [22], axioms
Σ are formulated in second-order logic, all other axioms are formulated in FOL, so
we assume the usual definitions of sorts, terms, well-formed formulas, and so on. A
fluent is a predicate with the last argument s of sort situation. As usual, we say that
a situation calculus FOL formula ψ(s) is uniform in s, if s is the only situation term
mentioned in ψ(s), the formula ψ has no occurrences of the predicates P oss, ≺, and
has no quantifiers over variables of sort situation. The formula ψ obtained by deleting
all arguments s from fluents in the formula ψ(s) uniform in s is called the formula with
suppressed situation argument; the interested reader can find details in [21].
Fluents with a single object argument, F (x, s), are called dynamic concepts, and
fluents with two object arguments, F (x, y, s), are called dynamic roles. In the signature
of a BAT D, any predicate that is not a fluent must have either one or two arguments,
and is called either a (static) concept, or a (static) role, respectively. Subsequently, we
consider only BATs with relational fluents, and do not allow any other function symbols
except do(a, s) and action functions A(x). In particular, terms of sort object can be only
constants or variables. Each action function can have any number of object arguments.
To specify syntactic constraints on Dap and Dssa , we consider a language L, that
has at most n + 2 object variables x, y, z1 , . . . , zn , for some integer n > 0. We assume
L has at least n constants bi , 1 ≤ n ≤ n. The purpose of the variables zi is to serve as
place-holders to be instantiated with constants bi that occur as named object arguments
of ground action terms. This language L consists of two related sets of formulas: Fx and
Fy . Formulas φ(x) from the set Fx can have as free variables either x, or some of the
place-holder variables zi , 1 ≤ i ≤ n, but cannot have free occurrences of y. Formulas
φ(y) from the set Fy can have free occurrences of either y, or some of the place holders
zi , 1 ≤ i ≤ n, but cannot have free occurrences of x. Note the formulas φ may have free
variables zi that are not shown explicitly, but it will be always clear from the context
which variables are free in the formulas. We use the symbol e· to denote a bijection
between Fx and Fy . If φ(x) ∈ Fx , then φ(y) e is the dual formula of φ(x), obtained
by renaming in φ(x) every occurrence of x (both free and bound) with y and every
bound occurrence of y with x. Similarly, if φ(y) ∈ Fy , then φ(x) e is the dual formula
to φ(y) obtained by replacing every occurrence of y with variable x, and every bound
occurrence of x with y. The sets Fx and Fy have a non-empty intersection. For example,
sentences that mention constants only, and Fx formulas that have only occurrences of z
variables belong to both Fx and to Fy . Each formula φ without x, y variables is mapped
by bijection φe to itself. We are ready to give the following inductive definition.
Definition 1. Let L be the set of first-order logic formulas such that L = Fx ∪ Fy , and
e· be a bijection between formulas in Fx and Fy as defined above, where the sets Fy
and Fx are minimal sets constructed as follows. (We focus on Fx , since Fy is similar.)
1. > and ⊥ are in Fx .
2. If AC is a unary predicate symbol, z is a variable distinct from x and y, and b is a
constant, then the formulas AC(x), AC(z), and AC(b) are in Fx .
3. If b is a constant, and z is a variable that is distinct from x and y, then the formulas
x = x, x = b, x = z are in Fx .
4. If R is a binary predicate symbol, b1 and b2 are constants, and z1 and z2 are vari-
ables that are distinct from x and y, then R(z1 , z2 ), R(b1 , b2 ), R(b1 , z2 ), R(z1 , b2 ),
R(x, b2 ) and R(x, z2 ) are formulas in Fx .
5. If φ ∈ Fx , then also ¬φ ∈ Fx .
6. If φ, ψ ∈ Fx , then both (φ ∧ ψ) ∈ Fx and (φ ∨ ψ) ∈ Fx .
7. If φ(x) ∈ Fx , R is a binary predicate symbol, b is any constant, z is any variable
distinct from x and y, and φ(y)
e is the formula dual to φ(x), then all of the fol-
lowing formulas with quantifiers guarded by R belong to Fx : ∃y.R(x, y) ∧ φ(y), e
∃y.R(b, y) ∧ φ(y),
e ∃y.R(z, y) ∧ φ(y),
e as well as ∀y.R(x, y) ⊃ φ(y),e ∀y.R(b, y) ⊃
φ(y), ∀y.R(z, y) ⊃ φ(y).
e e
8. If φ ∈ Fx , φe is the formula dual to φ, then [∃x].φ(x), [∀x].φ(x) as well as
[∃y.]φ(y),
e [∀y.]φ(y)
e belong to Fx , where [∃] ([∀], respectively) means that quanti-
fiers are optional and applied only when a formula has a free variable.
The intuition behind the definition of L is that any variable z other than x and y has to be
x y
free in a formula from L. The set of formulas F ODL = F ODL ∪ F ODL defined in [13]
x y
is a proper subset of L because the set of formulas F ODL (F ODL , respectively) is a
x y
proper subset of F (F , respectively): no place holder variables z1 , . . . , zn are allowed
x y
in F ODL and F ODL . We say a formula φ ∈ L is a z-free L formula, if all occurrences
of variables z (if any), other than x and y, in φ are instantiated with constants.
Lemma 1. There are syntactic translations between the set of z-free formulas φ ∈
L and the concept expressions from the language ALCO(U) in both directions, i.e.,
they are equally expressive. Moreover, such translations lead to no more than a linear
increase in the size of the translated formula.
This lemma is proved using the standard translation between DLs and FOL; the
proof is similar to the proof of Lemma 1 in [13]. Using the fluents Loaded(box, s),
At(box, city, s), and In(box, vehicle, s) from Logistics as an example, after suppress-
ing s, a z-free L formula Loaded(B1 ) ∨ ∃x(Box(x) ∧ x 6= B1 ∧ In(x, T1 )) is trans-
lated as ∃U.({B1 } u Loaded) t ∃U.(Box u ¬{B1 } u ∃In.{T1 }, where {B1 }, {T1 }
are nominals (i.e., concepts interpreted as singleton sets), and ∀x(¬Box(x) ∨ x =
B1 ∨ At(x, T oronto)), all boxes distinct from B1 are in Toronto, is translated as
∀U.(¬Box t {B1 } t ∃At.{T oronto}). Notice why nominals and U are important.
Subsequently, we consider BATs that use in axioms L-like formulas uniform in s. This
motivates the following requirements. For brevity, let a vector x of object variables de-
note either x, or y, or hx, yi; also, let z denote a finite vector of place holder variables.
Action precondition axioms DAP : For each action function A(z), there is a single pre-
condition axiom uniform in s:
(∀z, s). P oss(A(z), s) ≡ ΠA (z, s), (1)
where ΠA (z, s) is uniform in s; it is an L formula with z as the only free variables,
if any, when s is suppressed. When object arguments of A(z) are instantiated with
constants, by Lemma 1, the RHS of each precondition axiom can be translated into a
concept in ALCO(U), when the situation variable s is suppressed.
Successor state axioms DSS : There is a single SSA 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 each axiom is as follows:
(∀x, s, a). F (x, do(a, s)) ≡ γF+ (x, a, s) ∨ F (x, s) ∧ ¬γF− (x, a, s) (2)
where each of the γF ’s are disjunctions either of the form
[∃z].a = A(u) ∧ φ(x, z, s), /* a set of variables z ⊆ u; may be {x} ∈ u */
if (2) is a SSA for a dynamic concept F (x, s) with a single object argument x, or
[∃z].a = A(u) ∧ φ(x, z, s) ∧ φ(y, z, s), /* z ⊆ u, possibly {x, y}∩u 6= Ø */
if (2) is a SSA for a dynamic role F (x, y, s), where φ(x, z, s) is a context condition
uniform in s saying when an action A can have an effect on the fluent F . The formula
φ(x, z, s) ∈ Fx , the formula φ(y, z, s) ∈ Fy , when s is suppressed. A set of variables
z in a context condition φ(x, z, s) must be a subset of object variables u. If u in an
action function A(u) does not include any z variable, then there is no ∃z quantifier.
If not all variables from x are included in u, then it is said that A(u) has a global
effect, since the fluent F experiences changes beyond the objects explicitly named in
A(u) (e.g., driving a truck between two locations changes location of all boxes loaded
in the truck). When a vector of object variables u contains both x and z, we say that the
action A(u) has a local effect. A BAT is called a local-effect BAT if all of its actions have
only local effects. Observe that in a local-effect SSA, when one substitutes a ground ac-
tion term A(bx , bz ) for a variable a in the formula [∃z].a = A(x, z)∧φ(x, z, s), apply-
ing UNA for action terms yields [∃z].x = bx ∧z = bz ∧φ(x, z, s), and applying ∃z(z =
b ∧ φ(z)) ≡ φ(b) repeatedly results in the equivalent formula x = bx ∧ φ(x, bz , s).
Initial Theory DS0 : The DS0 is an L sentence without z variables, i.e., it can be trans-
formed into an ALCO(U) concept.
A basic action theory D that satisfies all of the above requirements is called an
action theory P. We note that BATs proposed in [13] are less general than P, be-
cause their axioms should be written using formulas from F ODL , but F ODL is a
proper subset of L. Sometimes, for clarity, when we talk about P, we say that it is
an L-based BAT, in contrast to F ODL -based BATs considered in [13]. The Blocks
World is an example of a F ODL -based BAT, while Logistics is an example of P. Lo-
gistics cannot be formulated as a F ODL -based BAT because it includes actions, e.g.,
drive(T ruck, Loc1 , Loc2 , City), with more than 2 arguments, and the SSA for a dy-
namic role At(obj, loc, s) uses as a context condition an Fx formula, while in [13],
the SSAs for dynamic roles must be context-free. Subsequently, for brevity, instead of
saying that φ(s) is a SC formula uniform in s that becomes an L formula when s is
suppressed, we say simply that φ is an L formula.
Due to space limitations, we skip introduction to DLs, but the reader can find one in
[2]. Recall that the satisfiability problem of a concept and/or the consistency problem
of an ABox in the DL language ALCO(U) can be solved in E XP T IME.
Example 1. As an example of P, imagine searching for a given file in a depth-first
search (DFS) like manner through directories. An action f orward(z1 , z2 , z3 ) makes
forward transition from a current directory z1 to its child directory z2 while searching
for a file z3 . It is possible in situation s, if z2 has never been visited. This is represented
using the fluent vis(z2 , z3 , s). A backtrack(z1 , z2 , z3 ) transition from z1 back to its
parent z2 is possible only if all children of z1 had been visited while searching for a file
z3 . P also includes situation independent unary predicates f ile(x), dir(x), and the bi-
nary predicate dirChild(x, y) meaning that x is a direct child of y in a file system. The
search for a file f in a directory d succeeds when f ind(d, f ) is executed. This action is
possible when d actually contains f . This is represented using the fluent at(d, f, s). Us-
ing chmod(z1 , z2 ) one can toggle in situation s permissions of a directory z1 between
z2 = on and z2 = off , if the current permission x for this directory z1 , represented using
the fluent perm(z1 , x, s), is such that the values of x and z2 are opposite. The following
are precondition axioms (PA) for all actions (the variables zi , s are ∀-quantified at front).
P oss(f orward(z1 , z2 , z3 ), s) ≡ dir(z1 ) ∧ dir(z2 ) ∧ z1 6= z2 ∧ f ile(z3 )∧
dirChild(z2 , z1 ) ∧ ¬vis(z2 , z3 , s) ∧ at(z1 , z3 , s)
P oss(backtrack(z1 , z2 , z3 ), s) ≡ dir(z1 ) ∧ dir(z2 ) ∧ f ile(z3 ) ∧ dirChild(z1 , z2 )∧
at(z1 , z3 , s) ∧ ¬∃y ( dirChild(y, z1 ) ∧ dir(y) ∧ ¬vis(y, z3 , s) )
P oss(f ind(z1 , z2 ), s) ≡ f ile(z1 ) ∧ dir(z2 ) ∧ dirChild(z1 , z2 ) ∧ at(z2 , z1 , s)
P oss(chmod(z1 , z2 ), s) ≡ dir(z1 ) ∧ (z2 = on ∨ z2 = off )∧
∃x.(perm(z1 , x, s) ∧ x 6= z2 ).
The direct effects of actions are formulated using successor state axioms (SSA).
The current DFS for a file y arrives at a directory x when either forward or backtrack-
ing transition leads to x; otherwise, if any other action is executed, it remains at x. Also,
the directory x becomes visited as soon as DFS arrives there following some forward
transition, but only if the current permission of x is on in situation s. Otherwise, for-
ward transition has no effect. Changing permission of a directory x to y has an effect
only when DFS for a file is currently located at x in situation s. A file f is found after
doing f ind(x, z1 in a directory z1 only if permission is on for this directory in s.
at(x, y, do(a, s)) ≡ ∃z1 (a = f orward(z1 , x, y) ∧ perm(x, on, s)) ∨
∃z1 (a = backtrack(z1 , x, y)) ∨
at(x, y, s) ∧ ¬∃z1 (a = f orward(x, z1 , y) ∧ perm(z1 , on, s))∧
¬∃z1 (a = backtrack(x, z1 , y))
vis(x, y, do(a, s)) ≡ ∃z1 (a = f orward(z1 , x, y) ∧ perm(x, on, s)) ∨ vis(x, y, s)
perm(x, y, do(a, s)) ≡ a = chmod(x, y) ∧ ∃y(at(x, y, s) ∧ y = y ) ∨
perm(x, y, s) ∧ ¬∃z1 (a = chmod(x, z1 ) ∧ y 6= z1 ∧ ∃y.at(x, y, s) ∧ y = y )
f ound(x, do(a, s)) ≡ ∃z1 (a = f ind(x, z1 ) ∧ perm(z1 , on, s)) ∨ f ound(x, s).
These SSAs satisfy syntactic constraints in P, but they cannot be formulated as
F ODL -based SSAs considered in [13] since SSAs for the dynamic roles at and perm
have context conditions and mention action functions with more than 2 arguments.
Clearly, neither PAs, nor SSAs can be translated to a DL, but nevertheless, there are
instances of the projection problem in this BAT that can be reduced to SAT in a DL.
The Projection Problem in P
Let D be a description logic based BAT defined in [13], α1 , · · · , αn be a sequence of
ground action terms, and Goal(s) be a query formula uniform in s such that it can be
transformed into an ALCO(U) concept, if s is suppressed. Subsequently, we call a query
Goal(S) a regressable formula, if S is a ground situation term. One of the most impor-
tant reasoning tasks in the SC is the projection problem, that is, to determine whether
D |= Goal(do([α1 , · · · , αn ], S0 )). Another basic reasoning task is the executability
problem: whether all ground actions in α1 , · · · , αn can be consecutively executed. This
can be reduced to the projection problem using the precondition axioms, and for this
reason we no longer consider it. Planning and high-level program execution are two im-
portant settings where the executability and projection problems arise naturally. Regres-
sion is a central computational mechanism that forms the basis of automated solutions
to the executability and projection tasks in the SC [22]. A recursive definition of the
modified regression operator R on any regressable formula Goal(S) is given in [13].
The modified regression operator makes sure that the only two available object variables
x, y are re-used when regressing a quantified formula in contrast to Reiter’s regression,
where new variables are introduced. For a regressable formula Goal(S), we use no-
tation R[Goal(S)] to denote the regressed formula uniform in S0 that results from
replacing repeatedly fluent atoms about do(α, s) by logically equivalent expressions
about s as given by the RHS of SSAs, until such replacements no longer can be made;
this is why the regressed formula is uniform in S0 . For any static concept C(x) and role
R(x, y), by definition of regression R[C(x)] = C(x) and R[R(x, y)] = R(x, y).
The regression theorem (Theorem 8) proved in [13] shows that R[Goal(S)] is a
F ODL formula, when S0 is suppressed and, as a consequence, one can reduce the
projection problem for a regressable sentence Goal(S) to the satisfiability problem in
ALCO(U) as long as a BAT D satisfies syntactic restrictions due to using F ODL for-
mulas in axioms:
D |= Goal iff DS0 |= R[Goal(S)],
where it is assumed that DS0 includes UNA, unique name axioms for objects. (Unique
name axioms for actions are used by modified regression, and they are no longer re-
quired when regression terminates.) This statement is proved in [13] for an extended
BAT that additionally includes a set of axioms DT = DT,st ∪ DT,dyn , where the static
TBox DT,st is an acyclic set of concept definitions that mentions only situation inde-
pendent predicates (in [13], DS0 includes DT,st ), while dynamic TBox DT,dyn is an
acyclic set of definitions such that it has occurrences of fluents, but defined fluents are
mentioned only in the RHS of SSAs, and they are eliminated by the modified regression
operator using lazy unfolding. For example, DT,st may include situation independent
static definitions such as “vehicle is a truck or an airplane”, while DT,dyn may include
convenient situation dependent abbreviations like M ovable(x, s) ≡ Loaded(x, s) ∧
∃yIn(x, y, s). The previously mentioned acyclicity assumption originates in [4].
We would like to eliminate a previous assumption that DT,st is acyclic. For sim-
plicity, let us consider a case when DT,dyn = ∅. Let D be P such that its initial
theory DS0 is augmented with an arbitrary satisfiable static TBox DT,st that may in-
clude general concept inclusions between ALCO(U) concepts. (This TBox can be ex-
pressed as an ALCO(U) concept.) Then, by the relative satisfiability theorem from [21],
Σ ∪ Dap ∪ Dssa ∪ UNA ∪ DS0 ∪ DT,st is satisfiable iff UNA ∪ DS0 ∪ DT,st is sat-
isfiable, i.e., the presence of a static satisfiable ontology is harmless. Moreover, since
regression does not affect the predicates without a situation term, in other words, since
axioms in DT,st are invariant wrt the regression operator, it can be used to answer
“static” queries and to reduce the projection problem to the satisfiability in ALCO(U):
Σ ∪ Dap ∪ Dssa ∪ UNA ∪ DS0 ∪ DT,st |= Goal iff UNA ∪ DS0 ∪ DT,st |= Goal, when
Goal is an L sentence without z-variables that has no occurrences of fluents (a “static”
query), and UNA includes unique name axioms only for objects. This simple observa-
tion is a consequence of Lemma 1 and the regression theorem from [21]. In addition, in
P we can prove that formulas from L remain to be in L after regression.
Theorem 1. Let D be an L-based BAT (a theory P), φ be a regressable L formula, and
α a ground action. The result of regressing φ[(do(α, S0 )], denoted by R[φ(do(α, S0 )],
is a formula uniform in situation S0 that is an L-formula if S0 is suppressed.
This can be proved similarly to Lemma 2 from Section 5.4 in [13] that is proved for a
F ODL -based BAT. However, this does not follow directly from [13, 12] because SSA
for dynamic roles may have context conditions in P, but in [13, 12] it was assumed that
SSA for dynamic roles are context free. Also, recall that F ODL is a proper subset of
L. The proof is long and laborious because regression is a syntactic operation, and the
SSAs in P may have several different syntactic forms, but we have to show that if we
start with a DL-like formula, then after a single step of regression we get a formula that
remains DL-like. As a consequence, for the “dynamic” queries, we have the following.
Theorem 2. Let D = Σ∪Dap ∪Dssa ∪UNA∪DS0 ∪DT,st be P augmented with a (static)
general ALCO(U) TBox , φ(S) be a regressable z-free L sentence, and S be a ground
situation. Then the projection problem can be reduced to satisfiability in ALCO(U):
Σ ∪ Dap ∪ Dssa ∪ UNA ∪ DS0 ∪ DT,st |= φ(S) iff
UNA ∪ DS0 ∪ DT,st |= R[φ(S)]
This follows from Theorem 1 by induction on the length of the situation term S, from
Lemma 1, and from the fact that UNA ∪ DS0 ∪ DT,st can be transformed into an
ALCO(U) concept. This theorem is important because it shows that any static ALCO(U)
ontology can be seamlessly integrated with reasoning about actions in P. Also, one can
add an acyclic dynamic TBox DT,dyn to P without any difficulties, as in [13]. However,
[4, 17, 6] and others argue that a general dynamic TBox leads to serious difficulties.
While [4] does not consider a general static TBox DT,st , it could be added, e.g., by
internalizing DT,st into an ALCO(U) concept and including it as an ABox assertion wrt
a dummy individual. This trick was not considered in [4], because the universal role U
is required for this trick to work, but U was missing in [4].
Example 1 (cont.) We would like to adapt for our purposes an example of a general
TBox from the paper by Giuseppe De Giacomo, Maurizio Lenzerini “TBox and ABox
Reasoning in Expressive Description Logics”, KR 1996, pages 316-327). Suppose that
a static TBox has the following general concept inclusions:
dir v ∀dirChild− .(dir t f ile) u ≤ 1 dirChild.dir
f ile v ¬dir u ∀dirChild− .⊥
Let an initial DS0 be the following theory (written as L formula for brevity):
dir(home) ∧ dir(mes) ∧ dir(root) ∧ dir(wyehia) ∧ f ile(f 1) ∧ f ile(f 2)
dirChild(f 1, mes) ∧ dirChild(f 2, wyehia) ∧ dirChild(home, root)∧
dirChild(mes, home) ∧ dirChild(wyehia, home)∧
at(wyehia, f 1, S0 ) ∧ ∀x.(¬(dir(x) ∨ f ile(x)) ∨ perm(x, on, S0 ))
The UNA for object constants (represented as nominals in ALCO(U)):
{f 1} =
6 {f 2} = 6 {home} = 6 {mes} = 6 {off } =6 {on} = 6 {root} = 6 {wyehia}
Let the projection query be whether D ∪ TBox |= f ound(f 1, S), where S is
do([backtrack(wyehia, home, f1), f orward(home, mes, f1), f ind(f1, mes)], S0)).
Then, it is easy to see that the regressed query is
( (f 1 = f 1 ∧ perm(mes, on, S0)) ∨ f ound(f 1, S0) )
This example demonstrates that we managed to solve the projection problem in the
presence of a general expressive static TBox. This example has been implemented:
axioms are implemented in XML and regression of a query was computed using a C++
program, see details at http://www.scs.ryerson.ca/mes/dl2012.zip
Progression in P
In this section, we use the notion of forgetting about a sequence of ground atoms, the
notion of progression in SC, the fact about definability of progression in FOL for local
effect BATs, and notation introduced in [15, 16, 18]. Recall that P is any L-based BAT.
It is easy to give an example of P with global effect actions such that progression of
DS0 is not definable as a z-free L sentence. Subsequently, we consider only local-effect
P action theories, and we talk about z-free L sentences that can be transformed into
an ALCO(U) concept. Below, we prove that progression of a z-free L sentence DS0
is still expressible as a z-free L sentence DSα (here and subsequently, for brevity, we
talk about situation-suppressed sentences). This does not follow from Theorem 3.6 in
[18] about definability of progression in FOL for local-effect BATs, since our initial
theory DS0 is formulated in a strict subset of FO2 language, and it is not obvious at all
whether in P progression DSα of DS0 can still be defined within our language. Since
progression involves forgetting about old values of fluents and computing new values,
we need a couple of intermediate lemmas. First, we show that new fluent values can be
expressed in L. Then, we prove that the result of forgetting about ground fluents in DS0
affected by a ground action α remains to be a z-free L sentence.
Lemma 2. Let D be a local effect P, α a ground action, and Ω(S0 ) be the characteris-
tic set of α with respect to D. Then DSS [Ω] is a set of L sentences without occurrences
of z-variables, when the situation terms are suppressed.
The characteristic set Ω(S0 ) is a set of ground fluents affected by α. Because they
change values, we have to forget their old values. To compute new values for them,
we instantiate DSS w.r.t. Ω(S0 ), do simplification and obtain the set of sentences
F (t, Sα ) ≡ ΦF (t, α, S0 ), which are denoted as DSS [Ω], where Sα = do(α, S0 ), and
ΦF (t, α, S0 ) is a z-free L sentence representing the RHS of a SSA for the fluent F .
F (t, Sα ) and ΦF (t, α, S0 ) mention different situation terms. However, F (t, Sα ) can
never occur in ΦF or any RHS of SSA of other fluents because they are all uniform
in S0 . Also, none of the ground fluents to be subsequently forgotten are relevant to
F (t, Sα ) simply because it is the value of F in a different situation. Consequently, we
can replace F (t, Sα ) temporarily by some atom Ft until forgetting of Ω(S0 ) is com-
pleted, and then put it back while preserving logical equivalence. The next lemma shows
that forgetting about ground atoms Ω(S0 ) in an L formula results in an L formula.
Lemma 3. Let φ be a Fx (or Fy ) formula and θ a truth assignment to some of the
atoms P (tj ) occurring in this formula (if any), then φ[θ] remains a Fx (Fy ) formula.
Notation φ[θ] for forgetting about several ground atoms, introduced
Wm in [18], means the
result of replacing every occurrence of an atom P (x) in φ by j=1 (x = tj ∧θ[P (tj )])∨
Vm
( j=1 x 6= tj ) ∧ P (x). This Lemma is proved by induction over structure of φ.
Theorem 3. Let D be a local-effect BAT based on L and α a ground action. Let Ω(s)
be the characteristic set of α. Then the following formula is a progression of DS0 w.r.t.
α and this formula is an L sentence:
^ _ ^ ^
UNA ∧ ( DS0 ∧ DSS [Ω])[θ] (Sα /S0 ) (3)
θ∈M(Ω(S0 ))
Proof : This is a consequence of Lemmas (2), (3) and Theorem 3.6 from [18]. Note that
the final formula is uniform in Sα . This theorem is important for our work because it
shows for P that if an initial theory DS0 is expressible as an ALCO(U)-like concept,
then progression DSα is also expressible as an ALCO(U)-like concept.
Theorem 3 shows progression DSα can be translated to ALCO(U), but in a general
case, the size of progression can be much larger than the size of DS0 . If one wants to
solve the projection problem by computing progression for a sequence of action, then
one has to find special cases of an initial theory DS0 such that the size of progression
remains linear w.r.t. the size of DS0 . It turns out that progression is computationally
tractable if an initial DS0 is in proper+ form [18], where proper+ theories generalize
databases by allowing incomplete disjunctive knowledge about some of the named el-
ements of the domain [14]. A proper+ knowledge base (KB) is more general than a
proper KB, which is equivalent to a possibly infinite consistent set of ground literals.
We show that in P, if DS0 is a set of proper+ formulas that can be translated into
ALCO(U), i.e., a boolean ALC ABox , then progression of DS0 in our normal form can
be computed efficiently, and the normal form can be maintained without introducing
any new variables. To achieve this, we introduce a new p+ normal form. We show that
a KB in our p+ normal form can be equivalently transformed into the same normal form
after forgetting about old values of fluents, and none of the intermediate logical transfor-
mations require introducing new variables to preserve logical equivalence. The fact that
forgetting in our normal form KB can be accomplished without introducing new vari-
ables is novelty that does not follow from [18]. Also, we show that after progression the
size of the progressed KB is linear wrt to the size of of the initial KB, i.e., progression
can be computed efficiently. Once an initial theory DS0 has been progressed to DSα ,
solving the projection problem can be done using any ALCO(U) satisfiability solver.
Due to lack of space we omit all technical details, but the interested readers can find
them in the longer version at http://www.scs.ryerson.ca/mes/dl2012.zip
Discussion and Future Work
Main contributions of our paper are as follows. First, we define a logical theory P in-
tegrating reasoning about action with DLs such that P is more expressive than theories
from [12, 13]. Second, Theorem 2 (regression in P) shouldn’t be underestimated. It
shows existing ontologies (with a general ALCO(U) static TBox) can be seamlessly in-
tegrated with P when solving the projection problem. To the best of our knowledge, this
seamless integration of DLs and reasoning about actions has never been proposed be-
fore. For example, [4, 13] allowed only acyclic dynamic TBox (that can be easily added
to P too). Third, Theorem 3 is a new non-trivial statement that doesn’t follow from
[18]. It is important because it guarantees that progression of ALCO(U) KBs can still be
formulated in the same language, and consequently, one can continue computing pro-
gression for subsequent actions. Fourth, theorems (not included in this version) about
maintaining our new p+ normal form after forgetting are proved using new techniques.
They don’t follow from [18], where progression was studied in FOL.
An approach to integrating DLs and reasoning about actions proposed in [4] inspired
a number of subsequent papers including [13], where the reader can find extensive com-
parison and discussion. The approach proposed in [4] is expressive, and it can be used
to represent many popular AI action theories. However, one can answer only ground
projection queries using their approach, but Theorem 2 shows we can use regression to
answer projection queries with quantifiers over object arguments in fluents. Also, our
regression can be used to solve the projection problem in a BAT where some actions
have global effects, but the approach proposed in [4] can answer projection queries only
in local effect BATs. In any case, it is important to compare our implementations with
an implementation based on [4] for the common classes of queries and theories. The
first step in this direction is taken in [3]. Due to lack of space we couldn’t discuss other
related work, but all related publications are very extensively discussed in [4, 6, 13, 17].
References
1. Artale, A., Franconi, E.: A survey of temporal extensions of description logics. Ann. Math.
Artif. Intell. 30(1-4), 171–210 (2000)
2. Baader, F., Horrocks, I., Sattler, U.: Description logics. In: van Harmelen, F., Lifschitz, V.,
Porter, B. (eds.) Handbook of Knowledge Representation, pp. 135–179. Elsevier (2007)
3. Baader, F., Lippmann, M., Liu, H., Soutchanski, M., Yehia, W.: Experimental results on
solving the projection problem in action formalisms based on description logics. In: Proc. of
the 25th Intern. Workshop on Description Logics (2012)
4. Baader, F., Lutz, C., Miliĉić, M., Sattler, U., Wolter, F.: Integrating description logics and
action formalisms: First results. In: Proceedings of the 20th AAAI Conference. pp. 572–
577. Pittsburgh, PA, USA (2005), extended version is available as LTCS-Report-05-02 at
http://lat.inf.tu-dresden.de/research/reports.html
5. Badea, L.: Planning in description logics: Deduction versus satisfiability testing. In: Proc. of
the Intern. Workshop on Description Logics (1998)
6. Calvanese, D., De Giacomo, G., Lenzerini, M., Rosati, R.: Actions and programs over de-
scription logic ontologies. In: Proc. of the Intern. Workshop on Description Logics (2007)
7. Chang, L., Shi, Z., Qiu, L., Lin, F.: Dynamic description logic: Embracing actions into de-
scription logic. In: Proc. of the Intern. Workshop on Description Logics (2007)
8. Cuenca Grau, B., Horrocks, I., Motik, B., Parsia, B., Patel-Schneider, P.F., Sattler, U.: OWL
2: The next step for OWL. J. Web Sem. 6(4), 309–322 (2008)
9. De Giacomo, G., Iocchi, L., Nardi, D., Rosati, R.: A theory and implementation of cognitive
mobile robots. J. Log. Comput. 9(5), 759–785 (1999)
10. De Giacomo, G., Lenzerini, M.: PDL-based framework for reasoning about actions. In: Gori,
M., Soda, G. (eds.) AI*IA. Lecture Notes in Computer Science, vol. 992, pp. 103–114.
Springer (1995)
11. Devanbu, P.T., Litman, D.J.: Taxonomic plan reasoning. Artif. Intell. 84(1-2), 1–35 (1996)
12. Gu, Y.: Advanced Reasoning about Dynamical Systems. Ph.D. thesis, Department of Com-
puter Science, University of Toronto, Canada (2010)
13. Gu, Y., Soutchanski, M.: A description logic based situation calculus. Ann. Math. Artif.
Intell. 58(1-2), 3–83 (2010)
14. Lakemeyer, G., Levesque, H.J.: Evaluation-based reasoning with disjunctive information in
first-order knowledge bases. In: Proc. of KR-02. pp. 73–81 (2002)
15. Lin, F., Reiter, R.: Forget it! In: Proceedings of the AAAI Fall Symposium on Relevance. pp.
154–159 (1994)
16. Lin, F., Reiter, R.: How to progress a database. Artificial Intelligence 92, 131–167 (1997)
17. Liu, H., Lutz, C., Milii, M., Wolter, F.: Reasoning about actions using description logics with
general TBoxes. In: Logics in Artificial Intelligence, Lecture Notes in Computer Science,
vol. 4160, pp. 266–279. Springer Berlin / Heidelberg (2006)
18. Liu, Y., Lakemeyer, G.: On first-order definability and computability of progression for local-
effect actions and beyond. In: Boutilier, C. (ed.) IJCAI. pp. 860–866 (2009)
19. Lutz, C., Sattler, U.: A proposal for describing services with dls. In: Proc. of the 15th Intern.
Workshop on Description Logics (2002)
20. McDermott, D.V.: The 1998 AI planning systems competition. AI Magazine 21(2), 35–55
(2000)
21. Pirri, F., Reiter, R.: Some contributions to the metatheory of the situation calculus. Journal
of the ACM 46(3), 325–364 (1999)
22. Reiter, R.: Knowledge in Action: Logical Foundations for Describing and Implementing
Dynamical Systems. The MIT Press (2001)
23. Wolter, F., Zakharyaschev, M.: Dynamic description logics. In: Advances in Modal Logic.
pp. 431–446. CSLI Publications (1998)