 |
Situation Calculus
|
Notes
from: Zohar Manna and Richard Waldinger, A Theory of Plans.
In M. P. Georgeff & A. L. Lansky (Eds.) Reasoning about Actions
and Plans. Los Altos, CA: Morgan Kaufman, 1987.Pp. 11-46.
In conventional Situation logic,
function and predicate symbols whose values might change, were
given state arguments...e.g. rather than clear(x) you have Clear(w,x)
where w is a state. In conventional sit. logic to construct a
plan that meets a specified convention you prove the condition
of the form Q[so,a,z] where so is the initial state, a the argument
of input parameter, and z the final state. Then the theorem to
be proved is:
|
| |
 |
|
|
A problem with the sit. logic
is that you can get nonexecutable plans because, for example,
it can put in conditions that specify a hypothetical state...i.e.
that is the state where the banana is in box a...but it doesn't
know if it is there or not...but it knows how to create a plan
if it were there...so they want to restrict to case where only
constructive plans (executable plans) can be proved.
Plan Theory
2 classes of expressions
Static or situational expressions to denote particular objects,
states, and truth-values.
E.g. hat'(s,b) the block that
is on top of b in state s, Clear(s,b) it is true that block b
is clear in state s , and put'(s,b,c) the state that results
from putting b on c from state s.
Corresponding fluent terms
which do not denote but will designate elements with respect
to a given state. E.g. hat(d), clear(d), and put(d,d') which
designate a block, truth-value, or state respectively with respect
to a given state (where d and d' themselves are fluent terms
that denote blocks)
Fluent terms do not refer to
any state explicitly...needs linkage operators for that....There
are three: s:e, s::e, or s;e where e designates an object, truth
value or state respectively. E.g., s:hat(d) s::clear(d), and
s;put(d,d')
Now the programs (plans) will
contain only fluent terms and in this way they restrict the knowledge
of the agent to the implicit current state...it will be unable
to tell what, say the hat of a given block is in a hypothetical
or future state.
Elements of Plan Theory
- the static (situational)
terms, s-terms, denote a particular element. They
include:
- object s-terms which denote an object such as a block
or a tablestate;
- s-terms, which denote a state;
- static sentences or s-sentences, denote a particular
truth value.
- the fluent terms or
f-terms, only designate an element with respect to
a given state. They include:
- object f-terms which designate an object with respect
to a given state;
- propositional f-terms which designate a truth-value with respect
to a given state;
- plan f-terms which designate a state with respect
to a given state.
The in Function ":"
If s is a state s-term and e
an object f-term, s:e is an object s-term denoting the object
designated by e in state s. In general, we introduce object f-function
symbols f(u1,...,un) and object s-function symbols f'(w,x1,...,xn)
together, where f takes object fluents u1,...,un as arguments
and yields an object fluent, while f' takes a state w and objects
x1,...,xn as arguments and yields an object. The two symbols
are linked in each case by the object linkage axiom:
|
| |
 |
|
|
Implicitly variables in axioms
are universally quantified and sort conditions are omitted for
simplicity (e.g., state(w))
E.g. corresponding to the object
f-function hat(u), which yields a block fluent, we have an object
s-function hat'(w,x) which yields a fixed block....the appropriate
instance of the object linkage axiom would be
w:hat(u) = hat'(w,w:u)
Thus, s:hat(d) denotes the block
on top of block s:d in state s
The in Relation "::"
If s is a state s-term and e
a propositional f-term s::e is a proposition denoting the truth
value designated by e in state s. E.g. so::clear(d) denotes the
truth-value designated by the propositional f-term clear(d) in
state so.
In general, introduce proposition
f-function symbols r(u1,...,un) and s-predicate symbols R(w,x1,...,xn)
together with the convention that r takes object fluents u1,...,un
as arguments and yields a propositional fluent, while R takes
a state w and objects x1,...,xn as arguments and yields a truth-value.
The two symbols are linked by the propositional linkage axiom:
|
| |
 |
|
|
E.g. w::clear(u) Clear(w,w:u)
The Execution Function ";"
If s is a state s-term and p
a plan f-term s;p is a state s-term denoting the state obtained
by executing plan p in state s.
In general, introduce plan f-function
symbols g(u1,...,un) and state s-function symbols g'(w,x1,...,xn)
together, where g takes object fluents u1,...,un as arguments
and yields a plan, while g' takes a state w and objects x1,...,xn
as arguments and yields a new state. The two symbols are linked
in each case by the plan linkage axiom:
|
| |
 |
|
|
E.g. corresponding to the plan
f-function put(u,v) which takes object fluents u and v as arguments
and produces a plan, we have a state s-function put'(w,x,y) which
takes a state w and actual objects x and y as args. and produces
a new state. The appropriate plan linkage axiom is
w;put(u,v) = put'(w, w:u, w:v)
The empty plan L is taken to
be a right identity under the execution function; that is
w; L = w for all state w.
Rigid Designator
An object f-constant u is a rigid
designator if w:u = u for all state w.
The Composition Function ";;"
If p1 and p2 are plan f-terms,
p1 ;; p2 is the composition of p1 and p2
Executing p1 ;; p2 is the same
as executing first p1 and then p2 . This is expressed by the
plan composition axiom:
|
| |
 |
|
|
for all states w and plans p1
and p2 .
Composition is associative, i.e.
(p1;; p2);; p3 = p1;;( p2;; p3)
and the identity plan is taken
to be the identity under composition.
E.G. Some Axioms expressed:
if notClear(w,y)
then On(w, hat'(w,y),y) (hat
axiom)
for all states w and blocks y.
In other words, if block y is not clear, its hat is directly
on top of it. (if y is clear, its hat is a "nonexistent"
object, not a block). It follows, if we take y to be w:v and
apply the propositional and object linkage axioms, that
if not(w::clear(v)
then w::on(hat(v),v)
for all states w and block fluents
v.
An action axiom example
if Clear(w,x)
then On(put'(w,x,table),x, table)
(put-table-on axiom)
for all states w and blocks x.
The axiom says that after a block has been put on the table the
block will indeed be on the table, provided that it was clear
beforehand. (The effects of attempting to move an unclear block
are not specified and therefore unpredictable.) It follows, if
we take x to be w:u and apply the linkage axioms plus the rigidity
of the designator table, that
if w::clear(u)
then On(w;put(u,table), w:u,
table)
for all states w and block fluents
u.
To construct a plan for achieving
a condition Q[so,a,z], we prove the theorem
|
| |
 |
|
|
|