A PSPACE-complete fragment of second-order linear logic

DOI10.1016/S0304-3975(98)00315-6MaRDI QIDQ1960427zbMATH OpenFDO

Authors Guy Perrier

Publication date 12 January 2000

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

Full work available at URL https://doi.org/10.1016/S0304-3975(98)00315-6

zbMATH Keywords

decision procedurefragmentinference permutability in proofsPSPACE-completesecond-order linear logic without exponentials

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 1114353
• scientific article; zbMATH DE number 1163987
• The undecidability of second order multiplicative linear logic
• scientific article; zbMATH DE number 785051
• Decision problems for propositional linear logic

Cites work

• scientific article; zbMATH DE number 1163987 (Why is no real title available?)
• scientific article; zbMATH DE number 1499088 (Why is no real title available?)
• Logic Programming with Focusing Proofs in Linear Logic
• On proof normalization in linear logic
• The undecidability of second order linear logic without exponentials
• The undecidability of second order multiplicative linear logic

Cited in

(4)

• Space-efficient fragments of higher-order fixpoint logic
• Logical foundations for hybrid type-logical grammars
• scientific article; zbMATH DE number 1114353 (Why is no real title available?)
• A PSPACE-complete first-order fragment of computability logic

This page was built for publication: A PSPACE-complete fragment of second-order linear logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1960427)