Information Technology Reference

In-Depth Information

Abstraction Within Partial Deduction

for Linear Logic

Peep Kungas

Norwegian University of Science and Technology

Department of Computer and Information Science

peep@idi.ntnu.no

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

Search WWH ::

Custom Search