[Prev][Next][Index][Thread]
Paper available by ftp
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