System BV is NP-complete

详细信息    查看全文

• 作者：Ozan Kahramano&#x11f ; ulları
• 关键词：Proof theory ; Deep inference ; Calculus of structures ; System
• 刊名：Annals of Pure and Applied Logic
• 出版年：2008
• 出版时间：March 2008
• 年：2008
• 卷：152
• 期：1-3
• 页码：107-121
• 全文大小：384 K

System is an extension of multiplicative linear logic () with the rules mix, nullary mix, and a self-dual, noncommutative logical operator, called seq. While the rules mix and nullary mix extend the deductive system, the operator seq extends the language of . Due to the operator seq, system extends the applications of to those where the sequential composition is crucial, e.g., concurrency theory. System is an extension of with the rules mix and nullary mix. In this paper, by relying on the fact that system is a conservative extension of system , I show that system is NP-complete by encoding the 3-Partition problem in . I provide a simple completeness proof of this encoding by resorting to a novel proof theoretical method for reducing nondeterminism in proof search, which is also of independent interest.