Paper available by ftp

To: types
Subject: Paper available by ftp
From: andre@saul.cis.upenn.edu (Andre Scedrov)
Date: Tue, 01 Sep 92 10:51:24 EDT
Sender: meyer@theory.lcs.mit.edu

Date: Mon, 31 Aug 92 16:38:50 EDT

        First Order Linear Logic Without Modalities is NEXPTIME-Hard 

                        P. Lincoln  and  A. Scedrov  


     ABSTRACT: In this paper the decision problem is studied for the 
     multiplicative-additive fragment of linear logic with first order 
     quantifiers. This fragment is shown to be NEXPTIME-hard. The hardness 
     proof combines Shapiro's logic programming simulation of nondeterministic
     Turing machines with the standard proof of the PSPACE-hardness of 
     quantified boolean formula validity, utilizing some of the surprisingly 
     powerful and expressive machinery of linear logic. In contrast to 
     previous work on linear logic proof search as a computational paradigm, 
     in which a computation proceeds ``upwards'' along a proof tree, here the 
     computation steps are applied ``horizontally across'' the leaves of a 
     proof tree.  


This paper can be retrieved by anonymous ftp using the instructions below.  
If you would like a copy but cannot use ftp to this site, please send me your 
postal address.   

% ftp ftp.cis.upenn.edu
Name: anonymous
Password:  <<your e-mail address>>
ftp> cd pub/papers/scedrov 
ftp> binary
ftp> get mall1.dvi  
ftp> quit