LINEAR LOGIC WITH FIXED RESOURCES

In this paper we continue the study of Girard's Linear Logic and intro duce a new Linear Logic with modalities. Our logic describes not only the consumption, but also the presence of resources. We introduce a ne w semantics and a new calculus for this logic. In contrast to the resu lts of Lincoln et al. [7] and Kanovich [4] about the NP-completeness o f the problem of the construction of a proof for a given sequent in th e multiplicative fragment of Girard's Linear Logic, we present here a non-exponential algorithm to construct a proof for a given sequent and a given point of a given model in our Linear Logic.