Decision problems for propositional linear logic

DOI10.1016/0168-0072(92)90075-BzbMATH Open0768.03003WikidataQ56340930 ScholiaQ56340930MaRDI QIDQ1192352FDOQ1192352

Authors: Natarajan Shankar, P. Lincoln, John Mitchell, Andre Scedrov 

Publication date: 27 September 1992

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

Recommendations

• The undecidability of second order multiplicative linear logic
• Decidability of linear affine logic
• The finite model property for various fragments of linear logic
• Constant-only multiplicative linear logic is NP-complete
• scientific article; zbMATH DE number 1163987

zbMATH Keywords

provabilitysequentsexponential-free fragmentfull propositional linear logictwo-counter machines

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (94)

• The complexity of decision procedures in relevance logic II
• Linear logic for nets with bounded resources
• Current trends in substructural logics
• Subexponentials in non-commutative linear logic
• The contraction rule and decision problems for logics without structural rules
• Focused proof-search in the logic of bunched implications
• On the decision problem for MELL
• Behavioural analysis of sessions using the calculus of structures
• System NEL is undecidable
• Exchange rules
• Implicational relevance logic is 2-\textsc{ExpTime}-complete
• A matrix characterization for multiplicative exponential linear logic
• Towards logical operations research -- propositional case
• The finite model property for various fragments of linear logic
• Relations and non-commutative linear logic
• Linearizing intuitionistic implication
• Disjunction property and complexity of substructural logics
• A logical characterization of forward and backward chaining in the inverse method
• Proof strategies in linear logic
• Multimodal linguistic inference
• A concurrent constraint programming interpretation of access permissions
• Linear logic automata
• The finite model property for knotted extensions of propositional linear logic
• Title not available (Why is that?)
• Logical foundations for hybrid type-logical grammars
• From multiple sequent for additive linear logic to decision procedures for free lattices
• Phase semantics and decidability of elementary affine logic
• Undecidability of the Lambek calculus with a relevant modality
• Petri nets, Horn programs, linear logic and vector games
• On Lambek's restriction in the presence of exponential modalities
• Soft subexponentials and multiplexing
• Direct encodings of NP-complete problems into Horn sequents of multiplicative linear logic
• Title not available (Why is that?)
• On the computational complexity of cut-elimination in linear logic.
• The multiplicative-additive Lambek calculus with subexponential and bracket modalities
• First-order linear logic without modalities is NEXPTIME-hard
• Proof complexity of substructural logics
• Linear concurrent constraint programming: Operational and phase semantics
• Complexity of the universal theory of bounded residuated distributive lattice-ordered groupoids
• Linear and affine logics with temporal, spatial and epistemic operators
• The decidability of the intensional fragment of classical linear logic
• Linear logic with fixed resources
• Undecidability of multiplicative subexponential logic
• Non-normal modalities in variants of linear logic
• Title not available (Why is that?)
• Focussing, \(\mathsf{MALL}\) and the polynomial hierarchy
• Linear Logic Proof Games and Optimization
• PSPACE-completeness of a thread criterion for circular proofs in linear logic with least and greatest fixed points
• Decision procedures for BDI logics
• Proof and refutation in MALL as a game
• Constant-only multiplicative linear logic is NP-complete
• Complexity of Lambek calculi with modalities and of total derivability in grammars
• Title not available (Why is that?)
• Preface to the special volume
• Complexity of a fragment of infinitary action logic with exponential via non-well-founded proofs
• Semantic data modelling using linear logic
• The undecidability of second order linear logic without exponentials
• A PSPACE-complete fragment of second-order linear logic
• Bunched logics displayed
• Title not available (Why is that?)
• Title not available (Why is that?)
• Non-associative, non-commutative multi-modal linear logic
• Title not available (Why is that?)
• Kleene star, subexponentials without contraction, and infinite computations
• The ILLTP library for intuitionistic linear logic
• Connection methods in linear logic and proof nets construction
• Title not available (Why is that?)
• State of the Art in Logics for Verification of Resource-Bounded Multi-Agent Systems
• From QBFs to \textsf{MALL} and back via focussing
• The undecidability theorem for the Horn-like fragment of linear logic (revisited)
• Title not available (Why is that?)
• Title not available (Why is that?)
• The ideal view on Rackoff's coverability technique
• MOST SIMPLE EXTENSIONS OF ARE UNDECIDABLE
• Two decision problems in Contact Logics
• MALL proof equivalence is logspace-complete, via binary decision diagrams
• Title not available (Why is that?)
• Encoding Hamiltonian circuits into multiplicative linear logic
• Expressing additives using multiplicatives and subexponentials
• Title not available (Why is that?)
• Relational Models for the Lambek Calculus with Intersection and Constants
• Multiplicative-additive proof equivalence is \textsf{logspace}-complete, via binary decision trees
• On Model Checking Boolean BI
• Towards a theory of resource: an approach based on soft exponentials
• Finite embeddability property for residuated lattices via regular languages
• A Linear-Logical Reconstruction of Intuitionistic Modal Logic S4
• Algorithmic complexity for theories of commutative Kleene algebras
• Synthetic Undecidability of MSELL via FRACTRAN Mechanised in Coq
• Linear Exponentials as Resource Operators: A Decidable First-order Linear Logic with Bounded Exponentials
• From double pushout grammars to hypergraph Lambek grammars with and without exponential modality
• Infinitary action logic with multiplexing
• RASP and ASP as a fragment of linear logic
• FULL LAMBEK CALCULUS WITH CONTRACTION IS UNDECIDABLE
• Decision problems for linear logic with least and greatest fixed points

This page was built for publication: Decision problems for propositional linear logic

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