Information Technology Reference
In-Depth Information
Based on these three sorts, to characterize ab action, they described the
precondition (under which the action could be performed) and the effect (the
change of the world after the execution of the action) by sentences of
LR
. In
LR
,
system with actions was treated uniformly as a logic theory that which was called
basic action theory. The
LR
framework and the corresponding basic action
theory provide a theoretical foundation for the study of actions.
Based on the
LR
framkwork, we present a many-sroted logic for the
representation and reasoning about actions (Tian, 1997). In this logic, actions are
treated as functions rather than individual sorts. Such a treatment is more
coincident with the intuitive understanding of actions and also has a clear
semantics in model theory. In the logic, the so-called minimal action theory is
introduced to characterize systems with actions; a model theory is
correspondingly established to analysis the progression in minimal action theory;
finally, some results on the definability of progression in minimal action theory
are presented.
2.10.1
Many-sorted logic for situation calculus
LR
is defined to be a many-sorted first order logic (Lin, 1994). In its signature
ќ
, there are three sorts: sort
s
for state, sort
o
for object and sort
a
for action.
The constant S
0
of sort
is used to denote the initial state. There is a
distinguished binary function
do
of type <
s
) denotes the successor
state to s resulting from performing the action a. The binary relation
Poss
of type
<
a, s; s
>; do(
a, s
) means that it is possible to perform the
action a in the state s. Finally, a binary relation < of type <
a, s
> is also introduced; Poss(
a, s
s, s
> is introduced to
denote the sequential relation between states.
A relation symbol is called to be state independent if all its parameters are of
sort
. A function symbol is called to be state independent if all of its parameters
as well as its function value are of sort
o
. A relation symbol is called to be a
fluent if there is a parameter of sort s while the other parameters are of sort o.
The number of state independent relations, state independent functions and
fluents are all supposed to be limit in
ќ
.
Term, atom formula, and formula of
LR
are defined in the usual way.
o
