On knowledge-based programming with sensing in the situation calculus.
We consider a class of knowledge-based Golog programs with sense actions. These programs refer explicitly to an agent's knowledge, and are designed to execute on-line, and under a dynamic closed-world assumption on knowledge. On-line execution of sense actions dynamically updates the background axioms with sentences asserting knowledge of the sense actions' outcomes. We formalize what all this might mean, and show that under suitable assumptions the knowledge modality in such programs can be implemented by provability. This leads to an on-line Golog interpreter for such programs, which we demonstrate on a knowledge-based program with sensing for the blocks world.
INTRODUCTION
Our concern will be with knowledge-based programs, specically, Golog programs
[Levesque et al. 1997] that appeal to knowledge and actions, including sense actions.
As an example, we consider the blocks world, and a program that explicitly refers to
an agent's knowledge, and to the sense actions she can perform to gain information
about the world. We imagine that initially the agent is positioned in front of a
table of blocks, with no prior knowledge about which blocks are where. The only
information she is given in advance is an enumeration of all the (nitely many)
blocks. Of course, the agent needs to know that this is a blocks world, so we
include suitable successor state and action precondition axioms. But the agent
denitely knows nothing about the initial conguration of blocks. For that matter,
neither do we, the program designers. Our program will allow the agent to gain the
information she needs, and to carry out the actions required to place all the blocks
onto the table:
Author's address: Department of Computer Science, University of Toronto, Toronto, Canada M5S
Permission to make digital/hard copy of all or part of this material without fee for personal
or classroom use provided that the copies are not made or distributed for prot or commercial
advantage, the ACM copyright/server notice, the title of the publication, and its date appear, and
notice is given that copying is by permission of the ACM, Inc. To copy otherwise, to republish,
to post on servers, or to redistribute to lists requires prior specic permission and/or a fee.
c
ACM 1529-3785/ c
ACM Transactions on Computational Logic, Vol. x, No.
proc allT oT able(b)
if :KWhether(clear(x)) then sense clear (x) endIf ;
if Knows(:clear(x)) then allT oT able(fxg [ b)
else if :KWhether(ontable(x)) then sense ontable (x) endIf ;
if Knows(ontable(x)) then allT oT able(fxg [ b)
else moveToT able(x) ; allT oT able(f g) endIf
endIf
This procedure appeals to Golog operators that should be intuitively clear, with the
possible exception of that for nondeterministic choice, ( x)(x), whose reading is
\Nondeterministically choose an x, and for that choice, do the program (x)." The
parameter b in allT oT able(b) stands for the set of those blocks that the agent has
considered, and rejected, as candidates for moving to the table since her previous
moveToT able action. The test action
prevents her from ever reconsidering
such a block. Thus, the initial call to this procedure is with allT oT able(f g). The
procedure assumes two knowledge-producing actions,
sense ontable (x) and sense clear (x);
whose action preconditions are always true. This program attempts to minimize
the number of sense actions the agent performs by rst checking that she doesn't
currently know the truth value of the sensed
uent. For example, the program
fragment if :KWhether(clear(x)) then sense clear (x) endIf instructs the agent
to sense whether x is clear only when she does not already know whether x is clear.
While on the face of it this program seems perfectly intuitive, there are a number
of technical problems lurking behind the scenes, particularly what it would take to
implement it:
(1) Knowledge and lack of knowledge. The background axiomatization must
characterize the agent's knowledge about the initial situation, and also her lack
of knowledge. So, for example, her ignorance about which blocks are where can
be represented by
Representing lack of knowledge can be problematic when an agent has complex
knowledge about the initial situation:
Assuming that the above characterizes all that the agent knows, what does the
agent not know in this example? Whatever that might be, it must somehow
be axiomatized because it does represent a truth about the agent's knowledge.
This is a very commonly occurring problem. We begin with a collection K of
axioms about what an agent does know, and we want to make a closed-world
assumption about knowledge to the eect that K captures everything that the
agent knows; any knowledge sentences not following logically from K are taken
On Knowledge-Based Programming with Sensing in the Situation Calculus  3
to be false. The problem here, of course, is to somehow capture this closed-world
assumption in a way that relieves the designer from having to gure out
the relevant lack of knowledge axioms when given what the agent does know.
(2) On-line execution. Because the program appeals to sense actions, it is designed
for on-line execution. This means that it must never backtrack over a
sense action; once such an action is performed, it cannot be undone. Knowledge-based
programs that invoke information-gathering actions must be carefully designed
to prevent execution traces that include sense actions but that eventually
lead to dead-ends. The above program has this property.
(3) Implementing sense actions. What should be done when such a program
encounters a sense action? The program is executing on-line, so that each action
in an execution trace is meant to be performed as it is generated during a
program run. Performing an ordinary action, like moveToT able(A), is unprob-
lematic; in a setting where the program is controlling a robot, the robot would
simply perform the action, and the action term would be added to the situation
history being constructed by the program interpreter. Performing a sense action
on-line is a dierent matter. Consider the robot receiving the on-line program
request sense clear (A) when the current action log is S. It will respond with one
of \yes" or \no", depending on the outcome of its sense action. If \yes" then the
robot now knows that A is clear: Knows(clear(A); do(sense clear (A); S)). If
\no" then Knows(:clear(A); do(sense clear (A); S)). Normally, neither of these
facts will be logical consequences of the underlying axioms; they provide new
information about the robot's world. Therefore, to provide an on-line implementation
of the sense action sense clear (A), dynamically add one of
do(sense clear (A); S));
do(sense clear (A); S));
to the background axioms, depending on the sense action's actual outcome.
knowledge-based Golog interpreter. For knowledge-based programs
like allT oT able above, we cannot depend on a conventional Golog interpreter
[Levesque et al. 1997], which relies on a closed initial database, and which,
in any case, would have to be augmented with the ability to reason about
knowledge.
For the above reasons, it is problematic to directly execute knowledge-based
programs like allT oT able using a closed-world Golog interpreter. The stance we
shall take here is to view such programs as specications for agent behaviours, and
seek an alternative representation for them that can be executed under standard
closed-world Golog.
2. FORMAL PRELIMINARIES
We rely on the description of the situation calculus of [Pirri and Reiter 1999], with
specic reference to the successor state axioms and action precondition axioms of
basic action theories, and we refer the reader to that paper for the details. We
rely also on the approach of [Scherl and Levesque 1993] for representing knowledge
and sensing actions in the situation calculus, and we assume that the reader is
familiar with their approach. We remind the reader that, following [Moore 1980;
4  Ray Reiter
1985], Scherl and Levesque introduce an accessibility relation K into the situation
calculus; the intended reading of K(s is that situation s 0 is accessible from
situation s. With the accessibility relation K in hand, one then denes knowledge
as an abbreviation:
Here,  is a situation-suppressed expression, and [s 0 ] is that situation calculus
formula obtained from  by restoring the situation argument s 0 to all predicate and
function symbols of  that take situation arguments.
2.1 Two Simplifying Assumptions
In the interest of simplifying the presentation of this paper, we shall make two
notationally undesirable but otherwise inessential assumptions about the underlying
language of the situation calculus:
(1) The language has no functional
uents, which are function symbols that take
situation arguments. Non
uent function symbols are permitted. To represent
a functional
uent, e.g., numberOfBlocksOnT able(s), the axiomatizer should
use a relational
uent, e.g., numberOfBlocksOnT able(n; s), and should en-
force, via its truth value in the initial database and via its successor state
axiom, that n must always exist and be unique.
(2) Except for the equality predicate, < and P oss, the language has no non
u-
ent predicate symbols. To represent such \eternal" relation, for example,
isP rimeNumber(n), the axiomatizer is required to use a relational
uent, e.g.,
isP rimeNumber(n; s), and to assign it the successor state axiom
isP rimeNumber(n; do(a; s))  isP rimeNumber(n; s):
Moreover, any assertion about isP rimeNumber(n) in the initial database must
be made in terms of isP rimeNumber(n; S 0 ).
2.2 Basic Action Theories with Knowledge and Sensing
Based on Scherl and Levesque's proposal, we can dene a basic action theory taking
the form
where,
(1)  consists of the following foundational axioms for the situation calculus with
knowledge:
Uniqueness of Situations
Subhistories
:s
Induction
On Knowledge-Based Programming with Sensing in the Situation Calculus  5
Here, we have introduced the abbreviation:
Any model of these axioms will consist of a forest of isomorphic trees, one
rooted at S 0 , the others rooted at the other initial situations in the model. All
these roots can serve in specifying a K relation over initial situations.
Accessible Initial Situations
(2) D ss is a set of successor state axioms including the following axiom for the
accessibility relation K:
(2)
Here, each sense action sense i (~x i associated with a condition
whose truth value in situation s the action is designed to de-
termine. Scherl and Levesque also treat read actions, whose purpose is to
determine the denotations of functional
uents, but since we are assuming no
functional
uents in our situation calculus language, we do not consider these.
It remains only to pin down the permissible syntactic forms that may take
in sense actions sense (~x).
Definition 2.1. (Objective situation-suppressed expressions).
(a) If F ( ~ t; ) is a relational
uent atom, then F ( ~ t) is an objective situation-
suppressed expression.
(b) If t 1 and t 2 are terms not of sort situation, then t is an objective
situation-suppressed expression.
(c) If  and are objective situation-suppressed expressions, so are :, _ ,
and (9v) , where v is not a situation variable.
Objective expressions are statements only about the world, not the agent's
mental state; they do not involve expressions of the form Knows(). An
objective situation-suppressed sentence is an objective situation-suppressed expression
In what follows, we shall simply say \ is
objective" in place of the long-winded \ is an objective situation-suppressed
sentence."
We require that every sense action sense (~x) be such that (~x) is an objective
situation-suppressed expression. So the idea is that an agent can sense objective
sentences|truths about the external world|but not, reasonably enough,
truths about his own knowledge.
The No Side-Eects Assumption for Sense Actions. For
uents other
than K, we suppose that they are provided with successor state axioms in the
usual way. But in the presence of sense actions, there is always the possibility
that such actions can aect these
uents, as in, for example
6  Ray Reiter
closeEyes:
However, we will not allow knowledge-producing actions to have such side-
eects on ordinary
uents; in the formal story we develop here, such actions
are only permitted to aect the K
uent. In other words, for each sense action
sense , and each relational
uent R, we require that R's successor state axiom,
together with the other background axioms, will entail
do(sense (~y); s))  R(~x; s):
This no side-eects condition is needed to obtain the above successor state
axiom for K. It also guarantees the intuitively necessary property that by
virtue of performing a knowledge-producing action, an agent will come to know
the outcome of that action. We shall make extensive use of this assumption in
what follows.
One might argue that the no side-eects assumption is unreasonable, that sense
actions often produce a change in the state of ordinary
uents, as in the above
senseF orObstacle example. The counter-argument is that indeed certain pre-conditions
(e.g., eyesOpen) may be necessary for sense actions to occur, but
then separate actions|not sense actions|should be provided by the axioms to
achieve these preconditions (e.g., openEyes). Then to perform a sense action,
one must rst perform the appropriate state-changing actions to establish that
sense action's preconditions. This is the perspective we adopt here.
(3) D ap is a set of action precondition axioms.
una is the set of unique-names axioms for actions.
(5) K Init is any set of initial accessibility axioms specifying the K relation in the
initial situation; these must have the property that, by virtue of the successor
state axiom for K, they will be true in all situations. In particular, using induc-
tion, this property can be shown to hold for the following standard accessibility
relations in initial situations.
(a) Re
exive in initial situations:
(b) Symmetric in initial situations:
(c) Transitive in initial situations:
(d) Euclidean in initial situations:
For example, with reference to the symmetry property, the following is a consequence
of the foundational axioms and the [Scherl and Levesque 1993] solution
to the frame problem for K:
(6) DS0 is a set of rst-order sentences describing the initial state of the world
being axiomatized. To pin these down, we need a couple of denitions.
On Knowledge-Based Programming with Sensing in the Situation Calculus  7
Definition 2.2. (Formulas about ). Let  be a term of sort situation. The
formulas about  are dened inductively:
(a) A relational
uent atom F ( ~ t; ) is a formula about .
(b) If t 1 and t 2 are terms not of sort situation, then t
.
(c) If  is an admissible situation-suppressed expression (dened below), then
Knows(;) is a formula about .
(d) If  and are formulas about , so are :,  _ , and (9v) , where v is
not a situation variable.
Definition 2.3. (Admissible situation-suppressed expressions). These are
inductively dened as follows:
(a) If F ( ~ t; ) is a relational
uent atom, then F ( ~ t) is an admissible situation-
suppressed expression.
(b) If t 1 and t 2 are terms not of sort situation, then t is an admissible
situation-suppressed expression.
(c) If  and are admissible situation-suppressed expressions, so are :, _ ,
Knows(), and (9v) , where v is not a situation variable.
Compare this with Denition 2.1 of the objective situation-suppressed expres-
sions. The objective expressions are always admissible, but unlike the former,
the latter are permitted to express properties of the agent's mental state, i.e.,
they may mention expressions of the form Knows().
We can now dene DS0 to be any set of sentences about S 0 .
Example 2.1. Here, we give the action precondition, and successor state axioms
for the blocks world that underlies the allT oT able knowledge-based program.
Action Precondition Axioms
Successor State Axioms
clear(x; do(a; s))
2.3 Satisability of Basic Action Theories with Knowledge
The main result about a basic action theory D with knowledge is the following:
Theorem 2.1. (Relative Satisability).
8  Ray Reiter
consists of any subset of the accessibility relations
Re
exive, Symmetric, Transitive, Euclidean, D is satisable
K Init is satisable.
Proof. Very much like the proof of relative satisability for basic action theories
without knowledge of [Pirri and Reiter 1999]. Essentially, one shows how a model
of DS0 [ D una [ K Init can be extended to a model of D. We omit the lengthy
details.
3. REDUCING KNOWLEDGE TO PROVABILITY FOR THE INITIAL SITUATION
The starting point for our implemention of knowledge-based programs is the observation
that, in a certain important special case, knowledge is reducible to provabil-
ity. Here, we describe what we mean by this, and we give suitable conditions under
which it will be true. Specically, we shall be concerned with characterizing entailments
of the form D terms of provability of knowledge-free
sentences.
First we need a simple consequence of the Relative Satisability Theorem 2.1:
Theorem 3.1. Suppose that Knows(;S 0 ) is a sentence about S 0 . Then,
consists of any subset of the accessibility relations
Re
exive, Symmetric, Transitive, Euclidean, then
Proof. D
that because :Knows(;S 0 ) is a syntactically legal sentence to include in an initial
database, then D[f:Knows(;S 0 )g is a basic action theory with knowledge whose
initial database is DS0 [ f:Knows(;S 0 )g. Now use Theorem 2.1.
Next, we introduce a special class of initial databases. Suppose the sentences of
DS0 are all of the form Knows( In
other words, the initial database consists exclusively of sentences declaring what
the agent knows about the world he inhabits, but there are no sentences declaring
what is actually true of the world, or what he knows about what he knows. So for
objective and since this
is logically equivalent to Knows( simply suppose that DS0
consists of a single sentence of the form Knows(;S 0 ); where  is objective, and
that is what we shall do from here on.
Lemma 3.1. Suppose that  is objective, that
objective, and that K init consists of any subset of the accessibility relations Re
exive,
Symmetric, Transitive, Euclidean. Then,
Proof. The ( direction follows from the fact that, because the axioms of D una
are situation independent, they are known in S 0 , and the fact that all logical consequences
of what is known are also known.
()). By Theorem 3.1, it is su-cient to prove:
On Knowledge-Based Programming with Sensing in the Situation Calculus  9
If
By hypothesis, K init [
Then it must continue to be so with K(s; s 0 ) taken to be . With this choice
for K, all sentences of K init become tautologies, Knows(;S 0 ) simplies to [S 0 ],
and :Knows(;S 0 ) simplies to :[S 0 ]. Therefore, D una [ f[S 0 ]; :[S 0 ]g is un-
satisable, and therefore, D una [ f[S 0
Therefore, for the initial situation, we have reduced the entailment problem for
knowledge sentences to that of knowledge-free sentences. This result relies on the
stated assumptions that:
(1) DS0 consists of a sentence of the form Knows(;S 0 ), where  is objective.
Therefore, the following would
not:
(2) The sentence to be proved has the form Knows(;S 0 ), where  is objective.
Lemma 3.1 gives us a provability story for entailments from D of the form
What about entailments of the form :Knows(;S 0 )? We defer
treating negative knowledge until Section 5 below, where we shall introduce the
closed-world assumption on knowledge, whose eect will be that entailments of
negative knowledge will reduce to non provability of knowledge-free sentences.
4. ON-LINE EXECUTION OF KNOWLEDGE-BASED PROGRAMS
As discussed earlier, we have in mind executing knowledge-based programs like
allT oT able on-line. This means that each time a program interpreter adds a new
program action to its action history, the robot also physically performs this action.
Some of these actions will be sense actions; since these normally increase the robot's
knowledge of its world, this means that its axioms must be augmented by knowledge
about the outcomes of its on-line sense actions. 1 To capture this idea formally, we
need some notation for describing this incrementally growing set of axioms. Initially,
before it has performed any actions on-line, the robot's background consists of a
basic action theory D, as dened in Section 2.2. Suppose that  is the current
situation recording all the actions performed on-line by the robot. We can suppose
that  mentions no variables, since it makes no sense to perform a non ground action
on-line. We want to dene the result of augmenting D with knowledge about the
outcomes of all the sense actions occurring in .
Definition 4.1. (Sense Outcome Function). A sense outcome function is any
mapping
from ground situation terms to sets of knowledge sentences, such that:
(1)
(2) If  is not a sense action,
1 In this respect, our work has much in common with prior approaches to on-line sensing, for
example, [Pirri and Finzi 1999; Lakemeyer 1999].
(3) If  is a sense action sense (~g);
do(sense (~g); ))g or
do(sense (~g); ))g:
In general, we shall be interested in D [
namely, the original basic action
theory D, augmented by knowledge about the outcomes of all sense actions in
the action history , according to the sense outcome
function
To analyze the
properties of this dynamically growing theory, we need the concept of regression.
4.1 Regression
Regression [Waldinger 1977; Pednault 1994; Pirri and Reiter 1999] is the principal
mechanism in the situation calculus for answering queries about hypothetical fu-
tures. The intuition underlying regression is this: Suppose we want to prove that
a sentence W is entailed by some basic action theory. Suppose further that W
mentions a relational
uent atom F ( ~ t; do(; )), where F 's successor state axiom
is F (~x; do(a; s))  F (~x; a; s). Then we can easily determine a logically equivalent
sentence W 0 by substituting F ( ~ t; ; ) for F ( ~ t; do(; )) in W . After doing so, the
uent atom F ( ~ t; do(; )), involving the complex situation term do(; ), has been
eliminated from W in favour of F ( ~ t; ; ), and this involves the simpler situation
term . In this sense, W 0 is \closer" to the initial situation S 0 than was W . More-
over, this operation can be repeated until the resulting goal formula mentions only
the situation term S 0 , after which, intuitively, it should be su-cient to establish
this resulting goal using only the sentences of the initial database. Regression is
a mechanism that repeatedly performs the above reduction starting with a goal
ultimately obtaining a logically equivalent goal W 0 whose only situation term
is S 0 . In [Pirri and Reiter 1999], the soundness and completeness of regression is
proved for basic action theories without knowledge and sensing actions. [Scherl and
Levesque 1993] denes regression for formulas involving knowledge, but we shall not
need that notion in this paper; our denition will be for knowledge-free formulas,
and is really a simpler version of that in [Pirri and Reiter 1999].
Definition 4.2. (The Regressable Formulas). A formula W is regressable wrt a
situation term  i:
(1) W is a
uent atom F ( ~ t; ), or an equality atom t are
not situation terms, or
(2) W has the form :W 1 or W 1 _W 2 or (9x)W 1 where x is not a situation variable,
and W 1 and W 2 are regressable wrt .
W is regressable i it is regressable wrt  for some ground situation term . 2
We can now dene the regression operator for regressable formulas.
Definition 4.3. (The Regression Operator). The regression operator R when
applied to a regressable formula W is determined relative to a basic theory of actions
This denition is less general than the denition of the regressable formulas given in [Pirri and
Reiter 1999]; it has the virtue of being simpler, and it will be su-cient for the purposes of this
paper.
On Knowledge-Based Programming with Sensing in the Situation Calculus  11
that serves as a background axiomatization. In what follows, ~ t is a tuple of terms,
is a ground term of sort action, and  is a ground term of sort situation.
(1) Suppose W is an atom. Since W is regressable, we have two possibilities:
(a) W is an equality atom between non situation terms, or W is a
uent atom
of the form F ( ~ t; S 0 ). In these cases,
(b) W is a relational
uent atom of the form F ( ~ t; do(; )). Let F 's successor
state axiom in D ss be
Without loss of generality, assume that all quantiers (if any) of F (~x; a; s)
have had their quantied variables renamed to be distinct from the free
variables (if any) of F ( ~ t; do(; )). Then
In other words, replace the atom F ( ~ t; do(; )) by a suitable instance of the
right-hand side of the equivalence in F 's successor state axiom, and regress
this formula. The above renaming of quantied variables of F (~x; a; s)
prevents any of these quantiers from capturing variables in the instance
(2) For the remaining cases, regression is dened inductively.
We shall also need to regress certain kinds of situation-suppressed expressions.
Definition 4.4. (Regression for situation-suppressed expressions). Recall that
when  is a situation-suppressed expression, and  a situation term, then [] is
that situation calculus formula obtained from  by restoring the situation argument
to every predicate of  that takes a situation argument. Let  be an objective
situation-suppressed expression. Therefore,  is the result of suppressing the situation
argument in some regressable formula of the situation calculus. Introduce a
\one-step" regression operator, R 1 (; ), whose role is to perform a single regression
step for  through the action  as follows: R 1 (; ) is that situation-suppressed
expression obtained from  by rst replacing all
uents in [do(; s)] with situation
argument do(; s) by the corresponding right-hand sides of their successor state
axioms (renaming quantied variables if necessary), and next, suppressing the situation
arguments in the resulting formula. Clearly, R 1 (; )[s] is logically equivalent
to [do(; s)] relative to the successor state axioms.
Finally, we dene the \multi step" regression operator on situation-suppressed
expressions. Let  be a ground situation term. R(; ) is the regression of the
situation-suppressed expression  through the actions of , dened by
We are here overloading the R notation. The one-argument version, R[W ] regresses
regressable formulas W of the situation calculus (to obtain a formula about S 0 ); the
two-argument version R(; ) regresses situation-suppressed expressions  through
the actions of . Clearly, R(; )[S 0 ] and R[[]] are logically equivalent, relative
to the background basic action theory.
4.2 Reducing Knowledge To Provability for On-Line Programs
Here, we focus on conditions under which the theory D [
consisting of the
original theory D augmented by the outcomes of all sense actions in , entails
sentences of the form Knows(;):
Lemma 4.1. Let (~x) be an objective, situation-suppressed expression. Then:
is not a sense action,
do(sense (~y); s))
Proof. First use the successor state axiom (2) for K. For 1, use the fact that,
when (~x) is an objective, situation-suppressed expression,
For 2, use the fact that, when (~x) is an objective, situation-suppressed expression,
do(sense (~y); s))  (~x; s)
by the no side-eects assumption for sense actions.
Corollary 4.1.
Proof. Take  to be in item 2 of Lemma 4.1.
Corollary 4.2. When K Init includes the re
exivity axiom,
Proof. Use Corollary 4.1, and the fact that when re
exivity holds in the initial
situation, it holds in all situations, so that what is known in s is true in s.
Lemma 4.2. When K Init includes the re
exivity axiom,
do(sense (~y); s))
do(sense (~y); s))  Knows( (~y)  (~x); s):
Proof. By item 2 of Lemma 4.1 and Corollary 4.2.
We shall need the following bit of notation:
Definition
4.5.
R ():
Suppose
is a sense outcome function, and  is a
ground situation term.
3 The notation  occurring in a sentence means that two sentences are being expressed: one in
which  is uniformly replaced by in the sentence, the other in which it is replaced by : .
On Knowledge-Based Programming with Sensing in the Situation Calculus  13
)g:
So, for example, if
then
Notice
that
R () is a situation-suppressed sentence. By
convention,
when
Lemma 4.3. If K Init includes the re
exivity axiom,
then
and
are logically equivalent, 4 relative to D. Recall that the
notation
stands
for the result of restoring situation argument S 0 back into the situation-suppressed
sentence
R ():
Proof. Corollary 4.2.
Lemma 4.4. Suppose  is objective,  is a ground situation term, and K Init
includes the re
exivity axiom. Then
Knows(
Proof. Induction on the number of actions in . When this is 0,  is S 0 , and
the result is immediate. For the inductive step, there are two cases:
Case 1. Suppose  is not a sense action. Then by item 1 of Lemma 4.1,
do(;
By induction hypothesis,
Knows(
The result now follows from the fact that when  is not a sense
action,
R (do(; )) and the fact that R(R 1 (;
Case 2.  is a sense action, say sense (~g). Without loss of generality, assume that
a sense outcome is (~g), so
by Lemma 4.2,
do(;
By induction hypothesis,
Knows(
The result now follows
because
R ()  R( (~g)  ; ) is the same
as
which is the same
as
R (do(;
Definition 4.6. (Deciding equality sentences). Suppose T is any situation calculus
theory. We say that T decides all equality sentences i for any sentence
over the language of T whose only predicate symbol is equality, T
4 We are slightly abusing terminology here; strictly speaking, we should say that the conjunction
of the sentences in
logically equivalent
to
R ()[S0 ].
14  Ray Reiter
The following is a purely technical lemma that we shall nd very useful in establishing
our principal results.
Lemma 4.5. Suppose that is objective, that D una [
decides all equality sentences, and K init consists of any subset of the accessibility
relations Re
exive, Symmetric, Transitive, Euclidean. Suppose further that
are objective, and that
Then for some 0  i  n; D
Proof. This takes a bit of proof theory. By hypothesis,
is unsatisable. Therefore, by item 2 of Theorem 2.1,
is unsatisable. Therefore, after expanding the Knows notation, we have that
is unsatisable. Therefore, after skolemizing the existentials, we get that
is unsatisable. It remains unsatisable if we take K(s; s 0 ) to be the complete graph
on
With this choice for K, all sentences of K init become tautologies, and we have that
must be unsatisable. Let
be a minimal subset of
such that
is unsatisable. If unsatisable, so by
Lemma 3.1, the result is immediate. Therefore, we can suppose that m  1. By
the above minimal subset property,
is satisable. By the Craig Interpolation Theorem, there exists a sentence I in the
intersection language of (3) and D una [f[m such that (3) [f:Ig and
are both unsatisable. But the intersection language
On Knowledge-Based Programming with Sensing in the Situation Calculus  15
consists of equality sentences only, 5 so I is such a sentence, and since D una [f[S 0
decides all such sentences, either D una [ f[S 0 I or D una [ f[S 0
latter case is impossible by the satisability of (3). We earlier concluded that
is unsatisable. It remains unsatisable when S 0 is
uniformly substituted for m , so that D una [
This, together with the fact that D una [ f[S 0 I implies the unsatisability of
]g. Therefore, by Lemma 3.1, D
Something like the assumption that D una [f[S 0 ]g decides all equality sentences
in the above lemma seems necessary. To see why, consider:
Example 4.1. Let F and G be unary
uents, and let  be the conjunction of
the following three sentences:
G:
Then it is easy to see that
but
Theorem 4.1. Suppose that  is objective,
objective, decides all equality sentences,  is a ground situation
term, and K Init includes the re
exivity axiom. Then
Proof. The (() direction follows from Lemmas 3.1 and 4.4.
For the ()) direction, suppose D [
Knows(
By Lemma 4.3,
f
Knows(
Therefore,
Knows(
By Lemma 4.5,
Knows(:
R
Knows(
If the latter is the case, we are done. Suppose the former. Then certainly,
Knows(:
i.e., D
Knows(
The result now follows from Lemma
3.1.
This is the central result of this section; it completely characterizes entailments of
the form Knows(;) relative to D [
in terms of provability, in the initial
5 Recall that we assume the underlying language of the situation calculus has no non
uent predicate
symbols and no functional
uents (Section 2.1).
situation, for knowledge-free sentences. What about entailments of sentences of the
form :Knows(;)? That is the topic of the next section.
5. THE DYNAMIC CLOSED-WORLD ASSUMPTION
We now consider the problem, discussed in item 1 of Section 1, of characterizing an
agent's lack of knowledge, and we begin rst by considering knowledge in the initial
situation we shall make the closed-world assumption
on knowledge, namely, that Knows(;S 0 ) characterizes everything that the agent
knows initially, and whatever knowledge does not follow from this will be taken
to be lack of knowledge. How can we characterize this closed-world assumption in
a way that relieves the axiomatizer from having to gure out the relevant lack of
knowledge axioms when given what the agent does know? We propose the following:
objective and D 6j= Knows(;S 0 )g:
Under the closed-world assumption on knowledge, the o-cial basic action theory
is taken to be closure(D). To make her life easier in specifying the initial database
of a basic action theory, we ask the axiomatizer only to provide a specication of
the positive initial knowledge DS0 that the robot has of its domain, but this is
understood to be a convenient shorthand for what holds initially, and closure(D),
as dened above, species the actual basic action theory.
Example 5.1. Here, we specify the positive initial knowledge available to the
agent inhabiting the blocks world of Example 2.1. While she knows nothing about
which blocks are where, this does not mean she knows nothing at all. There are state
constraints associated with this world, and we must suppose the agent knows these.
Specically, she must know that these constraints hold initially, and therefore, her
initial database consists of the following:
By making the closed-world assumption about this initial database, the axiomatizer
need not concern herself with writing additional lack of knowledge axioms like
does she have to worry about whether she has succeeded in expressing all the
relevant lack of knowledge axioms. The closed-world assumption takes care of
these problems for her.
However, as noted above, the axioms of D are being continuously augmented by
sentences asserting knowledge about the outcomes of the sense actions that have
been performed during the on-line execution of a program, and D [
species
what these axioms are, when the program is currently in situation . Therefore,
under the closed-world assumption in situation , we are supposing that D [
characterizes all of the agent's positive knowledge about the initial situation, so we
are actually interested in the closure of DS0 relative to D [
here we are
actually making a dynamic closed-world assumption.
Definition 5.1. Dynamic Closed-World Assumption on Knowledge.
On Knowledge-Based Programming with Sensing in the Situation Calculus  17
closure(D [
objective and D [
Under the dynamic closed-world assumption on knowledge, the o-cial basic action
theory, when the on-line execution of a program is in situation , is taken to be
closure(D [
)).
This closed-world assumption on knowledge is a metalevel account of a special
case of Levesque's logic of only knowing [Levesque 1990]. His results have been
considerably extended (to include an account of knowledge within the situation
calculus) in [Levesque and Lakemeyer 2001; Lakemeyer and Levesque 1998].
Next, we need to study the properties of closure(D [
)), with the ultimate
objective of reducing negative knowledge to non provability.
Lemma 5.1. Suppose that
decides all equality sentences, and K Init includes the re
exivity axiom, together
with any subset of the accessibility relations Symmetric, Transitive, Eu-
clidean. Then
closure(D [
Proof.
R ()[S 0 ]g is unsatisable. Then by Lemma 3.1,
Knows(:
R re
exivity, D
R ()[S 0 ]; and therefore, D [
f
R ()[S 0 ]g is unsatisable. Because, by Lemma
4.3,
and
are
logically equivalent (relative to D), D [
is unsatisable, and therefore, so is
closure(D [
is unsatisable. Therefore,
objective and D [
is unsatisable. Therefore, by Lemma 4.3,
f
objective and D [
is unsatisable. By item 2 of Theorem 2.1,
objective and D [
is unsatisable. By compactness, there is a nite, possibly empty subset of
objective and D [
say
such that
is unsatisable. Therefore,
f
is unsatisable, so
By Lemma 4.5, D
Knows(:
R
latter case is impossible, because for
fore, D
Knows(:
R
unsatisable.
Lemma 5.2. Suppose
decides all equality sentences,  is a ground situation term, and K Init includes the
re
exivity axiom. Suppose further that closure(D [
closure(D [
Proof. The (() direction follows from Theorem 4.1.
the result is immediate by Theorem 4.1. If
Knows(
R ()
R(;
Lemma 4.4, closure(D [
contradicting the hypothesis
that closure(D [
Definition 5.2. (Subjective Sentences). We say a sentence is a subjective sentence
about a ground situation term  i it has the form Knows(;), where  is
objective, or it has the form :W , where W is a subjective sentence about , or it
has the form W 1 _ W 2 , where W 1 and W 2 are subjective sentences about .
Lemma 5.3. Suppose K Init includes the re
exivity axiom. Then for any subjective
sentence W about a ground situation term ,
closure(D [
Proof. Induction on the syntactic form of W , using Lemma 4.4 to help prove
the base case.
We can now combine Lemmas 5.1, 5.2, and 5.3 to obtain our main result:
Theorem 5.1.
Let
be a sense outcome function. Suppose that
decides all equality sentences.
(3 )  is a ground situation term.
(4
(5 ) K Init consists of the re
exivity axiom, together with any subset of the accessibility
axioms Symmetric, Transitive, Euclidean.
Then,
closure(D [
is a subjective sentence about ,
closure(D [
(3 ) When W 1 and W 2 are subjective sentences about ,
closure(D [
closure(D [
On Knowledge-Based Programming with Sensing in the Situation Calculus  19
6. AN INTERPRETER FOR KNOWLEDGE-BASED PROGRAMS WITH SENSING
Under the stated conditions, Theorem 5.1 justies the following decisions in implementing
an interpreter for an on-line knowledge-based program.
(1) If the implementation uses [S 0 ] as its initial database.
(2) Whenever a sense (~g) action is performed by the program in a situation , the
implementation adds the regression of (~g; to the current initial
database, depending on the outcome of the sense action.
(3) Suppose a test condition W is evaluated by the program in a situation . Using
items 2 and 3 of Theorem 5.1, the implementation recursively breaks down
W [] into appropriate subgoals of proving, or failing to prove, sentences of the
form Knows(;). By item 1, these reduce to proving, or failing to prove,
the regression of [] relative to the current initial database. So for these base
cases, the implementation performs this regression step, then invokes a theorem
prover on the regressed sentence, using the current initial database (plus unique
names for actions) as premises. Notice the assumption here, required by the
theorem, that every test condition W of the program will be such that, at
evaluation time, W [] will be a subjective sentence about .
Guarded Sense Actions. Condition 4 of Theorem 5.1 requires that D una [
R ()[S 0 ]g be satisable. Therefore, an implementation must perform
this satisability test, and it must do so after each sense action. However, there
is one natural condition on a knowledge-based program that would eliminate
the need for such a test, and that is that every sensing action in the program
be guarded. By this, we mean that a sense action is performed only when
its outcome is not already known to the robot. In the allT oT able program,
the statement if :KWhether(clear(x)) then sense clear (x) endIf provides
such a guard for the sense clear action. Whenever the program guards all its
sense actions, as allT oT able does, then condition 4 of Theorem 5.1 reduces to
requiring the satisability of D una [ f[S 0 ]g, and this can be performed once
only, when the initial database is rst specied. This is the content of the
Proposition 6.1. Assume the conditions of Theorem 5.1. Assume further
that sense (~g) is a ground sense action, and that
closure(D [
Then
R (do(sense (~g); ))[S 0 ]g is satisable.
Proof. Without loss of generality, assume
that
a sense outcome is (~g),
so
do(sense
Therefore, by Lemma 4.4,
Knows(
Ray Reiter
Hence, by Lemma 3.1,
f
and therefore, D una [ f[S 0
must be satis-
able. The result now follows because :R(: (~g); )[S 0 ] is the same thing as
because
is
R (do(sense (~g); )):
7. COMPUTING CLOSED-WORLD KNOWLEDGE
The reduction of knowledge to provability under the closed-world assumption on
knowledge makes little computational sense for full rst-order logic, because its
provability relation is not computable. Therefore, in what follows, we shall restrict
ourselves to the quantier-free case. Specically, we shall assume:
(1) The only function symbols not of sort action or situation are constants.
(2) DS0 includes knowledge of unique names axioms for these constants:
(3) All quantiers mentioned in DS0 , and all quantiers mentioned in test expressions
of a knowledge-based program are typed, and these types are abbreviations
for descriptions of nite domains of constants:
where there will be one such abbreviation for each type  .
Therefore, typed quantiers can be eliminated in formulas in favour of conjunctions
and disjunctions, so we end up with sentences of propositional logic, for which the
provability relation is computable. Because the agent has knowledge of unique
names, D una [DS0 will decide all typed equality sentences. Therefore, the conditions
of Theorem 5.1 will hold.
8. PUTTING IT ALL TOGETHER
We have implemented an on-line Golog interpreter for knowledge-based programs
based on Theorem 5.1. It assumes that all sense actions in the program are guarded,
and it therefore does not perform the consistency check required by condition 4 of
Theorem 5.1. Here, we include the principal new features that need to be added to
a standard Golog interpreter [Reiter 2001] to obtain this knowledge-based program
interpreter.
A Golog Interpreter for Knowledge-Based Programs with Sense Actions Using
Provability to Implement Knowledge
% The clauses for do remain as for standard Golog, except that an extra clause is
% added to treat sense actions by interactively asking the user for the outcome of
% the action, and updating the initial database with the regression of this outcome.
This clause for sense actions appeals to a user-provided declaration
senseAction(A,SensedOutcome), meaning that A is a sense action, and SensedOutcome
% is the formula whose truth value the action A is designed to determine.
% restoreSitArgThroughout(W,S,F) means F is the result of restoring the situation
% argument S into every fluent mentioned by the formula W.
On Knowledge-Based Programming with Sensing in the Situation Calculus  21
queryUser(SensedOutcome,YN), restoreSitArgThroughout(SensedOutcome,S,Outcome),
regress(Outcome,R),
queryUser(SensedOutcome,YN) :- nl, write("Is "),
true now? y or n."), read(YN).
% Add the following clauses to those for holds in the standard Golog interpreter.
Implementing knowledge with provability .
holds(knows(W),S) :- restoreSitArgThroughout(W,S,F), prove(F).
In the above interpreter, two Prolog predicates were left unspecied:
(1) The theorem prover prove. Any complete propositional prover will do. We
use one that supposes the current initial database is a set of prime implicates.
There is no signicance to this choice; we simply happen to have had available
a prime implicate generating program. prove(F) rst regresses F, converts the
result to clausal form, then tests these clauses for subsumption against the
initial database of prime implicates.
(2) updateInitDatabase(R), whose purpose is to add the sentence R, which is the regression
of the outcome of a sense action, to the initial database. Because in our
implementation this is a database of prime implicates, updateInitDatabase(R)
converts R to clausal form, adds these to the initial database, and recomputes
the prime implicates of the resulting database.
Here is an execution of the allT oT able program, with a four block domain, using
this prover and the above Golog interpreter. 6
Running the Program for Four Blocks
[eclipse 2]: compile. % Compile the initial database to prime implicate form.
Clausal form completed. CPU time (sec): 0.06 Clauses: 34
Database compiled. CPU time (sec): 0.04 Prime implicates: 34
yes.
[eclipse 3]: run.
Is clear(a) true now? y or n. y.
Is ontable(a) true now? y or n. y.
Is clear(b) true now? y or n. n.
Is clear(c) true now? y or n. y.
Is ontable(c) true now? y or n. n.
6 All code needed to run this blocks world example is available, on request, from the author.
22  Ray Reiter
Performing moveToTable(c).
Is clear(b) true now? y or n. n.
Performing moveToTable(d).
Final situation: [senseClear(a), senseOnTable(a), senseClear(b), senseClear(c),
senseOnTable(c), moveToTable(c), senseClear(b), moveToTable(d)]
Notice how smart the program is: after learning that a is clear and need not be
moved, and after moving c to the table and learning that b is still not clear, it
gures that d must therefore be on b and that b must be on the table, so it simply
moves d.
9. DISCUSSION
The concept of knowledge-based programming was rst introduced in [Halpern and
Fagin 1989]. Chapter 7 of [Fagin et al. 1995] contains an extensive discussion, with
specic reference to the specication of communication protocols. Knowledge-based
programs play a prominent role in the literature on agent programming; see, for
example, [Shoham 1993].
The closed-world assumption on knowledge is also made in [de Giacomo et al.
1996], where they reduce the entailment problem for knowledge to entailment of
knowledge-free sentences. Their work diers from ours in two essential ways: theirs
is an epistemic description logic, and their epistemic modality is for the purposes
of planning, not knowledge-based programming.
This paper is a close relative of [Pirri and Finzi 1999]. There, Pirri and Finzi give
a mechanism for on-line execution of action sequences, with sense actions. Their
concept of sense actions and their outcomes is more sophisticated than ours, partly
because they allow for perceptions that may con
ict with an agent's theory of the
world, but in one special case|the so-called safe action sequences|their treatment
of a sense actions outcome is the same as ours: update the initial database with the
regression of this outcome. Their concept of safety also corresponds closely to our
notion of guarded sense actions. The basic dierences between us is that our action
theories are formulated with knowledge, while theirs are not, and we are interested
in the on-line execution of programs, not just action sequences. Nevertheless, it
seems that one way of viewing (some of) the results of this paper is as a specica-
tion of agent behaviours in terms of knowledge and the closed-world assumption,
for which the Pirri-Finzi account is a provably correct implementation. But this
possibility raises so many issues, they are best dealt with in future work.
10. POSTSCRIPT
It is particularly gratifying to be able to provide this paper in honour of Bob Kowal-
ski's 60th birthday because he has long been an advocate of metalevel reasoning,
especially for reasoning about modalities. So although Bob has not been a great fan
of the situation calculus, 7 I expect he would approve of my reduction to provability
7 But who knows, perhaps he has had a change of heart recently; turning does have certain
mellowing eects.
On Knowledge-Based Programming with Sensing in the Situation Calculus  23
of the knowledge modality. I do hope so, because this is my birthday gift to him,
and there is no exchange policy where it came from.



--R

Moving a robot: The KR&R approach at work.
Reasoning about Knowledge.
Modelling knowledge and action in distributed systems.
On sensing and
AOL: a logic of acting
All I know: A study in autoepistemic logic.
The Logic of Knowledge Bases.

Reasoning about knowledge and action.
A formal theory of knowledge and action.
ADL and the state-transition model of action
An approach to perception in theory of actions: Part 1.
http://www.
Some contributions to the metatheory of the situation calculus.
Journal of the ACM
Knowledge in Action: Logical Foundations for Specifying and Implementing Dynamical Systems.
The frame problem and knowledge producing actions.

Agent oriented programming.
Achieving several goals simultaneously.
--TR
All I know: a study in autoepistemic logic
Agent-oriented programming
Reasoning about knowledge
Some contributions to the metatheory of the situation calculus
The logic of knowledge bases
Knowlege in action

--CTR
Stefan Schiffer , Alexander Ferrein , Gerhard Lakemeyer, Football is coming home, Proceedings of the 2006 international symposium on Practical cognitive agents and robots, November 27-28, 2006, Perth, Australia
Michael Thielscher, FLUX: A logic programming method for reasoning agents, Theory and Practice of Logic Programming, v.5 n.4-5, p.533-565, July 2005
Sebastian Sardina , Giuseppe De Giacomo , Yves Lesprance , Hector J. Levesque, On the Semantics of Deliberation in Indigologfrom Theory to Implementation, Annals of Mathematics and Artificial Intelligence, v.41 n.2-4, p.259-299, August 2004
Richard B. Scherl , Hector J. Levesque, Knowledge, action, and the frame problem, Artificial Intelligence, v.144 n.1-2, p.1-39, March
Viviana Mascardi , Maurizio Martelli , Leon Sterling, Logic-based specification languages for intelligent software agents, Theory and Practice of Logic Programming, v.4 n.4, p.429-494, July 2004
situation calculus;situation calculus programming languages;dynamic closed-world assumption;theorem-proving;sensing and knowledge