Abstraction Within Partial Deduction for Linear Logic - Artificial Intelligence and Symbolic Computation - page 62

Theorem 4. If the preconditions of Proposition 1 are satisfied, then our algo-
rithm in Fig. 2 gives us an optimal abstraction hierarchy.

Proof. The proof follows from Proposition 1 and Definition 21.

The last theorem identifies that in order to take advantage of optimal ab-
straction hierarchies, we have to constrain heavily the CSCs in a CSA. However,
even if an optimal abstraction hierarchy is not constructed for a CSA, the non-
optimal one may still help to reduce the complexity of PD.

5 An Abstraction Example

In order to demonstrate PD with abstraction, let us consider the following CSA:

CSA 0 ::= E ⊗ M ⊗ X 3 ⊗ !( E ⊗ N H ) ⊗ !( H E ⊗ I ⊗ M ) ⊗ !( M N ) ⊗

!( I 7 !( F ⊗ X Y 2 ) !( Y 2 ⊗ X 2 X 2 ) E ⊗ M ⊗ X 2 ⊗ F ) ⊗ ⊗

The corresponding constraint graph, achieved by using the algorithm in
Fig. 1, is presented in Fig. 5(a). A directed edge from node A to node B in the
graph indicates that A cannot occur lower in the abstraction hierarchy than B .

F Y

I

E M N X

IMNEH F XY

H

(a) (b)

Fig. 5. The constraint graph (a) and the abstraction hierarchy derived from it (b).

One corresponding abstraction hierarchy derived from the graph presented in
Fig. 5(a) is depicted in Fig. 5(b). Using this abstraction hierarchy, we introduce 2
new abstracted CSAs

CSA 1 and CSA 2 for abstraction levels 1 and 2 respectively:

CSA 1 ::= X 3 !( Y 2 ⊗ X 2 X 2 ) !( F ⊗ X Y 2 ) X 2 ⊗ ⊗ ⊗ !(1 F )

CSA 2 ::= X 3 !( Y 2 ⊗ X 2 X 2 ) !( X Y 2 ) X 2 ⊗ ⊗

The literals and CSCs available at different abstraction levels are represented
inTable1.Thevalue“—”thererepresents that a CSC was abstracted to 1 1

and was thus then discarded, because this axiom is already included in HLL.
In Table 1 the CSCs at abstraction level 2 are obtained by substituting all
literals except X and Y with constant 1. For instance, H E ⊗I ⊗M is first

abstracted to 1 1 ⊗ 1 ⊗ 1, because literals H , E , I and M are not allowed at