Involutive Nonassociative Lambek Calculus: Sequent Systems and Complexity

Wojciech Buszkowski

Bulletin of the Section of Logic (2017)

  • Volume: 46, Issue: 1/2
  • ISSN: 0138-0680

Abstract

top
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.

How to cite

top

Wojciech Buszkowski. "Involutive Nonassociative Lambek Calculus: Sequent Systems and Complexity." Bulletin of the Section of Logic 46.1/2 (2017): null. <http://eudml.org/doc/295599>.

@article{WojciechBuszkowski2017,
abstract = {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.},
author = {Wojciech Buszkowski},
journal = {Bulletin of the Section of Logic},
keywords = {nonassociative Lambek calculus; linear logic; sequent system; cut elimination; PTIME complexity},
language = {eng},
number = {1/2},
pages = {null},
title = {Involutive Nonassociative Lambek Calculus: Sequent Systems and Complexity},
url = {http://eudml.org/doc/295599},
volume = {46},
year = {2017},
}

TY - JOUR
AU - Wojciech Buszkowski
TI - Involutive Nonassociative Lambek Calculus: Sequent Systems and Complexity
JO - Bulletin of the Section of Logic
PY - 2017
VL - 46
IS - 1/2
SP - null
AB - 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.
LA - eng
KW - nonassociative Lambek calculus; linear logic; sequent system; cut elimination; PTIME complexity
UR - http://eudml.org/doc/295599
ER -

References

top
  1. [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. [2] A. Bastenhof, Categorial Symmetry, Ph.D. Thesis, University of Utrecht (2013). 
  3. [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. [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. [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. [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. [7] N. Galatos and P. Jipsen, Residuated frames with applications to decidability, Transactions of American Mathematical Society 365 (2013), pp. 1219–1249. 
  8. [8] N. Galatos, P. Jipsen, T. Kowalski and H. Ono, Residuated Lattices. An Algebraic Glimpse at Substructural Logics, Elsevier (2007). 
  9. [9] J.-Y. Girard, Linear logic, Theoretical Computer Science 50 (1987), pp. 1–102. 
  10. [10] Ph. de Groote and F. Lamarche, Classical Non-Associative Lambek Calculus, Studia Logica 71/3 (2002), pp. 355–388. 
  11. [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. [12] J. Lambek, Cut elimination for classical bilinear logic, Fundamenta Informaticae 22 (1995), pp. 53–67. 
  13. [13] J. Lambek, Some lattice models of bilinear logic, Algebra Universalis 34 (1995), pp. 541–550. 
  14. [14] G.Malinowski,Many-valued Logics, Oxford Logic Guides 25, The Clarendon Press, Oxford University Press, 1993. 
  15. [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. [16] M. Pentus, Lambek calculuc is NP-complete, Theoretical Computer Science 357 (2006), pp. 186–201. 
  17. [17] M. Pentus, Lambek calculuc is NP-complete, Theoretical Computer Science 357 (2006), pp. 186–201. 

NotesEmbed ?

top

You must be logged in to post comments.

To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

                
Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.