Information Technology Reference
In-Depth Information
D
=
∪
D
ss
∪
D
ap
∪
D
una
∪
D
s0
(2.27)
where
(1)
is a set of logic formulas stating that the domain of sort
s
is a branching
temporal structure, with
S
0
the root and
do
the successive function. Formally it
contains the following axioms:
S
0
do(
a,s
)
do(
2
)
∀
P[(P(S
0
)
∧
∀
a
,
s
(P(
s
)
P(do(
a,s
))))
a
1
,s
1
) = do(
a
2
,s
2
)
(
a
1
=
a
2
∧
s
1
=
s
∀
s P(
s
)]
¬ (
s
< S
0
)
s
< do(
a,s
')
↔
(Poss(
a,s
')
∧
s
s
')
。
(2) D
ss
is a set of logic sentences expressing the effect after an action is
performed. Generally, each sentence is of the form
d
,do(
a,s
))
F
(
d
,
a,s
))
x
x
Poss(
a,s
)
(F(
(2.28)
Where F is a fluent and
F
is a logic formula in
ќ
s
。
(3) D
ap
is a set of logic sentences expressing the precondition under which an
action could be performed. Each sentence has the following general form
d
,
s
))
A
(
d
,
s
) (2.29)
x
x
Poss(A(
Where A is an action and
A
is a logic formula in
ќ
S
.
(4) D
una
is a set of logic formulas expressing that two actions performed on two
groups of objects will not have the same effect unless these two actions as well as
these two groups of objects are the same respectively. Generally, each pair of
formulas is of the following forms:
gd
)
d
)
A'(
x
y
A(
gd
)
(
gd
)
d
) = A(
d
=
x
y
x
y
A(
(5) D
S0
is a finite set of logic formulas in
ќ
S0
, and is called the initial condition of
the action theory.
