Information Technology Reference
In-Depth Information
ↆ
) can also be explained in terms of the second item of Proposition 1. Let
L
and
L
as above. By taking the contrapositive implication of Proposition 1.(ii) and
rewriting the diamond
Rule (
γ
γ
in terms of the dual [
], we obtain the following:
(
˃
:
ˁ
;
ˁ
˕
)(
˃
:
ʸ
¬ˈ
)
(
˃
ne
w
:
¬
[
ˁ
][
ˁ
]
¬˕
)(
˃
ne
w
:
[
ʸ
]
¬ˈ
)
ↆ
).
As before, there are two constraints on the construction of tableaus: A prefix gener-
ating rule is never applied twice to the same premise on the same branch; A formula
is never added to a tableau branch where it already occurs. The notions of
saturated
tableau
and
saturated branch
are as before. In order to deal with terms of the form
(
∩
) we can justify the rule (
By a procedure similar to the used for (
), the notion of closed branch is extended as follows: a branch of a tableau is
closed
when (1) it contains terms (
˃
:
L
×
˃
:
L
˕
)and(
˃
:
L
¬˕
)forsome
˃
,
L
and
˕
,or
(2) it contains (
; otherwise, the branch is called
open
. The notions of
closed
and
open tableau
are defined as before.
˃
:
×
)forsome
˃
4.1
Soundness
We start with the
∩
-semantics. As before, given a branch
ʘ
, Prefix(
ʘ
) denotes the set
ʘ
of all prefixes in
.
Definition 3.
Givenabranch
ʘ
and a MNM
M=
(
W
,˄,
V
)
,
ʘ
is
faithful
to
M
if there
is amapping f
: Prefix(
ʘ
)
ₒ
Wsuch that, for all
˃∈
Prefix(
ʘ
)
,
M
∩ˈ
1
;
···
;
∩ˈ
n
-
(
˃
:
ˈ
1
;
···
;
ˈ
n
˕
)
∈ʘ
implies
,
f
(
˃
)
|=˕
, and
M
∩ˈ
1
;
···
;
∩ˈ
n
's domain.
-
(
˃
:
ˈ
1
;
···
;
ˈ
n
×
)
∈ʘ
implies thatf
(
˃
)
is not in
Lemma 3.
Let
ʘ
be any branch of a tableau and
M=
(
W
,˄,
V
)
a MNM. If
ʘ
is faithful
ʘ
such
to
M
, and a tableau rule is applied to it, then it produces atleast oneextension
ʘ
is faithfulto
that
M
.
∩
). For the cases of rules (
Proof.
We only show the case for rule (
ₓ
), ([
·
]), (
×
Back
),
ˁ
n
.Let
L
≡ʸ
1
;
(
Back
), see Appendix A.3. Throughout this proof, let
L
≡ˁ
1
;
···
;
···
;
ʸ
m
∩
) of Table 2. Since (
in the rule (
˃
:
L
˕
)
,
(
˃
:
L
¬ˈ
)
∈ ʘ
,thereisan
f
s.t.
f
(
˃
)
∈ ˕
M
∩ˁ
1
;
···
;
∩ˁ
n
and
f
(
˃
)
ˈ
M
∩ʸ
1
;
···
;
∩ʸ
m
.Thus,
˕
M
∩ˁ
1
;
···
;
∩ˁ
n
ˈ
M
∩ʸ
1
;
···
;
∩ʸ
m
and hence, by Proposition 1,
[
ˁ
1
]
···
[
ˁ
n
]
˕
M
[
ʸ
1
]
···
[
ʸ
m
]
ˈ
M
:thereis
u
in
M
such
that
u
∈
[
ˁ
1
]
···
[
ˁ
n
]
˕
M
but
u
[
ʸ
1
]
···
[
ʸ
m
]
ˈ
M
. From the latter it follows that
u
M
∩ʸ
1
;
···
;
∩ʸ
m
survives the successive intersection updates of
ʸ
1
,
...
,
ʸ
n
but
,
u
|= ˈ
.From
M
∩ˁ
1
;
···
;
∩ˁ
n
;then
M
∩ˁ
1
;
···
;
∩ˁ
n
the former, suppose (1)
u
is in the domain of
,
u
|= ˕
and
ʘ
:
we can take
= ʘ∪{
(
˃
ne
w
:
L
˕
)
,
(
˃
ne
w
:
L
¬ˈ
)
}
and extend the original
f
into
f
: Prefix(
ʘ
)
W
by defining
f
(
M
∩ˁ
1
;
···
;
∩ˁ
n
ₒ
˃
ne
w
):
=
u
. It follows that
,
f
(
˃
ne
w
)
|=˕
M
∩ʸ
1
;
···
;
∩ʸ
m
ʘ
is faithfulto
and
,
f
(
˃
ne
w
)
|=ˈ
,andso
M
.Otherwise,(2)
u
is not in the
M
∩ˁ
1
;
···
;
∩ˁ
n
, an a similar argument shows that
ʘ
=ʘ∪{
domain of
(
˃
ne
w
:
L
×
)
,
(
˃
ne
w
:
L
¬ˈ
}
M
)
is faithfulto
.
Theorem 3.
Given any formula
˕
and any list L
≡ ˁ
1
;
···
;
ˁ
n
,ifthere is a closed
M
∩ˁ
1
;
···
;
∩ˁ
n
tableau for
(
˃
initial
:
L
¬˕
)
,then
˕
is valid in
for all MNMs
M
.
