Information Technology Reference
In-Depth Information
M =
,˄,
Proof.
We show the contrapositive. Suppose that there is a
MNM
(
W
V
)and
w ∈
M
∩ˁ
1
;
···
;
∩ˁ
n
,w|= ˕
ʘ={
˃
initial
:
L
¬˕
}
a
W
such that
. Then the initial tableau
(
)
is
M
faithfulto
and hence, by Lemma 3, only faithfultableau to
MNM
will be produced.
A faithful branch cannot be closed. Hence (
˃
initial
:
L
¬˕
) can have no closed tableau.
Now, for the
ↆ
-semantics, we have the following.
Lemma 4.
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
.
ↆ
). Let
L
ˁ
n
and
L
≡ʸ
1
;
Proof.
We only show the case for the rule (
≡ˁ
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
. Then, there is
u
in
M
ʸ
1
···ʸ
m
ˈ
M
. From the former it fol-
lows that
u
survives the successive subset updates of
such that
u
∈ ˁ
1
···ˁ
n
˕
M
but
u
M
ↆˁ
1
;
···
;
ↆˁ
n
ˁ
1
, ...,
ˁ
n
and
,
u
|=˕
.
M
ↆʸ
1
;
···
;
ↆʸ
m
;then
M
ↆʸ
1
;
···
;
ↆʸ
m
From the latter, 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
;
···
;
ↆʸ
m
ₒ
˃
ne
w
):
=
u
. It follows that
,
f
(
˃
ne
w
)
|=ˈ
M
ↆˁ
1
;
···
;
ↆˁ
n
ʘ
is faithfulto
and
,
f
(
˃
ne
w
)
|= ˕
,andso
M
.Otherwise,(2)
u
is not in
M
ↆʸ
1
;
···
;
ↆʸ
m
, and a similar argument shows that
ʘ
:
the domain of
= ʘ∪{
(
˃
ne
w
:
L
×
)
,
(
˃
ne
w
:
L
˕
)
}
is faithfulto
M
.
Theorem 4.
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
.
4.2
Completeness
∩
L
PAL
∪{×,
}ₒN
We start with the
-semantics. Define the function len :
L
as
len(
×
):
=
1
,
len(
¬˕
):
=
len(
˕
)
+
1
,
len(
˕∧ˈ
):
=
len(
˕
)
+
len(
ˈ
)
+
1
,
len(
p
):
=
1
,
len(
˕
):
=
len(
˕
)
+
1
,
len([
˕
]
ˈ
):
=
len(
˕
)
+
len(
ˈ
)
+
1
,
len(
L
):
=
len(
˕
1
)
+···+
len(
˕
n
)
for
L
≡˕
1
;
···
;
˕
n
.
M
ʘ
=
(
W
ʘ
,˄
ʘ
,
V
ʘ
)
Lemma 5.
Givenanopen saturated branch
ʘ
,definethe model
asW
ʘ
:
)
,V
ʘ
(
p
):
W
ʘ
|
W
ʘ
,
=
Prefix(
ʘ
= {˃ ∈
(
˃
:
p
)
∈ ʘ}
and, for every
˃ ∈
∈˄
ʘ
(
X
˃
)
i
ff
there are
˕
andLsuch that
{˃
∈
W
ʘ
|
˃
:
L
×
˃
:
L
˕
(
˃
:
L
˕
)
∈ʘ
and
(
)
∈ʘ
or
(
)
∈ʘ}ↆ
X
.
Then,forall lists L
=ˁ
1
;
···
;
ˁ
n
and all formulas
˕
,
M
ʘ
)
∩ˁ
1
;
···∩ˁ
n
(i) (
˃
:
L
˕
)
∈ʘ
implies
(
,˃|=˕
M
ʘ
)
∩ˁ
1
;
···∩ˁ
n
(ii) (
˃
:
L
¬˕
)
∈ʘ
implies
(
,˃|=˕
M
ʘ
)
∩ˁ
1
;
···∩ˁ
n
.
(iii) (
˃
:
L
×
)
∈ʘ
implies
˃
is not in thedomain of
(
