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

Algorithm CreateHierarchy ( Γ , G )

inputs: a set of CSCs Γ and a goal state G
output: an ordered monotonic abstraction hierarchy

begin
graph ← DetermineConstraints ( {}, Γ , G )
components ← FindStronglyConnectedComponents ( graph )
partialOrder ← ConstructReducedGraph ( graph, components )
absHierarchy TopologicalSort ( partialOrder )

return absHierarchy
end CreateHierarchy

←

Fig. 2. Creating an abstraction hierarchy.

extended by observing the succedents of CSCs and in the case it consists only of
1, the CSC would not be considered. Anyway these CSCs may be needed during
reasoning.

3.1 The Role of the Initial State

While building a constraint graph for abstraction, dependencies between literals
are detected. If it should happen that at least one literal l ∈ S is not included in
the constraint graph and it does not occur in the goal state G either, then there
is no proof for the particular CSA. This applies iff there are no CSCs, which
could consume literal l .

Theorem 1. Given a CSA and a set of edges D e of the constraint graph D ,

which was constructed for the CSA, and if ∃l. ( l ∈ S ∧ l ∈ G ∧ l ∈ D e ∧∀c ∈

Γ. ( succ ( c ) =1) , then there is no proof for the CSA.

Proof. While finding dependencies between literals through constraint graph
construction, roughly a way for literal propagation is estimated for reaching the
goal G and literals on the way are inserted to the graph. Therefore, if not all
literals l ∈ S are included in the constraint graph, then there is no way to find
aprooffor Γ ; S G .
Anyway, some literals in the initial state S may be not engaged during PD
and thus they exist in both states S and G . In that case the missing literal from
a constraint graph does not indicate that the state G is not reachable. Similarly,
CSCs C with succ ( C )

≡

1 have to be considered, since they only consume literals
and therefore are rejected, when generating a constraint graph.

This case is illustrated in Fig. 3(b), where a constraint graph is generated for
CSA Γ ; A ⊗ B ⊗ C F . As it can be seen in Fig. 3(b) the literal B , although
being in the state S , is not included in the constraint graph. The same applies
for literal A . Therefore the CSA has no proof.