Mostra el registre d'ítem simple
A count invariant for Lambek calculus with additives and bracket modalities
dc.contributor.author | Valentín Fernández Gallart, José Oriol |
dc.contributor.author | Serret, Daniel |
dc.contributor.author | Morrill, Glyn |
dc.contributor.other | Universitat Politècnica de Catalunya. Departament de Llenguatges i Sistemes Informàtics |
dc.date.accessioned | 2013-10-09T12:02:14Z |
dc.date.created | 2013 |
dc.date.issued | 2013 |
dc.identifier.citation | Valentin 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. |
dc.identifier.isbn | 978-364239997-8 |
dc.identifier.uri | http://hdl.handle.net/2117/20347 |
dc.description.abstract | 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. |
dc.format.extent | 14 p. |
dc.language.iso | eng |
dc.publisher | Springer-Verlag Berlin Heidelberg |
dc.subject | Àrees temàtiques de la UPC::Informàtica::Informàtica teòrica::Algorísmica i teoria de la complexitat |
dc.subject.lcsh | Invariant (mathematics) |
dc.subject.other | Categorial grammar |
dc.subject.other | Lambek calculus |
dc.subject.other | Linear logic |
dc.subject.other | Multiplicative linear logic |
dc.subject.other | Mutual recursion |
dc.subject.other | Proof search |
dc.title | A count invariant for Lambek calculus with additives and bracket modalities |
dc.type | Conference report |
dc.subject.lemac | Invariants |
dc.contributor.group | Universitat Politècnica de Catalunya. LARCA - Laboratori d'Algorísmia Relacional, Complexitat i Aprenentatge |
dc.identifier.doi | 10.1007/978-3-642-39998-5_17 |
dc.description.peerreviewed | Peer Reviewed |
dc.rights.access | Restricted access - publisher's policy |
local.identifier.drac | 12793291 |
dc.description.version | Postprint (published version) |
dc.date.lift | 10000-01-01 |
local.citation.author | Valentin Fernandez, J.; Serret, D.; Morrill, G. |
local.citation.contributor | Formal Grammar |
local.citation.pubplace | Dusseldorf |
local.citation.publicationName | Proceedings of the 18th International Conference on Formal Grammar |
local.citation.startingPage | 263 |
local.citation.endingPage | 276 |