Information Technology Reference
In-Depth Information
⇒ ∀
n
:
NF
. ∃
e
:
EM
.
NT
(
n
,
e
) → ∃
e
:
EM
. ∀
s
:
DT
.
ST
(
e
,
s
)
Therefore, we get a sub-goal which leads to the goal:
goal
2(
n
) ≡ ∃
e
:
EM
.
NT
(
n
,
e
)
with input
n
. However, although
goal
2 checks domain
NF
, it still does not contain input
u
. Using A2,
we have the following deduction:
∀
l
:
LK
. ∀
n
:
NF
. (
MT
(
l
,
n
) → ∃
e
:
EM
.
NT
(
n
,
e
))
⇒ ∀
l
:
LK
. ∃
n
:
NF
. (
MT
(
l
,
n
) → ∃
e
:
EM
.
NT
(
n
,
e
))
⇒ ∀
l
:
LK
. ∃
n
:
NF
.
MT
(
l
,
n
) → ∀
n
:
NF
. ∃
e
:
EM
.
NT
(
n
,
e
)
and we obtain another sub-goal:
goal
1(
l
) ≡ ∃
n
:
NF
.
MT
(
l
,
n
)
with input
l
. With a similar deduction using A1:
∀
u
:
UD
. ∀
l
:
LK
. (
MA
(
u
,
l
) → ∃
n
:
NF
.
MT
(
l
,
n
))
⇒ ∀
u
:
UD
. ∃
l
:
LK
. (
MA
(
u
,
l
) → ∃
n
:
NF
.
MT
(
l
,
n
))
⇒ ∀
u
:
UD
. ∃
l
:
LK
.
MA
(
u
,
l
) → ∃
l
:
LK
. ∃
n
:
NF
.
MT
(
l
,
n
)
we can further obtain:
goal
0(
u
) ≡ ∃
l
:
LK
.
MA
(
u
,
l
)
which contains input
u
.
Note that the input and output of the sub-goals form a pipelining structure:
u
l
n
e
→
goal
0
→
goal
1
→
goal
2
→
goal
According to Rule 7 in Section 3, the verification program of
goal
0 can be constructed as:
<
goal
0[
u
]> = <
t
,
ff
,
true
,
false
,
LK
,
false
,
∅:
R
> where
true
= γ(
l
:
LK
)<
MA
[
u, l
]>=<
true
>.
true
,
l
:
R
,
true
false =
γ(
l
:
LK
)
< MA
[
u, l
]>=<
false
>.
false
,
false
ff =
γ(
false
,
l
)
l≠
true
∧
type
(
l
)
≠R
.
false
t
=
γ(
true
,
l
)
type
(
l
)
≠R
.
true
where
MA
[
u
,
l
] denote the molecule constructed to verify specification MA(u, l).
Search WWH ::
Custom Search