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

Definition 20. Let A and B be arbitrary vertices in a directed graph. Then we
say that they are strongly connected, if there exists a cycle with A as its initial
and final vertex such that this cycle includes Venice B .
An ordered monotonic abstraction hierarchy is constructed by dividing lit-
erals a CSA between abstraction levels such that the literals at level i do not
interact with literals at level i + 1. We say that places A and B do not interact
with each other, if they are not strongly connected in the constraint graph of the
particular CSA. Therefore, the ordered monotonicity property guarantees that
the goals and subgoals arising during the process of refining an abstract solution
will not interact with the conditions already achieved at more abstract levels.
This sort of abstraction is considered as Theorem Increasing in [4], stating that
if a theorem is not provable in an abstract space, it neither is in the base space.

Algorithm DetermineConstraints ( graph, Γ , G )

inputs: a set of CSCs Γ and a goal state G
output: constraints, which guarantee ordered monotonicity

begin
for ∀literal ∈ G
if not( ConstraintsDetermined ( literal, graph ) ) then
ConstraintsDetermined ( literal, graph ) ← true
for ∀csc ∈ Γ
if literal ∈ succ ( csc ) then
for ∀l ∈ succ ( csc )
AddDirectedEdge ( literal, l, graph )
end for
for ∀l ∈ ant ( csc )
AddDirectedEdge ( literal, l, graph )
end for
DetermineConstraints ( graph , Γ , ant ( csc ))

end if
end for
end if
end for
return graph
end DetermineConstraints

Fig. 1. Building a constraint graph.

Our algorithm first generates a graph representing dependencies (see Fig. 1)
between literals in a CSA, and then, by using that graph, finally generates an
ordered monotonic abstraction hierarchy (see Fig. 2).
Antecedents of CSCs if form K

1(where K is a multiplicative conjunction
of literals), are inserted as they occur in the goal state because they, although
possibly needed for achieving the goal, contain possibly literals not included in
the constraint graph. The latter is due to the fact that the constraint graph is