Information Technology Reference
In-Depth Information
p
, the only atomic proposition. An M-Tableau for checking
EG
p
looks as follows
f
0
;
1
g`
E
(
G
p
)
0
1
p
f
0
;
1
g`
E
(
p
;
XG
p
)
p
f
0
;
1
g`
E
(
XG
p
)
and the application of
R
X
to the leaf sequent leads back to the root sequent. The tableau
represents one successful M-Path that contains only one image calculation. The given
M-Tableau is mapped into the following two S-Tableaux:
0
`
E
(
G
p
)
1
`
E
(
G
p
)
0
`
E
(
p
;
XG
p
)
1
`
E
(
p
;
XG
p
)
0
`
E
(
XG
p
)
1
`
E
(
XG
p
)
1
`
E
(
G
p
)
0
`
E
(
G
p
)
1
`
E
(
p
;
XG
p
)
0
`
E
(
p
;
XG
p
)
1
`
E
(
XG
p
)
0
`
E
(
XG
p
)
Again the application of
R
X
to the leaf nodes yields the root. In general, mapping an
M-Tableau may produce larger tableaux.
For each generated S-Tableau it is easy to construct a graph homomorphism
that
maps nodes and edges of the S-Tableau to the nodes, respectively edges, of the M-
Tableau, with the following property: If
λ
λ
(
n
S
)=
n
M
,where
n
S
is a node of the S-
`
Tableau, labeled with the S-Sequent
s
E
(
Φ
S
),and
n
M
is a node in the M-Tableau,
`
2
labeled with an M-Sequent
S
E
(
Φ
M
),then
s
S
and
Φ
M
=
Φ
S
. Further every edge,
that was generated by the application of an S-Rule
R
Λ
is mapped into an edge of the
M-Tableau that was generated by the M-Rule
R
Λ
.
Let
T
M
be an M-Tableau and
T
S
be an S-Tableau with
T
S
2
Ψ
0
(
T
M
).Thenwesay
that
T
S
matches
T
M
. We call an S-Path
x
a
matching path
to an M-Path
X
iff the S-
Tableau in which
x
occurs matches the M-Tableau of
X
and
λ
(
x
)=
X
for the corre-
sponding graph homomorphism
λ
.
Lemma 6.
Let X be a successful finite or cyclic M-Path in an M-Tableau
T
M
.Then
there exists an S-Tableau
T
S
that matches
T
M
and contains an successful S-Path x
matching X .
Proof.
First let
X
be a finite successful path. Then
X
ends with a sequent
S
`
E
()
with
S
6
fg
. We pick an arbitrary state
s
2
S
and traverse
X
backward until the root
is reached. At
X
(
i
) we generate the S-Sequent
x
(
i
) starting with
s
=
`
E
().
S
i
and the
following restriction. As long as no
R
X
rule is applied to
X
(
i
) we define the LHS of
x
(
i
)
to be the state on the LHS of
x
(
i
+ 1).If
R
X
is applied to
X
(
i
) then we define
s
i
as an
arbitrary predecessor of
s
i
+1
in
S
i
.
Second let
X
=
Y
Let
X
(
i
)=(
S
i
`
E
(
Φ
i
)), then we generate
x
(
i
)=(
s
i
`
E
(
Φ
i
)) with
s
i
2
Z
ω
be a cyclic successful path. The generated
x
will also be of
z
ω
,where
y
matches
Y
and
z
matches
Z
n
the form
x
=
y
for some
n
>
0. We start with
an arbitrary
s
1andtraverse
Z
backward until
Z
(0) is reached,
generating S-Sequents as in the finite case. After we have reached
Z
(0) we continue at
Z
(
m
). This process is repeated until the same S-Sequent was generated twice during the
2
Z
(
m
) where
m
=
j
Z
j−
Search WWH ::
Custom Search