Information Technology Reference
In-Depth Information
structure of the M-Tableau. If
)) is the root sequent of the M-
Tableau, the result of the mapping will be
n
S-Tableaux with roots
σ
=(
f
r
1
;:::;
r
n
g`
E
(
Φ
σ
i
=(
r
i
`
E
(
Φ
)) for
i
= 1
n
. Now we apply the rule that has been applied to the root M-sequent to each
individual root S-sequent as well, obtaining valid successor sequents in the S-Tableau.
Then the newly generated nodes are extended by applying the same rule as in the M-
Tableau. This process is repeated until the constructed tableau can not be extended
anymore.
Let
T
be an M-Tableau with root σ, as above, then Ψ
0
(
T
) is defined as the set of S-
Tableaux
:::
(
T
;
σ
;
σ
1
)
;:::;
Ψ(
T
;
σ
;
σ
n
)
g
,whereΨis defined along the graph structure
of
T
starting with the root sequent
f
Ψ
σ
, as defined below. Note that
Ψ
returns a single
S-Tableau while
Ψ
0
returns a set of S-Tableaux.
we map every instance of an M-Rule in the M-Tableau to an application
of the corresponding S-Rule in the S-Tableau using the fact that in an M-Tableaux every
node can be identified uniquely by its label. Let
To d efin e
Ψ
Φ
M
)) be an M-Sequent of
T
and σ
S
=(
s
`
E
(Φ
S
)) be an S-Sequent. Then Ψ(
T
;
σ
M
;
σ
S
) is only defined iff
s
2
S
and
σ
M
=(
S
`
E
(
Φ
M
.Nowlet
R
Λ
be the M-Rule that is applied in
T
to σ
M
:
Φ
=
Φ
S
=
`
S
E
(
Φ
)
R
Λ
:
S
1
`
E
(
Φ
1
)
S
k
`
E
(
Φ
k
)
By definition of the rules, if
Λ
2f
U
;
R
;
F
;
G
;^;_g
,then
R
Λ
is applicable to
σ
S
as an
S-Rule and yields:
s
`
E
(
Φ
)
R
Λ
:
`
`
s
E
(
Φ
1
)
s
E
(
Φ
k
)
In this case
s
2
S
=
S
1
=
=
S
k
and we continue our construction by expanding the
(
T
;
S
`
E
(Φ
i
)
;
s
`
E
(Φ
i
)) for
i
= 1
:::
k
.IfΛ=split, then
S-Sequent
s
`
E
(
Φ
i
) by
Ψ
2
there exists an
j
with
s
S
j
, since the partition covers
S
. Therefore we can apply the
S-Rule
R
split
on
σ
S
which yields a new node labeled with
σ
S
again. This new node is
(
T
;
S
j
`
E
(Φ)
;
σ
S
).
Regarding the rules for atomic propositions we only consider the positive case
R
A
+
.
The definition of
expanded by
Ψ
S
then we proceed as
above. Otherwise the construction of the S-Tableau is terminated with an unsuccessful
finite path and
Ψ
for
R
A
−
is similar. If
R
A
+
is applicable to
σ
(
T
;
σ
M
;
σ
S
) consists of a single node labeled with σ
S
. Finally con-
sider the
R
X
rule that involves the image operator. Let
T
= Img(
S
),
T
s
= Img(
Ψ
f
s
g
)=
f
t
1
;:::;
t
m
g
T
,
A
=(
Φ
1
:::;
Φ
l
),and
X
A
=(
X
Φ
1
;:::;
X
Φ
l
).
R
X
:
S
`
E
(
X
A
)
s
`
E
(
X
A
)
R
X
:
T
`
E
(
A
)
t
1
`
E
(
A
)
t
m
`
E
(
A
)
(
T
;
T
`
E
(
A
)
;
t
i
`
E
(
A
)).This
And again we expand the nodes labeled
t
i
`
E
(
A
) with
Ψ
simple recursive definition of
may result in an infinite S-Tableau. We can keep the
result finite if we exit the recursion by introducing a loop as soon as the same arguments
to
Ψ
occur the second time, as in the following example for mapping an M-Tableau into
its corresponding S-Tableaux.
Consider the Kripke structure
K
with two states 0 and 1, both initial states, and two
transitions from state 0 to state 1 and from state 1 to state 0. Both states are labeled with
Ψ
Search WWH ::
Custom Search