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

level, in the initial theorem to be proved by the unit of , which is 1. In this

way corresponding abstracted initial and final states are formed. Analogously
we substitute literals in CSCs to form a set of abstracted CSCs.
Due to ordered monotonicity at every level of abstraction only new CSCs
can be inserted into a proof, because the old ones have already been placed at
their respective positions in the proof, if they were needed. By permitting only
newly introduced CSCs at each level the branching factor of proof search space
is decreased.
Every proof found at an higher abstraction level may generate a sequence
of subgoals for a lower level abstraction, if literals have been restored to CSCs
used in these proofs. Thus, through using abstraction, also the distance between
subgoal states is reduced. While extending a proof with new CSCs at particular
abstraction level, gaps in a proof are filled. The gaps were introduced by moving
to the lower abstraction level. The high-level algorithm for theorem proving with
abstraction is presented in Fig. 4.

⊗

Algorithm AbstractProver ( S , G,H, Γ )
inputs: the initial and the goal state, an abstraction hierarchy,

Γ

P

output: //a set of valid proofs

begin
level ← highestLevel ( hierarchy )
proof ←{}
absInit ←A level ( S )
absGoal ←A level ( G )
P ← Solve ( absInit, proof , absGoal, Γ new
level

)

l ← level − 1 to 0
P 2 ←{}
for ∀p ∈ P
absInit ←A l ( S )
absGoal ←A l ( G )
P 2 ← P 2 ∪ ExtendProof ( 0 , absInit, absGoal, p, Γ new
l

for

, l )

end for
P ← P 2
end for
return P
end AbstractProver

Fig. 4. A pseudocode for theorem proving with abstraction.

AbstractProver goes incrementally through all abstraction levels starting
from the highest and ending at the base abstraction level. At every abstrac-
tion level it computes a set of abstract proofs, which are refined at lower levels
until a proof has been computed or it is determined that there is no solution for
aparticularCSA.
The main operation of algorithm ExtendProof is to detect and fill gaps in
proofs when refining them. The complexity of the algorithm AbstractProver to-
gether with the ExtendProof depends on the number of abstraction levels l h ,on