A Count Invariant for Lambek Calculus with Additives and Bracket Modalities

  • Oriol Valentín
  • Daniel Serret
  • Glyn Morrill
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8036)


The count invariance of van Benthem (1991[16]) is that for a sequent to be a theorem of the Lambek calculus, for each atom, the number of positive occurrences equals the number of negative occurrences. (The same is true for multiplicative linear logic.) The count invariance provides for extensive pruning of the sequent proof search space. In this paper we generalize count invariance to categorial grammar (or linear logic) with additives and bracket modalities. We define by mutual recursion two counts, minimum count and maximum count, and we prove that if a multiplicative-additive sequent is a theorem, then for every atom, the minimum count is less than or equal to zero and the maximum count is greater than or equal to zero; in the case of a purely multiplicative sequent, minimum count and maximum count coincide in such a way as to together reconstitute the van Benthem count criterion. We then define in the same way a bracket count providing a count check for bracket modalities. This allows for efficient pruning of the sequent proof search space in parsing categorial grammar with additives and bracket modalities.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Andreoli, J.M.: Logic programming with focusing in linear logic. Journal of Logic and Computation 2(3), 297–347 (1992)MathSciNetzbMATHCrossRefGoogle Scholar
  2. 2.
    Girard, J.-Y.: Linear logic. Theoretical Computer Science 50, 1–102 (1987)MathSciNetzbMATHCrossRefGoogle Scholar
  3. 3.
    Hendriks, H.: Studied flexibility. Categories and types in syntax and semantics. PhD thesis, Universiteit van Amsterdam. ILLC, Amsterdam (1993)Google Scholar
  4. 4.
    Hepple, M.: Normal form theorem proving for the Lambek calculus. In: Karlgren, H. (ed.) Proceedings of COLING, Stockholm (1990)Google Scholar
  5. 5.
    Kanazawa, M.: The Lambek calculus enriched with additional connectives. Journal of Logic, Language and Information 1, 141–171 (1992)MathSciNetzbMATHCrossRefGoogle Scholar
  6. 6.
    König, E.: Parsing as natural deduction. In: Proceedings of the Annual Meeting of the Association for Computational Linguistics, Vancouver (1989)Google Scholar
  7. 7.
    Lambek, J.: On the Calculus of Syntactic Types. In: Jakobson, R. (ed.) Structure of Language and its Mathematical Aspects, Proceedings of the Symposia in Applied Mathematics XII, pp. 166–178. American Mathematical Society, Providence (1961)CrossRefGoogle Scholar
  8. 8.
    Moortgat, M.: Multimodal linguistic inference. Journal of Logic, Language and Information 5(3,4), 371–401 (1996); Also in Bulletin of the IGPL 3(2,3), 371–401 (1995)Google Scholar
  9. 9.
    Morrill, G.: Grammar and Logical Types. In: Stockhof, M., Torenvliet, L. (eds.) Proceedings of the Seventh Amsterdam Colloquium, pp. 429–450 (1990); Barry, G., Morrill, G.: Studies in Categorial Grammar, Edinburgh Working Papers in Cognitive Science, vol. 5, pp. 127–148 (1990); Revised version published as Grammar and Logic. Theoria, LXII 3, 260–293 (1996)Google Scholar
  10. 10.
    Morrill, G.: Categorial Formalisation of Relativisation: Pied Piping, Islands, and Extraction Sites. Technical Report LSI-92-23-R, Departament de Llenguatges i Sistemes Informàtics, Universitat Politècnica de Catalunya (1992)Google Scholar
  11. 11.
    Morrill, G.: Logic Programming of the Displacement Calculus. In: Pogodalla, S., Prost, J.-P. (eds.) LACL 2011. LNCS, vol. 6736, pp. 175–189. Springer, Heidelberg (2011)Google Scholar
  12. 12.
    Morrill, G.: CatLog: A Categorial Parser/Theorem-Prover. In: LACL 2012 System Demonstrations, Logical Aspects of Computational Linguistics 2012, Nantes, pp. 13–16 (2012)Google Scholar
  13. 13.
    Morrill, G., Valentín, O., Fadda, M.: The Displacement Calculus. Journal of Logic, Language and Information 20(1), 1–48 (2011), doi:10.1007/s10849-010-9129-2.MathSciNetzbMATHCrossRefGoogle Scholar
  14. 14.
    Morrill, G.V.: Type Logical Grammar: Categorial Logic of Signs. Kluwer Academic Publishers, Dordrecht (1994)zbMATHCrossRefGoogle Scholar
  15. 15.
    Morrill, G.V.: Categorial Grammar: Logical Syntax, Semantics, and Processing. Oxford University Press, New York and Oxford (2011)Google Scholar
  16. 16.
    van Benthem, J.: Language in Action: Categories, Lambdas, and Dynamic Logic. Number 130 in Studies in Logic and the Foundations of Mathematics. North-Holland, Amsterdam (1991); (revised student edition printed in 1995 by the MIT Press)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2013

Authors and Affiliations

  • Oriol Valentín
    • 1
  • Daniel Serret
    • 2
  • Glyn Morrill
    • 1
  1. 1.Universitat Politècnica de CatalunyaSpain
  2. 2.Universitat de BarcelonaSpain

Personalised recommendations