Journal of Logic and Computation Advance Access originally published online on November 11, 2007
Journal of Logic and Computation 2008 18(1):171-199; doi:10.1093/logcom/exm063
Original Articles |
Cut Elimination and Decidability for Classical Lambek Logic
Ili
Faculty of Forestry, University of Belgrade, Kneza Vi
eslava 1, 11000 Belgrade, Serbia. E-mail: isakm{at}yubc.net
Received 14 December 2006.
In this article we give a cut elimination procedure for two-sided sequent system of classical Lambek logic and, on the basis of the presented procedure, a new proof of decidability for this logic.
Keywords: Classical Lambek logic; Cut-elimination theorem; Decidability
References
- Abrusci VM. Phase semantics and sequent calculus for pure noncomutative classical linear propositional logic. The Journal of Symbolic Logic (1991) 56:1403–1451.[CrossRef]
- Gentzen G. Investigations into Logical Deduction. The Collected Papers of Gerhard Gentzen—Szabo ME, ed. (1969) North-Holland, Amsterdam.
- Hudelmaier J, Schroeder-Heister P. Classical Lambek Logic, Theorem Proving with Analytic Tableaux and Related Methods. Baumgartner Peter, Hähnle Reiner, Posegga Joachim, eds. (1995) Berlin, Heidelberg: Springer. 245–262.
- Lafont Y. The finite model property for various fragments of linear logic. The Journal of Symbolic Logic (1997) 62:1202–1208.[CrossRef]
- Lambek J. The mathematics of sentence structure. The American Mathematical Monthly (1958) 65:154–170.[CrossRef]
- Lambek J. From Categorial Grammar to Bilinear Logic. Substructural Logics—Schroeder-Heister P, Do
en K, eds. (1993) Oxford: Oxford University Press. 207–237.
| ||||||||||||||||||||||||||||||||||||||||||||||