The other linear logic

Abstract

One of computer science motivations for Linear Logic is that proofs in this logic reflect the use of certain resources. However, the problem of availability of resources is not addressed. In this paper we are attempting to fill this gap.

Our approach can be illustrated most clearly by example of a Horn fragment. In this fragment, the left part of each sequent is a conjunction of simple implications and supplies, and the right part is a simple conjunction of supplies. An implication is called simple, if both its succedent and antecedent are conjunctions of supplies. As usual, a supply is simply a letter.

The standard axiom system for this Horn fragment consists of three inference rules, while the axioms are all the sequents with a single letter both for the left and right parts (the letter is the same).

On the other hand, the implications can be thought of as determining relations in a commutative semigroup and then we show that a sequent is provable iff the collection of supplies in its right part can be obtained from the left one by applying all the relations from the left part in appropriate order.

Now, let us require that the left part (i.e. all its supplies) is available. For this case we construct a new axiom system with sligtly more complex axioms and inference rules in which any axiom can be used at most once. Among other corollaries of this result we obtain the NP-completeness of the Horn fragment (known result).

However, for a bounded number of implication types we construct a subexponential algorithm for the derivation search.