Rights accessRestricted access - publisher's policy
The count invariance of van Benthem (1991) 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.
CitationValentin Fernandez, J.; Serret, D.; Morrill, G. A count invariant for Lambek calculus with additives and bracket modalities. A: Formal Grammar. "Proceedings of the 18th International Conference on Formal Grammar". Dusseldorf: Springer-Verlag Berlin Heidelberg, 2013, p. 263-276.
All rights reserved. This work is protected by the corresponding intellectual and industrial property rights. Without prejudice to any existing legal exemptions, reproduction, distribution, public communication or transformation of this work are prohibited without permission of the copyright holder. If you wish to make any use of the work not provided for in the law, please contact: firstname.lastname@example.org