Proving theorems of the second order Lambek calculus in polynomial time
Studia Logica 53 (3):373 - 387 (1994)
| Abstract | 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 | ||||||||||
| Options |
|
|||||||||
| PhilPapers Archive |
Upload a copy of this paper Check publisher's policy on self-archival Papers currently archived: 5,711 |
| External links |
|
| Through your library | Configure |
Heinrich Wansing (2002). A Rule-Extension of the Non-Associative Lambek Calculus. Studia Logica 71 (3):443-451.
Thomas Strahm (1997). Polynomial Time Operations in Explicit Mathematics. Journal of Symbolic Logic 62 (2):575-594.
Andreas Blass & Yuri Gurevich (2003). Strong Extension Axioms and Shelah's Zero-One Law for Choiceless Polynomial Time. Journal of Symbolic Logic 68 (1):65-131.
Wojciech Zielonka (2002). On Reduction Systems Equivalent to the Lambek Calculus with the Empty String. Studia Logica 71 (1):31-46.
Michael Alekhnovich, Sam Buss, Shlomo Moran & Toniann Pitassi (2001). Minimum Propositional Proof Length is NP-Hard to Linearly Approximate. Journal of Symbolic Logic 66 (1):171-191.
A. Carbone (2002). The Cost of a Cycle is a Square. Journal of Symbolic Logic 67 (1):35-60.
Maria Bulińska (2005). The Pentus Theorem for Lambek Calculus with Simple Nonlogical Axioms. Studia Logica 81 (1):43 - 59.
Philippe De Groote & François Lamarche (2002). Classical Non-Associative Lambek Calculus. Studia Logica 71 (3):355 - 388.
Philippe de Groote & François Lamarche (2002). Classical Non-Associative Lambek Calculus. Studia Logica 71 (3):355-388.
Maria Bulińska (2009). On the Complexity of Nonassociative Lambek Calculus with Unit. Studia Logica 93 (1).
Monthly downloads |
Added to index2009-01-28Total downloads9 ( #114,265 of 551,105 )Recent downloads (6 months)1 ( #63,341 of 551,105 )How can I increase my downloads? |

