System BV is NP-complete

DOI10.1016/J.APAL.2007.11.005MaRDI QIDQ2478549zbMATH OpenOpenAlexFDO

Authors Ozan Kahramanoğulları

Publication date 28 March 2008

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

Full work available at URL https://doi.org/10.1016/j.apal.2007.11.005

zbMATH Keywords

NP-completenessproof theorynondeterminismdeep inferencecalculus of structuresextension of multiplicative linear logicsystem BV

Mathematics Subject Classification ID

Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Proof-theoretic aspects of linear logic and other substructural logics (03F52)

Recommendations

• A system of interaction and structure
• Constant-only multiplicative linear logic is NP-complete
• A System of Interaction and Structure II: The Need for Deep Inference
• Direct encodings of NP-complete problems into Horn sequents of multiplicative linear logic
• Lambek calculus is NP-complete

Cites work

• scientific article; zbMATH DE number 2185722 (Why is no real title available?)
• scientific article; zbMATH DE number 3959364 (Why is no real title available?)
• scientific article; zbMATH DE number 42752 (Why is no real title available?)
• scientific article; zbMATH DE number 3639144 (Why is no real title available?)
• scientific article; zbMATH DE number 1980929 (Why is no real title available?)
• scientific article; zbMATH DE number 2090535 (Why is no real title available?)
• A Local System for Intuitionistic Logic
• A System of Interaction and Structure II: The Need for Deep Inference
• A system of interaction and structure
• A systematic proof theory for several modal logics
• Constant-only multiplicative linear logic is NP-complete
• From Proof Nets to the Free *-Autonomous Category
• Linear logic
• MELL in the calculus of structures
• Reducing Nondeterminism in the Calculus of Structures
• Subnets of proof-nets in multiplicative linear logic with MIX
• System NEL is undecidable

Cited in

(5)

• A System of Interaction and Structure III: The Complexity of BV and Pomset Logic
• On the decision problem for MELL
• True concurrency of deep inference proofs
• Maude as a platform for designing and implementing deep inference systems
• A logical basis for quantum evolution and entanglement

This page was built for publication: System BV is NP-complete

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