A PSPACE-complete fragment of second-order linear logic

Authors
Perrier, G
Citation
G. Perrier, A PSPACE-complete fragment of second-order linear logic, THEOR COMP, 224(1-2), 1999, pp. 267-289
Citations number
10
Categorie Soggetti
Computer Science & Engineering
Journal title
THEORETICAL COMPUTER SCIENCE
ISSN journal
03043975 → ACNP
Volume
224
Issue
1-2
Year of publication
1999
Pages
267 - 289
Database
ISI
SICI code
0304-3975(19990806)224:1-2<267:APFOSL>2.0.ZU;2-E
Abstract
Existentially quantified variables are the source of non-decidability for s econd-order linear logic without exponentials (MALL2). We present a decisio n procedure for a fragment of MALL2 based on a canonical instantiation of t hese variables and using inference permutability in proofs. We also establi sh that this fragment is PSPACE-complete. (C) 1999 Elsevier Science B.V. Al l rights reserved.