Lambek calculus is NP-complete

DOI10.1016/J.TCS.2006.03.018MaRDI QIDQ2500488zbMATH OpenOpenAlexFDO

Authors Mati Pentus

Publication date 16 August 2006

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

Full work available at URL https://doi.org/10.1016/j.tcs.2006.03.018

zbMATH Keywords

complexitycyclic linear logicderivabilityLambek calculusmultiplicative fragmentsnoncommutative linear logic

Mathematics Subject Classification ID

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) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17)

Review text

The main goal of the paper is to show that the derivability problems for the Lambek calculus (L) and for the Lambek calculus allowing empty premises (L*) are NP-complete. The construction of a reduction from the problem CSAT to the L-derivability and L*-derivability problems is described, and the correctness of this reduction is proved. The proof of one lemma used in the proof of the main results is based on the technique of proof nets. A consequence of the main result of the paper is the NP-completeness of the derivability problem for the multiplicative fragments of cyclic linear logic and noncommutative linear logic. It is the first paper which shows the NP-completeness of derivability for the multiplicative fragments of noncommutative linear logics. A survey of complexity results for commutative linear logic was given by \textit{P. Lincoln} [``Deciding provability of linear logic formulas, in: J.-Y. Girard et al. (eds.), Advances in linear logic. Based on the linear logic workshop held June 14--18, 1993 at the Mathematical Sciences Institute, Cornell University, Ithaca, New York, USA. Cambridge: Cambridge University Press. Lond. Math. Soc. Lect. Note Ser. 222, 109--122 (1995; Zbl 0823.03004)].

Recommendations

• Product-free Lambek calculus is NP-complete
• Product-Free Lambek Calculus Is NP-Complete
• The monotone Lambek calculus is NP-complete
• Complexity of the Lambek calculus and its fragments
• LC graphs for the Lambek calculus with product
• The product-free Lambek-Grishin calculus is NP-complete
• An application of proof-nets to the study of fragments of the Lambek calculus
• The complexity of Horn fragments of linear logic
• scientific article; zbMATH DE number 1114352
• The Lambek-Grishin Calculus Is NP-Complete

Cites work

• scientific article; zbMATH DE number 4099289 (Why is no real title available?)
• scientific article; zbMATH DE number 3639144 (Why is no real title available?)
• scientific article; zbMATH DE number 1222927 (Why is no real title available?)
• scientific article; zbMATH DE number 1341472 (Why is no real title available?)
• scientific article; zbMATH DE number 976409 (Why is no real title available?)
• scientific article; zbMATH DE number 1114352 (Why is no real title available?)
• scientific article; zbMATH DE number 786489 (Why is no real title available?)
• scientific article; zbMATH DE number 1406803 (Why is no real title available?)
• Language in action. Categories, lambdas and dynamic logic
• Non‐associative Lambek Categorial Grammar in Polynomial Time
• Phase semantics and sequent calculus for pure noncommutative classical linear propositional logic
• Polynomial equivalence among systems LLNC, LLNC\(_a\) and LLNC\(_0\)
• Proving theorems of the second order Lambek calculus in polynomial time
• Quantales and (noncommutative) linear logic
• The Mathematics of Sentence Structure

Cited in

(56)

• Algebraic structures in categorial grammar
• Lambek calculus and its relational semantics: Completeness and incompleteness
• Proving theorems of the second order Lambek calculus in polynomial time
• The complexity of Horn fragments of linear logic
• Direct encodings of NP-complete problems into Horn sequents of multiplicative linear logic
• Pregroup grammars with letter promotions: complexity and context-freeness
• Models for the Lambek calculus
• The multiplicative-additive Lambek calculus with subexponential and bracket modalities
• Complexity of Lambek calculi with modalities and of total derivability in grammars
• Infinitary action logic with exponentiation
• Hypergraph Lambek grammars
• Non-associative, non-commutative multi-modal linear logic
• Powerful and NP-complete: hypergraph Lambek grammars
• Logical foundations for hybrid type-logical grammars
• Kleene star, subexponentials without contraction, and infinite computations
• Complexity of the universal theory of bounded residuated distributive lattice-ordered groupoids
• On involutive nonassociative Lambek calculus
• Type logics and pregroups
• System BV is NP-complete
• Recognition of derivability for the Lambek calculus with one division
• Lambek calculus with a unit and one division
• The finite model property for BCI and related systems
• Current trends in substructural logics
• Undecidability of the Lambek calculus with a relevant modality
• Proof nets for the displacement calculus
• Complexity of the Lambek calculus and its fragments
• Term graphs and the NP-completeness of the product-free Lambek calculus
• The product-free Lambek-Grishin calculus is NP-complete
• Good types are useful for learning
• Lambek Grammars with One Division Are Decidable in Polynomial Time
• Product-Free Lambek Calculus Is NP-Complete
• Product-free Lambek calculus is NP-complete
• Towards NP-P via proof complexity and search
• Trivalent logics arising from L-models for the Lambek calculus with constants
• Involutive nonassociative Lambek calculus: sequent systems and complexity
• Categorial grammars and their logics
• One-Sided Sequent Systems for Nonassociative Bilinear Logic: Cut Elimination and Complexity
• Extensions of Lambek calculi
• Pomset logic. The other approach to noncommutativity in logic
• LaserTank is NP-Complete
• Complexity of the infinitary Lambek calculus with Kleene star
• scientific article; zbMATH DE number 7204441 (Why is no real title available?)
• On translating Lambek grammars with one division into context-free grammars
• An application of proof-nets to the study of fragments of the Lambek calculus
• Subexponentials in non-commutative linear logic
• On Lambek's restriction in the presence of exponential modalities
• Extended Lambek calculi and first-order linear logic
• The monotone Lambek calculus is NP-complete
• Bracket induction for Lambek calculus with bracket modalities
• Proof-theoretic aspects of the logic of scope
• Complexity of nonassociative Lambek calculus with classical logic
• Chair of Mathematical Logic and Theory of Algorithms
• Lambek calculus with banged atoms for parasitic gaps
• Complexity of nonassociative Lambek calculus with classical and intuitionistic logic
• Infinitary action logic: complexity, models and grammars
• Unidirectional Lambek grammars in polynomial time

This page was built for publication: Lambek calculus is NP-complete

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