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

Abstraction Within Partial Deduction
for Linear Logic

Peep Kungas

Norwegian University of Science and Technology
Department of Computer and Information Science
[e-mail]

Abstract. Abstraction has been used extensively in Artificial Intelli-
gence (AI) planning, human problem solving and theorem proving. In
this article we show how to apply abstraction within Partial Deduction
(PD) formalism for Linear Logic (LL). The proposal is accompanied with
formal results identifying limitations and advantages of the approach.
We adapt a technique from AI planning for constructing abstraction hier-
archies, which are then exploited during PD. Although the complexity of
PD for propositional LL is generally decidable, by applying abstraction
the complexity is reduced to polynomial in certain cases.

1 Introduction

Partial Deduction (PD) (or partial evaluation of logic programs, which was first
introduced by Komorowski [8]) is known as one of optimisation techniques in
logic programming. Given a logic program, PD derives a more specific program
while preserving the meaning of the original program. Since the program is more
specialised, it is usually more ecient than the original program.
A formalism of PD for !-Horn fragment [5] of Linear Logic [3] (LL) is given
in [11]. Also soundness and completeness of the formalism are proved there.
However, the formalism is still limited with the computational complexity arising
from the underlying logic. Since propositional !-Horn fragment of LL (HLL) can
be encoded as a Petri net, the complexity of HLL is equivalent to the complexity
of Petri net reachability checking and thus decidable [5]. Therefore, we consider
it very important to identify methodologies, which would help to decrease the
effects inherited from the complexity.
Abstraction techniques, constituting a subset of divide-and-conquer approac-
hes, are widely viewed as methods for making intractable problems tractable. Us-
ing abstraction techniques we may cut solution search space from b d to kb d/k [9,
15], where b and d are respectively the branching factor and the depth of the
search tree and k is the ratio of the abstraction space to the base space in an
abstraction hierarchy.
Korf [9] showed that when optimal abstraction hierarchies are used, it is pos-
sible to reduce the expected search time from O ( n )to O ( log n ). This improve-
ment makes combinatorial problems tractable. For instance, if n is a function