1ST-ORDER LINEAR LOGIC WITHOUT MODALITIES IS NEXPTIME-HARD

Authors
LINCOLN P SCEDROV A
Citation
P. Lincoln et A. Scedrov, 1ST-ORDER LINEAR LOGIC WITHOUT MODALITIES IS NEXPTIME-HARD, Theoretical computer science, 135(1), 1994, pp. 139-153
Citations number
20
Categorie Soggetti
Computer Sciences","Computer Science Theory & Methods
Journal title
Theoretical computer science → ACNP
ISSN journal
03043975
Volume
135
Issue
1
Year of publication
1994
Pages
139 - 153
Database
ISI
SICI code
0304-3975(1994)135:1<139:1LLWMI>2.0.ZU;2-6
Abstract
The decision problem is studied for the nonmodal or multiplicative-add itive fragment of first-order linear logic. This fragment is shown to be NEXPTIME-hard. The hardness proof combines Shapiro's logic programm ing simulation of nondeterministic Turing machines with the standard p roof of the PSPACE-hardness of quantified boolean formula validity, ut ilizing some of the surprisingly powerful and expressive machinery of linear logic.