Studia Logica 53 (3):373 - 387 (1994)
In the Lambek calculus of order 2 we allow only sequents in which the depth of nesting of implications is limited to 2. We prove that the decision problem of provability in the calculus can be solved in time polynomial in the length of the sequent. A normal form for proofs of second order sequents is defined. It is shown that for every proof there is a normal form proof with the same axioms. With this normal form we can give an algorithm that decides provability of sequents in polynomial time.
|Keywords||No keywords specified (fix it)|
|Categories||categorize this paper)|
References found in this work BETA
No references found.
Citations of this work BETA
Non‐Associative Lambek Categorial Grammar in Polynomial Time.Erik Aarts & Kees Trautwein - 1995 - Mathematical Logic Quarterly 41 (4):476-484.
Similar books and articles
A Rule-Extension of the Non-Associative Lambek Calculus.Heinrich Wansing - 2002 - Studia Logica 71 (3):443-451.
Polynomial Time Operations in Explicit Mathematics.Thomas Strahm - 1997 - Journal of Symbolic Logic 62 (2):575-594.
Strong Extension Axioms and Shelah's Zero-One Law for Choiceless Polynomial Time.Andreas Blass & Yuri Gurevich - 2003 - Journal of Symbolic Logic 68 (1):65-131.
On Reduction Systems Equivalent to the Lambek Calculus with the Empty String.Wojciech Zielonka - 2002 - Studia Logica 71 (1):31-46.
Minimum Propositional Proof Length is NP-Hard to Linearly Approximate.Michael Alekhnovich, Sam Buss, Shlomo Moran & Toniann Pitassi - 2001 - Journal of Symbolic Logic 66 (1):171-191.
Classical Non-Associative Lambek Calculus.Philippe De Groote & François Lamarche - 2002 - Studia Logica 71 (3):355 - 388.
Added to index2009-01-28
Total downloads43 ( #122,177 of 2,177,980 )
Recent downloads (6 months)2 ( #166,489 of 2,177,980 )
How can I increase my downloads?