Information Technology Reference
In-Depth Information
To explain the notion of level let us consider an abstraction hierarchy in
Table 1. There
Level
(
X
)
2, meaning that literal
X
occurs in all abstracted
versions of a net starting from level 2. Similarly
Level
(
F
)
≡
≡
1and
Level
(
M
)
≡
0
in the same table.
j
=1
A
i
(
S
)(
l
j
)
,
n
Definition 9.
State
S
at abstraction level
i
is denoted with
A
i
(
S
)
≡
where
l
j
is the
j
-th literal in
S
,
S
has
n
literals, and
A
i
(
S
)(
l
)=
l
,if
Level
(
l
)
≥ i
1
,otherwise
In the preceding 1 is a constant of HLL. In the following we may omit some
instances of 1 in formulae to keep the representation simpler. Anyway, our for-
malism is still consistent since there are rules in HLL facilitating the removal of
1 from formulae and we assume that these rules are applied implicitly.
Definition 10.
Abstracted CSC
I
O
at abstraction level
i
is defined as
A
i
(
I
O
)
≡ A
i
(
I
)
A
i
(
O
)
.
Definition 11.
Abstracted CSA
A
=
Γ
;
S G
at abstraction level
i
is defined
as
A
i
(
A
)=
Γ
;
A
i
(
G
)
,where
Γ
=
A
i
(
S
)
1
A
i
(
c
)
.
∀c∈Γ∧A
i
(
c
)
=
1
≡ A
.Wewrite
Γ
i
and
L
i
to denote respectively a set of CSCs and literals of a CSA
A
0
(
A
)
At abstraction level 0 an original CSA is presented -
A
i
(
A
).
Definition 12.
Serialised proof fragment (SPF) is a sequence
S
0
,C
1
,S
1
,...,
C
n
,S
n
starting with a state
S
0
and ending with a state
S
n
. Between every
two states there is a CSC
C
i
,i
=1
...n
such that
S
i−
1
is the state where
C
i
was applied with a PD rule and the state
S
i
is the result achieved by applying
C
i
. Whenever a compact representation of a SPF is required, we shall write
C
1
,...,C
n
.
Definition 13.
Partial proof is a pair
(
H, T
)
,whereboth
H
and
T
are SPFs
with the first element of
H
being the initial state and the last element of
T
respectively the goal state. Initially the partial proof has only one element in both
H
and
T
- the initial state in
H
and the goal state in
T
.
The proof is extended in the following way. PD forward step can be applied
only to the last element of
H
. Symmetrically, PD backward step can be applied
only to the first element of
T
. In the former case the applied CSC and a new
state are inserted to the end of
H
. In the latter case the new state and the
applied CSC are inserted to the beginning of
T
.
Definition 14.
Complete proof is a partial proof with the last element of
H
and
the first element of
T
being equal.
If there is no need to distinguish partial and complete proofs, we write just
proof.
Search WWH ::
Custom Search