Decision problems for propositional linear logic

DOI10.1016/0168-0072(92)90075-BzbMath0768.03003WikidataQ56340930 ScholiaQ56340930MaRDI QIDQ1192352

Natarajan Shankar, Andrej Scedrov, Patrick D. Lincoln, John C. Mitchell

Publication date: 27 September 1992

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

zbMATH Keywords

provabilitysequentsexponential-free fragmentfull propositional linear logictwo-counter machines

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Undecidability and degrees of sets of sentences (03D35) Decidability of theories and sets of sentences (03B25) Complexity of computation (including implicit computational complexity) (03D15) Cut-elimination and normal-form theorems (03F05) Subsystems of classical logic (including intuitionistic logic) (03B20)

Related Items

Current trends in substructural logics, On Lambek’s Restriction in the Presence of Exponential Modalities, Linear and affine logics with temporal, spatial and epistemic operators, Proof strategies in linear logic, State of the Art in Logics for Verification of Resource-Bounded Multi-Agent Systems, Logical foundations for hybrid type-logical grammars, First-order linear logic without modalities is NEXPTIME-hard, Constant-only multiplicative linear logic is NP-complete, Complexity of a fragment of infinitary action logic with exponential via non-well-founded proofs, Behavioural Analysis of Sessions Using the Calculus of Structures, Semantic data modelling using linear logic, Petri nets, Horn programs, linear logic and vector games, FULL LAMBEK CALCULUS WITH CONTRACTION IS UNDECIDABLE, IMPLICATIONAL RELEVANCE LOGIC IS 2-EXPTIME-COMPLETE, Relations and non-commutative linear logic, Phase semantics and decidability of elementary affine logic, Linear logic for nets with bounded resources, Linear logic automata, Multimodal linguistic inference, RASP and ASP as a fragment of linear logic, Nonelementary Complexities for Branching VASS, MELL, and Extensions, Non-normal modalities in variants of linear logic, MOST SIMPLE EXTENSIONS OF ARE UNDECIDABLE, Bunched logics displayed, Relational Models for the Lambek Calculus with Intersection and Constants, Finite embeddability property for residuated lattices via regular languages, Proof and refutation in MALL as a game, Infinitary action logic with multiplexing, Unnamed Item, From QBFs to \textsf{MALL} and back via focussing, Unnamed Item, Linear Exponentials as Resource Operators: A Decidable First-order Linear Logic with Bounded Exponentials, Unnamed Item, Linear Logic Proof Games and Optimization, A logical characterization of forward and backward chaining in the inverse method, The undecidability of second order linear logic without exponentials, On the decision problem for MELL, The contraction rule and decision problems for logics without structural rules, Focused proof-search in the logic of bunched implications, Expressing additives using multiplicatives and subexponentials, Kleene star, subexponentials without contraction, and infinite computations, A concurrent constraint programming interpretation of access permissions, Exchange rules, The finite model property for various fragments of linear logic, Preface to the special volume, Linearizing intuitionistic implication, System NEL is Undecidable, The undecidability theorem for the Horn-like fragment of linear logic (Revisited), Disjunction property and complexity of substructural logics, Unnamed Item, Unnamed Item, The complexity of decision procedures in relevance logic II, Encoding Hamiltonian circuits into multiplicative linear logic, Proof complexity of substructural logics, The ideal view on Rackoff's coverability technique, The multiplicative-additive Lambek calculus with subexponential and bracket modalities, The finite model property for knotted extensions of propositional linear logic, The decidability of the intensional fragment of classical linear logic, A Linear-Logical Reconstruction of Intuitionistic Modal Logic S4, On Model Checking Boolean BI, Complexity of Lambek calculi with modalities and of total derivability in grammars, Towards a theory of resource: an approach based on soft exponentials, Complexity of the universal theory of bounded residuated distributive lattice-ordered groupoids, Undecidability of the Lambek Calculus with a Relevant Modality, Subexponentials in non-commutative linear logic, Connection methods in linear logic and proof nets construction, Unnamed Item, Soft subexponentials and multiplexing, Linear concurrent constraint programming: Operational and phase semantics, Non-associative, non-commutative multi-modal linear logic

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Linear logic
• Recursive unsolvability of Post's problem of Tag und other topics in theory of Turing machines
• Petri nets and large finite sets
• A decidable fragment of predicate calculus
• The linear abstract machine
• The semantics and proof theory of linear logic
• Bounded linear logic: A modular approach to polynomial-time computability
• The structure of multiplicatives
• On the finite containment problem for Petri nets
• The complexity of the word problems for commutative semigroups and polynomial ideals
• The Mathematics of Sentence Structure
• Quantales and (noncommutative) linear logic
• The undecidability of entailment and relevant implication
• How to Program an Infinite Abacus
• Alternation
• Quantales, observational logic and process semantics
• Recursive Unsolvability of a problem of Thue
• From petri nets to linear logic