Clausal proof nets and discontinuity
Visualitza/Obre
Estadístiques de LA Referencia / Recolecta
Inclou dades d'ús des de 2022
Cita com:
hdl:2117/96810
Tipus de documentReport de recerca
Data publicació1994-03
Condicions d'accésAccés obert
Tots els drets reservats. Aquesta obra està protegida pels drets de propietat intel·lectual i
industrial corresponents. Sense perjudici de les exempcions legals existents, queda prohibida la seva
reproducció, distribució, comunicació pública o transformació sense l'autorització del titular dels drets
Abstract
We consider the task of theorem proving in Lambek calculi and their generalisation to "multimodal residuation calculi". These form an integral part of categorial logic, a logic of signs stemming from categorial grammar, on the basis of which language processing is essentially theorem proving. The demand of this application is not just for efficient processing of some or other specific calculus, but for methods that will be generally applicable to categorial logics. It is proposed that multimodal cases be treated by dealing with the highest common factor of all the connectives as linear (propositional) validity. The prosodic (sublinear) aspects are encoded in labels, in effect the term-structure of quantified linear logic. The correctness condition on proof nets ("long trip condition") can be implemented by SLD resolution in linear logic with unification on labels/terms limited to one-way matching. A suitable unification strategy is obtained for calculi of discontinuity by normalisation of the ground goal term followed by recursive decent and redex pattern-matching on the head term.
CitacióMorrill, G. "Clausal proof nets and discontinuity". 1994.
Forma partLSI-94-21-R
Fitxers | Descripció | Mida | Format | Visualitza |
---|---|---|---|---|
1400191476.pdf | 1,395Mb | Visualitza/Obre |