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
execution. 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
terminological systems, this problem was formulated using roles to represent transitions and
concept expressions to represent states. This line of research as well as earlier
applications 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
combinations 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
elements.) 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
situation 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
Logistics domain from the first International Planning Competition (IPC) [
20
], cannot be
represented due to syntactic restrictions on the language they consider. Here and
subsequently, 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
possible 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
specifications (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
explore 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
reasoning 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) 2 Fx, then e(y) 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) 2 Fy, then e(x) 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
variables 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 2 Fx, then also : 2 Fx.
76.. IIff ;(x)22FFxx,,thRenisbaotbhin(ar^ypr)ed2icFatxe asnymdb(ol,_b is) a2nyFcxo.nstant, z is any variable
distinct from x and y, and e(y) is the formula dual to (x), then all of the
following formulas with quantifiers guarded by R belong to Fx: 9y:R(x; y) ^ e(y),
9y:R(b; y) ^ e(y), 9y:R(z; y) ^ e(y), as well as 8y:R(x; y) e(y), 8y:R(b; y)
e(y), 8y:R(z; y) e(y).
8. If 2 Fx, e is the formula dual to , then [9x]: (x), [8x]: (x) as well as
[9y:] e(y); [8y:] e(y) belong to Fx, where [
9
] ([
8
], respectively) means that
quantifiers 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
y
free in a formula from L. The set of formulas F ODL = F ODxL [ F ODL defined in [
13
]
is a proper subset of L because the set of formulas F ODxL (F ODyL, respectively) is a
proper subset of Fx (Fy, respectively): no place holder variables z1; : : : ; zn are allowed
in F ODxL and F ODyL. We say a formula 2 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 2
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
suppressing s, a z-free L formula Loaded(B1) _ 9x(Box(x) ^ x 6= B1 ^ In(x; T1)) is
translated as 9U:(fB1g u Loaded) t 9U:(Box u :fB1g u 9In:fT1g, where fB1g; fT1g
are nominals (i.e., concepts interpreted as singleton sets), and 8x(:Box(x) _ x =
B1 _ At(x; T oronto)), all boxes distinct from B1 are in Toronto, is translated as
8U:(:Box t fB1g t 9At:fT orontog). 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
denote 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
precondition axiom uniform in s:
(8z; s): P oss(A(z); s)
A(z; s);
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:
(1)
(2)
(8x; s; a): F (x; do(a; s))
F+(x; a; s) _ F (x; s) ^ : F (x; a; s)
where each of the F ’s are disjunctions either of the form
[9z]:a = A(u) ^ (x; z; s), /* a set of variables z u; may be fxg 2 u */
if (2) is a SSA for a dynamic concept F (x; s) with a single object argument x, or
[9z]:a = A(u) ^ (x; z; s) ^ (y; z; s), /* z u, possibly fx; yg\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) 2 Fx, the formula (y; z; s) 2 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 9z 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
action term A(bx; bz) for a variable a in the formula [9z]:a = A(x; z) ^ (x; z; s),
applying UNA for action terms yields [9z]:x = bx ^ z = bz ^ (x; z; s), and applying 9z(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
transformed 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,
because 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.
Logistics 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
dynamic 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 EXPTIME.
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
binary 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).
Using 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 8-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) ^ :9y ( 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 )^
9x:(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
backtracking 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,
forward 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)) 9z1(a = f orward(z1; x; y) ^ perm(x; on; s)) _
9z1(a = backtrack(z1; x; y)) _
at(x; y; s) ^ :9z1(a = f orward(x; z1; y) ^ perm(z1; on; s))^
:9z1(a = backtrack(x; z1; y))
vis(x; y; do(a; s)) 9z1(a = f orward(z1; x; y) ^ perm(x; on; s)) _ vis(x; y; s)
perm(x; y; do(a; s)) a = chmod(x; y) ^ 9y(at(x; y; s) ^ y = y ) _
perm(x; y; s) ^ :9z1(a = chmod(x; z1) ^ y 6= z1 ^ 9y:at(x; y; s) ^ y = y )
f ound(x; do(a; s)) 9z1(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
important reasoning tasks in the SC is the projection problem, that is, to determine whether
D j= 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
important settings where the executability and projection problems arise naturally.
Regression 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
notation 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
formulas in axioms:
D j= Goal iff DS0 j= 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
required 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
independent 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) ^
9yIn(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
simplicity, 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
include general concept inclusions between ALCO(U ) concepts. (This TBox can be
expressed 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
satisfiable, 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 j= Goal iff UNA [ DS0 [ DT;st j= 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
observation 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.
[ Dap [ Dssa [ UNA [ DS0 [ DT;st j=
UNA [ DS0 [ DT;st j= R[ (S)]
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 ):
(S) iff
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 8dirChild :(dir t f ile) u 1 dirChild:dir
f ile v :dir u 8dirChild :?
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) ^ 8x:(:(dir(x) _ f ile(x)) _ perm(x; on; S0))
The UNA for object constants (represented as nominals in ALCO(U )):
ff 1g 6= ff 2g 6= fhomeg 6= fmesg 6= foff g 6= fong 6= frootg 6= fwyehiag
Let the projection query be whether D [ TBox j= 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
characteristic 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
completed, 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 in [
18
], means the
result of replacing every occurrence of an atom P (x) in by Wjm=1(x = tj ^ [P (tj )])_
(Vjm=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)
2M( (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
elements 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
transformations require introducing new variables to preserve logical equivalence. The fact that
forgetting in our normal form KB can be accomplished without introducing new
variables 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