Information Technology Reference
In-Depth Information
Proof.
The claim follows from the previous propositions regarding correctness
of the various axioms in
FC
D
and from the fact that the right hand side
formulas of Equations (2.32) and (2.33) encode the appropriate transitive
closures.
Qed.
Example 2.9.1.
Let
D
be the ramication domain modeling the electric cir-
cuit consisting of two switches and a light bulb of Fig. 2.3 as in Example 2.2.2.
Then
FC
D
includes the axioms
Action
(
a; c; e
)
9x
[
a
=
toggle
(
x
)
^
(
c
=
:
up
(
x
)
^ e
=
up
(
x
)
_ c
=
up
(
x
)
^ e
=
:
up
(
x
))]
Acceptable
s
(
s
)
>
Acceptable
(
s
)
(
Holds
(
light
;s
)
Holds
(
up
(
s
1
)
;s
)
^ Holds
(
up
(
s
2
)
;s
))
Causal
s
(
`
"
;`
%
;s
)
?
Causal
(
`
"
;`
%
;s
)
`
"
=
up
(
s
1
)
^ `
%
=
light
^ Holds
(
up
(
s
2
)
;s
)
_ `
"
=
up
(
s
2
)
^ `
%
=
light
^ Holds
(
up
(
s
1
)
;s
)
_ `
"
=
:
(
s
1
)
^ `
%
=
:
light
_ `
"
=
:
up
(
s
2
)
^ `
%
=
:
light
We have already seen that
FC
D
entails the following.
9z
[
:
up
(
s
1
)
z
=
:
up
(
s
1
)
up
(
s
2
)
:
light
^ s
0
=
z
up
(
s
1
)]
It also entails
up
Causes
(
up
(
s
1
)
up
(
s
2
)
:
light
;
up
(
s
1
)
;
up
(
s
1
)
up
(
s
2
)
light
;
up
(
s
1
)
light
)
The latter implies
Ramify
(
up
(
s
1
)
up
(
s
2
)
:
light
;
up
(
s
1
)
;
up
(
s
1
)
up
(
s
2
)
light
)
according to axioms (2.32) and (2.33) and following the given denitions of
Causes
,
Acceptable
s
, and
Acceptable
. Consequently,
Successor
(
:
up
(
s
1
)
up
(
s
2
)
:
light
;
toggle
(
s
1
)
;
up
(
s
1
)
up
(
s
2
)
light
)
according to axiom (2.34).
2.9.3 Dening Transition Models
The Fluent Calculus-based axiomatization
FC
D
provides a formal account
of the notion of state transition including ramications. What remains to
be done is to formalize the application of whole action sequences to an (un-
specied) initial state in view of encoding observations. Our objective is to
extend axioms
FC
D
in such a way that there is a one-to-one correspondence
between the standard, i.e., `classical' models of the resulting axiomatization
and the models of a set of observations in the sense of our action theory.
