On the Progression of Situation Calculus Basic Action Theories:
Resolving a 10-year-old Conjecture
Stavros Vassos and Hector J. Levesque
Department of Computer Science
University of Toronto
Toronto, ON, M5S 3G4, Canada
fstavros, hectorg@cs.toronto.edu
Abstract
In a seminal paper, Lin and Reiter introduced a model-
theoretic definition for the progression of the initial knowl-
edge base of a basic action theory. This definition comes
with a strong negative result, namely that for certain kinds of
action theories, first-order logic is not expressive enough to
correctly characterize this form of progression, and second-
order axioms are necessary. However, Lin and Reiter also
considered an alternative definition for progression which is
always first-order definable. They conjectured that this alter-
native definition is incorrect in the sense that the progressed
theory is too weak and may sometimes lose information. This
conjecture, and the status of first-order definable progression,
has remained open since then. In this paper we present two
significant results about this alternative definition of progres-
sion. First, we prove the Lin and Reiter conjecture by pre-
senting a case where the progressed theory indeed does lose
information. Second, we prove that the alternative definition
is nonetheless correct for reasoning about a large class of sen-
tences, including some that quantify over situations. In this
case the alternative definition is a preferred option due to its
simplicity and the fact that it is always first-order.
Introduction
The situation calculus is a logical language that is specially
designed for reasoning about action and change (McCarthy
& Hayes 1969). A basic action theory is a logical theory in
the situation calculus that describes what holds initially in
the world as well as how the world evolves under the effects
of actions. An example of a basic action theory is one that
captures the dynamics of a board game: part of the theory,
the initial knowledge base, describes the initial positions of
the pieces on the board, and the rest of the theory charac-
terize the legal moves of the game and the effects (and non-
effects) of performing those moves.
A fundamental problem in reasoning about action and
change is to determine whether or not some condition holds
after a given sequence of actions has been performed. In
other words, we start in an initial situation S0, we perform a
sequence of actions  taking us to a new situation S, and
we wish to know if the condition holds in S. There are in
fact two versions of this problem. The special case where
Copyright c
2008, Association for the Advancement of Artificial
Intelligence (www.aaai.org). All rights reserved.
the condition only refers to S is called the (simple) projec-
tion problem (Reiter 2001). For example, we might want to
know if a game piece is at a certain location after move .
The more general case is where the condition may refer to
situations in the future of S. For example, we might want
to know if a game piece can ever get to a certain location
after move . This sort of reasoning, which we will call
the generalized projection problem, is a prerequisite to other
forms of reasoning in dynamic domains such as planning
and high-level program execution (Reiter 1993).
The simple projection problem can be solved by regres-
sion or by progression (Lin 2007). Roughly speaking, re-
gression involves taking the condition about S and trans-
forming it to an equivalent one about S0 where we can use
the initial knowledge base to answer the question; progres-
sion, on the other hand, involves replacing the initial knowl-
edge base in the basic action theory by a new knowledge
base that captures the facts that hold in S.
For the generalized problem, where the condition may re-
fer to the future of S, the case is less clear. There is no re-
sult for evaluating such conditions based on regression, and
it is not clear if there is a practical definition for progression
that is logically correct for this reasoning task.
A model-theoretic definition of progression in the situa-
tion calculus that does the trick was first proposed by Lin and
Reiter (1997). However, their definition, which we call LR-
progression, comes with a strong negative result: for certain
kinds of basic action theories, first-order logic is not expres-
sive enough and second-order logic is needed. Nonetheless,
their result did not preclude the possibility of other forms of
progression that could still allow us to solve the generalized
problem while remaining first-order definable. In particular,
one possible candidate for the new knowledge base is the in-
finite set of all those first-order sentences about S that are
entailed by the original basic action theory. We will call this
second notion of progression FO-progression.
While FO-progression clearly captures what holds in S,
it is not clear that it is sufficient to characterize the future
of S, even in combination with the rest of the basic action
theory. Lin and Reiter conjectured that it was too weak. It
has been an open problem whether this conjecture is true or
false, rendering unclear also the question whether there can
be an alternative to LR-progression that solves the general-
ized problem and is first-order definable.
Proceedings of the Twenty-Third AAAI Conference on Artificial Intelligence (2008)
1004

