Involutive Nonassociative Lambek Calculus: Sequent Systems and Complexity

• Autorzy: Wojciech Buszkowski
• Języki publikacji: EN

Abstrakty

EN

In [5] we study Nonassociative Lambek Calculus (NL) augmented with De Morgan negation, satisfying the double negation and contraposition laws. This logic, introduced by de Grooté and Lamarche [10], is called Classical Non-Associative Lambek Calculus (CNL). Here we study a weaker logic InNL, i.e. NL with two involutive negations. We present a one-sided sequent system for InNL, admitting cut elimination. We also prove that InNL is PTIME.

Słowa kluczowe

EN

nonassociative Lambek calculus; linear logic; sequent system; cut elimination; PTIME complexity

• Wydawca: Wydawnictwo Uniwersytetu Łódzkiego
• Czasopismo: Bulletin of the Section of Logic
• Rocznik: 2017
• Tom: 46
• Numer: 1/2

Daty

wydano

2017-06-30

Twórcy

autor

Wojciech Buszkowski

• Adam Mickiewicz University, Faculty of Mathematics and Computer Science, Poznań, Poland

Bibliografia

• [1] V. M. Abrusci, Phase semantics and sequent calculus for pure noncommutative classical linear propositional logic, Journal of Symbolic Logic 56 (1991), pp. 1403–1451.
• [2] A. Bastenhof, Categorial Symmetry, Ph.D. Thesis, University of Utrecht (2013).
• [3] W. Buszkowski, Lambek Calculus with Nonlogical Axioms, [in:] Casadio, C., Scott, P.J. and Seely, R.A.S., Language and Grammar. Studies in Mathematical Linguistics and Natural Language. CSLI Lecture Notes 168 (2005), pp. 77–93.
• [4] W. Buszkowski, An Interpretation of Full Lambek Calculus in Its Variant without Empty Antecedents of Sequents, [in:] Asher, N. and Soloviev, S. (eds.), Logical Aspects of Computational Linguistics, Lecture Notes in Computer Science, vol. 8535 (2014), Springer, pp. 30–43.
• [5] W. Buszkowski, On Classical Nonassociative Lambek Calculus, [in:] Amblard, M,, de Groote, Ph., Pogodalla, S., and Retoré, C. (eds.), Logical Aspects of Computational Linguistics, Lecture Notes in Computer Science, vol. 10054 (2016), Springer, pp. 68–84.
• [6] W. Buszkowski, Phase Spaces for Involutive Nonassociative Lambek Calculus, [in:] Loukanova, R. and Liefke, K. (eds.), Proc. Logic and Algorithms in Computational Linguistics (LACompLing 2017), Stockholm University, (2017), pp. 21–45.
• [7] N. Galatos and P. Jipsen, Residuated frames with applications to decidability, Transactions of American Mathematical Society 365 (2013), pp. 1219–1249.
• [8] N. Galatos, P. Jipsen, T. Kowalski and H. Ono, Residuated Lattices. An Algebraic Glimpse at Substructural Logics, Elsevier (2007).
• [9] J.-Y. Girard, Linear logic, Theoretical Computer Science 50 (1987), pp. 1–102.
• [10] Ph. de Groote and F. Lamarche, Classical Non-Associative Lambek Calculus, Studia Logica 71/3 (2002), pp. 355–388.
• [11] J. Lambek, On the calculus of syntactic types, [in:] Jakobson, R. (ed.) Structure of Language and Its Mathematical Aspects, pp. 166–178. AMS, Providence (1961).
• [12] J. Lambek, Cut elimination for classical bilinear logic, Fundamenta Informaticae 22 (1995), pp. 53–67.
• [13] J. Lambek, Some lattice models of bilinear logic, Algebra Universalis 34 (1995), pp. 541–550.
• [14] G.Malinowski,Many-valued Logics, Oxford Logic Guides 25, The Clarendon Press, Oxford University Press, 1993.
• [15] M. Okada and K. Terui, The finite model property for various fragments of intuitionistic linear logic, Journal of Symbolic Logic 64 (1999), pp. 790–802.
• [16] M. Pentus, Lambek calculuc is NP-complete, Theoretical Computer Science 357 (2006), pp. 186–201.
• [17] M. Pentus, Lambek calculuc is NP-complete, Theoretical Computer Science 357 (2006), pp. 186–201.

Identyfikatory

DOI

10.18778/0138-0680.46.1.2.07