A PSPACE-complete fragment of second-order linear logic

DOI10.1016/S0304-3975(98)00315-6zbMath0933.03018MaRDI QIDQ1960427

Guy Perrier

Publication date: 12 January 2000

Published in: Theoretical Computer Science (Search for Journal in Brave)

zbMATH Keywords

PSPACE-completedecision procedurefragmentinference permutability in proofssecond-order linear logic without exponentials

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Complexity of computation (including implicit computational complexity) (03D15) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) (03B47) Proof-theoretic aspects of linear logic and other substructural logics (03F52)

Related Items

Logical foundations for hybrid type-logical grammars

Cites Work

• On proof normalization in linear logic
• The undecidability of second order multiplicative linear logic
• Logic Programming with Focusing Proofs in Linear Logic
• The undecidability of second order linear logic without exponentials
• Unnamed Item
• Unnamed Item