This paper contains two major results. First of all, we
prove the Lin and Reiter conjecture: FO-progression is in-
deed too weak for characterizing the future of S. We pro-
vide a basic action theory and a sentence about the future
of S that demonstrate this. This result (Theorem 2) further
supports the claim by Lin and Reiter that the progression of
unrestricted basic action theories cannot be formalized cor-
rectly in first-order logic.
The second result is more positive. FO-progression was
shown by Lin and Reiter (1997) to be correct for the sim-
ple projection problem. Here we prove that it is also correct
for a much wider class of sentences including sentences of
the form “after , property  will always be true.” This re-
sult (Theorem 4) establishes that FO-progression is actually
more useful than was originally believed.
Situation calculus
The language L of the situation calculus (McCarthy &
Hayes 1969) is first-order with equality and many-sorted,
with sorts for actions, situations, and objects (everything
else). A situation represents a world history as a sequence
of actions. The constant S0 is used to denote the initial situ-
ation where no actions have occurred. Sequences of actions
are built using the function symbol do, such that do(a; s) de-
notes the successor situation resulting from performing ac-
tion a in situation s. A relational fluent is a predicate whose
last argument is a situation, and thus whose value can change
from situation to situation. For the scope of this paper we do
not allow the language to include functional fluents but we
note that they can be represented as relational fluents with
some extra axioms. Actions need not be executable in all
situations, and the predicate Poss(a; s) states that action a is
executable in situation s. The language L also includes the
binary predicate symbol @ which provides an ordering on
situations. The atom s@ s0 means that the action sequence
s0 can be obtained from the sequence s by performing one or
more actions in s. We will typically use the notation v0
as a macro for @0 _ =0.
Often we need to restrict our attention to sentences in L
that refer to a particular situation. For example, the initial
knowledge base is a finite set of sentences in L that do not
mention any situation terms except for S0. For this purpose,
for any situation term , we define L to be the subset of
L that does not mention any other situation terms except for
, does not mention Poss, and where  is not used by any
quantifier (Lin & Reiter 1997). When a formula () is in
L we say that it is uniform in  (Reiter 2001). Also, we
will use L2 to denote the second-order extension of L that
only allows predicate variables that take arguments of sort
object. L2 then denotes the second-order extension of L
by predicate variables with arguments of sort object.
We will use notation similar to (Gabaldon 2002) and
(Reiter 2001) to talk about sequences of actions and
situations that are rooted. Let  be a situation term
and  be a (possibly empty) sequence of action terms
h1; : : : ; ni. We use do(; ) to denote the situation
do(n; do(n1; : : : do(1; ) : : :)). We say that a situation
term  is rooted at 0 iff  is the term do(; 0) for some 
(in which case, 0 v  clearly holds). Finally, we will use
S to denote the situation term do(; S0).
We will also need to restrict our attention to sentences that
refer to  and the possible futures of . We say that  is in
the future of  in , where  is a rectified sentence in L, iff
  is , or
  is rooted at some  0 in the future of  in , or
  is a variable and 8( 0 v   ) or 9( 0 v  ^ )
appears in , where  0 is in the future of  in .
We define LF as the subset of L such that for any  2 L
F

the situation terms in  that appear as arguments of Poss or
some fluent or the equality predicate are all in the future of
 in . When a sentence  is in LF we say that  is about
the future of .
To see the intuition behind LF first note that the sentence
8s(Sv s  (s)) is in LFS and expresses that (s) holds
in all situations that are rooted at S. The recursion allows
the sentence 8s(S v s  (s) ^ 9s0(sv s0 ^ (s0)) and
sentences of this form to be in LFS as well. In general if a
sentence is in LF then its truth depends only on situations
that are in the future of .
Basic action theories
We will be dealing with a specific kind of L-theory, the so-
called basic action theories. The definition that follows is
the same as in (Reiter 2001) except that, similarly to (Lake-
meyer & Levesque 2004), Dap consists of a single action
precondition axiom for all actions instead of one separate
axiom for each action symbol. A basic action theory D has
the following form:1
D = Dap [ Dss [ Duna [ DS0 [ Dfnd
1. Dap contains a single precondition axiom for all actions
of the form Poss(a; s)  (a; s), where (a; s) is in Ls.
2. Dss is a set of successor state axioms (SSAs), one for
each fluent symbol F , of the form F (~x; do(a; s)) 
F (~x; a; s), where F (~x; a; s) is in Ls. SSAs charac-
terize the conditions under which the fluent has a specific
value at situation do(a; s) as a function of situation s.
3. Duna is the set of unique-names axioms for actions:
A(~x) 6=A0(~y), and A(~x)=A(~y)  ~x=~y, for each pair of
distinct action symbols A and A0.
4. DS0  LS0 describes the initial situation.
5. Dfnd is a set of domain independent foundational axioms
which formally define legal situations and @.
Regression
An important computational mechanism for reasoning about
actions is regression. A formula  is regressable iff the fol-
lowing conditions hold (Reiter 2001):2
1. every situation term in  is rooted at S0;
2.  does not quantify over situations;
1For the sake of readability we will be omitting the leading uni-
versal quantifiers.
2Unlike (Reiter 2001), here unrestricted Poss atoms are allowed
as a consequence of having a single axiom in Dap.
1005