Information Technology Reference
In-Depth Information
abstraction level 2. Since the abstracted CSC is basically equivalent to
1,
it is discarded at this abstraction level. Analogously in the CSCs at abstraction
level 1 only literals
F
,
X
and
Y
are permitted. Finally at abstraction level 0 all
literals are allowed, because it is the lowest level of abstraction in the particular
abstraction hierarchy.
1
Table 1.
An abstraction hierarchy.
Level 0
Level 1
Level 2
Literals
I,E,M,H,N,F,X,Y
F, X, Y
X, Y
CSC
1
E ⊗ N
H
—
—
CSC
2
H
E ⊗ I ⊗ M
—
—
CSC
3
M
N
—
—
I
7
F
CSC
4
1
F
—
F ⊗ X
Y
2
F ⊗ X
Y
2
X
Y
2
CSC
5
Y
2
⊗ X
2
X
2
Y
2
⊗ X
2
X
2
Y
2
⊗ X
2
X
2
CSC
6
E ⊗ M ⊗ X
3
E ⊗ M ⊗ X
2
X
3
X
2
X
3
X
2
S G
We start PD from level 2 (the highest abstraction level) by finding a proof for
CSA
2
. The resulting complete proof (head
H
and tail
T
are not distinguished)
is represented as:
X
3
,
CSC
5
,X
2
⊗ Y
2
,
CSC
6
,X
2
.
Now, when moving from abstraction level 2 to level 1, although the CSA
to be proved would remain the same, the representation of
CSC
5
has changed.
Thus this part of the proof has to be extended. Therefore the resulting proof for
X
3
X
2
at abstraction level 1 is in serialised form:
X
3
,
CSC
4
,X
3
⊗ F,
CSC
5
,X
2
⊗ Y
2
,
CSC
6
,X
2
.
At abstraction level 0, in the original problem space, only CSCs
CSC
1
,
CSC
2
and
CSC
3
are new and may be used to extend the partial proof obtained at
abstraction level 1 to prove the initial problem
E ⊗ M ⊗ X
3
E ⊗ M ⊗ X
2
.
Thus the complete proof at abstraction level 0 would be:
E ⊗ M ⊗ X
3
, P
f
,E⊗ M ⊗ X
3
⊗ I
7
,
CSC
4
,E⊗ M ⊗ X
3
⊗ F,
CSC
5
,
,E⊗ M ⊗ X
2
⊗ Y
2
,
CSC
6
,E⊗ M ⊗ X
2
,
where
CSC
3
,E⊗N ⊗X
3
⊗I
i
,
CSC
1
,H⊗X
3
⊗I
i
,
CSC
2
,E⊗M ⊗X
3
⊗I
i
+1
7
,
P
f
=
{
}
where in turn
i
=0
...
6 denotes the iteration index.
6
Related Work and Conclusions
The first explicit use of abstraction in automated deduction was in the planning
version of GPS [13]. ABSTRIPS [16] was the first system that attempted to
Search WWH ::
Custom Search