Information Technology Reference
In-Depth Information
exponential in the problem size, then
log n
is just linear, according to Korf. The
essential reason why abstraction reduces complexity is that the total complexity
is the sum of the complexities of the multiple searches, not their product.
In the following we shall show how to generate automatically abstraction
hierarchies for LL applications. Then, when applying PD, first an initial (par-
tial) proof is constructed in the most abstract space in that hierarchy and then
gradually the proof is extended while moving from higher levels of abstraction
towards the base level given by the initial problem. A (partial) proof found at a
certain abstraction level may be viewed as a proof including “gaps”, which have
to be filled at lower levels of abstractions.
The rest of the paper is organised as follows. Section 2 introduces prelim-
inaries and basic definitions. Section 3 introduces a method for constructing
abstraction hierarchies. Section 4 focuses on PD with abstraction hierarchies.
Section 5 demonstrates the application of abstraction to PD. Section 6 reviews
the related work and concludes the paper.
2
Preliminaries and Definitions
2.1 Horn Linear Logic
In the following we are considering !-Horn fragment [5] of LL (HLL) consisting of
multiplicative conjunction (
) and “of course” operator
(!). In terms of resource acquisition the logical expression
A⊗ B C ⊗ D
means
that resources
C
and
D
are obtainable only if both
A
and
B
are obtainable.
After the sequent has been applied,
A
and
B
are consumed and
C
and
D
are
produced.
While implication
A
B
as a computability statement clause in HLL could
be applied only once, !(
A
B
) may be used an unbounded number of times.
Therefore the latter formula could be represented with an extralogical LL axiom
A
B
.When
A
B
is applied, then literal
A
becomes deleted from and
B
inserted to the current set of literals. If there is no literal
A
available, then
the clause cannot be applied. In HLL ! cannot be applied to other formulae than
linear implications.
Whenever a compact representation is needed we shall write the set of ex-
tralogical axioms
⊗
), linear implication (
{ A ⊗ B
C, D ⊗ E
F,...}
and the sequent
X Y
to
be proved as a single sequent
X⊗
⊗ ... Y
.To
allow shorter representation of formulae, we are using in the following sometime
abbreviation
a
n
=
a ⊗ ...⊗ a
!(
A ⊗ B
C
)
⊗
!(
D ⊗ E
F
)
,for
n>
0.
n
2.2 Partial Deduction for HLL
In this section we present the definitions of the basic concepts of PD for HLL.
We adopt the PD framework as it was formalised in [11].
Definition 1.
Computation Specification Clause (CSC) is a LL sequent
I
f
O,
Search WWH ::
Custom Search