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

Definition 15. New CSCs at abstraction level n are defined with Γ new
n

= C i |

( C i ∈ Γ ) ∧ ( A n +1 ( C i ) ≡ 1 1) ∧ ( A n ( C i ) = A n +1 ( C i )) .

Definition 16. SPF s = C 1 ,...,C n ,C j ∈ Γ, j =1 ...n at abstraction level i

is defined as A i ( s )= C j | 0 <j≤|s|,C j ∈ Γ i .

Basically it means that at abstraction level i in a partial proof s only these
CSCs are allowed, which exist in the abstracted CSA at abstraction level i .Other
CSCs are just discarded. Opposite operation to abstraction is refinement.

l k ,k > l of a SPF s =

Definition 17. Refinement C 1 ,...,C n ,C j ∈ Γ, j =

1 ...n from abstraction level k to abstraction level l is defined as a sequence
R

R

l k ( s )=

α 0 ,C 1 ,α 1 ,...α n− 1 ,C n ,α n ,where α i ,i =0 ...n is a sequence of CSCs

l

from A ∈ Γ i .

i = k− 1

This means that during refinement only new CSCs at particular abstraction
level may be inserted to partial proofs. In the following we write

R

j

instead of

j
j +1 .

R

3 Generating Abstraction Hierarchies

In this section we describe how to construct abstraction hierarchies for CSAs.
These hierarchies are later used to gradually refine an abstract solution dur-
ing PD. The abstraction method, we propose here, has been inspired from an
abstraction method [7] from the field of AI planning.
Given a problem space, which consists of a CSA, our algorithm reformulates
the original problem into more abstract ones. The main effect of abstraction
is the elimination of inessential program clauses at every abstraction level and
thus the division of the original search space into smaller, sequentially searchable
ones. The original problem represents the lowest abstraction level.
Ordered monotonicity property is used as the basis for generating abstraction
hierarchies. This property captures the idea that if an abstract solution is refined,
the structure of the abstract solution should be maintained. Hence elements in
the proof fragments of a proof, would not be reordered while extending this
sequence at abstraction level i − 1. The process of refining an abstract solution

requires the application of additional CSCs to achieve the literals ignored at
more abstract levels.

Definition 18. Ordered monotonic refinement R is a refinement of an abstract

j
i ( s )) = s, j ≤ i ,where s is a proof fragment, i denotes the
abstraction level, where s was constructed and j is the target abstraction level.

solution s so that A i ( R

Definition 19. Ordered monotonic hierarchy is an abstraction hierarchy with
the property that for every solvable problem there exists an abstract solution that
has a sequence of ordered monotonic refinements into the base space.