Proof-theoretic methods in natural language processing
Course description |
A set of course notes with exercises is available for printing.
The links to electronic reading materials will be updated soon. Links to Springer Lecture
Notes publications are available from within the UU domain.
This course focuses on computational aspects of type logical
grammars and related formalisms, and on the relevance of
proposed computational models for human language processing.
a companion course,
we have presented grammatical derivations
in the Gentzen calculus and in the Natural Deduction format. From a
computational point of view, these formats are problematic. Natural
Deduction is good for the presentation of proofs once they have been found,
but it doesn't offer pleasant proof search facilities. Gentzen calculus
does have a nice backward chaining proof search interpretation, but it is
inefficient as a result of spurious non-determinism: there can be different
derivations that compute one and the same meaning. Moreover, these two
formats do not address the left-to-right incrementality of human language
processing, and the various performance phenomena related to it.
The proof-net approach of Linear offers interesting features to
deal with such processing issues. Proof nets are graphs satisfying certain
well-formedness conditions. You can view a proof net as a 'parallellized'
derivation: nets capture the essence of a derivation without redundant
choice points. The original well-formedness conditions
for proof nets check for resource multiplicity:
every resource has to be used exactly once. The challenge, in adapting the
for NLP purposes, is to introduce additional constraints to also check
the relevant aspects of grammatical structure. One way of
doing that is to decorate the nodes in a proof structure graph with terms
taken from an algebra of structural labels.
Alternatively, one can build in the structural factors directly in the
graph-theoretic characterization of nets.
In the first part of the course (Week 1 to Week 3), we study the technical
aspects of proof nets. In the second part of the course, we look at
proposals for incremental proof net constructions, and their relevance
for human language processing issues. Also we investigate the trade-off between
expressivity and processing efficiency for some approximations of the
full grammar logic.
To earn the credits for this course, participants have to fulfill two
A tentative course schedule is given below, together with the reading
- During the course, a number of quizzes test your understanding of the
literature discussed in class. These tests stand for 6/10 of the total course credit.
- There is a class presentation of an individual piece of work.
The presentations take one hour (discussion included). The subject can
be a critical evaluation of a literature item or a computational
exploration of an aspect of the course. The grading for this component
determines the remaining 4/10 of the course credit.
Week 1. Basics
- Michael Moortgat, `Categorial parsing as deduction', Section 7 of
Chapter 2 `Categorial type logics', in Van Benthem and ter Meulen (eds.)
Handbook of Logic and Language, Elsevier/MIT Press, pp 163-170.
- F. Lamarche and Christian Retoré, `Proof nets for the
Lambek calculus - an overview'.
In V. Michele Abrusci and Claudia Casadio (eds.)
Proceedings of the 1996 Roma Workshop
`Proofs and Linguistic Categories.
Applications of Logic to the Analysis and Implementation of Natural Language',
Roma, April 10-13, 1996. CLUEB, Bologna, pp. 241--262.
Week 2. Proof nets and semantic readings
- Philippe de Groote and Christian Retoré,
`On the semantic readings of proof nets'
In G.-J. Kruijff, G. Morrill, D. Oehrle, editors,
Formal Grammar, FoLLI, p. 57-70, Prague, August 1996.
PDF alleen voor printen: geen Type 1 fonts)
- Philippe de Groote,
`An algebraic correctness criterion for intuitionistic proof nets'.
To appear in Theoretical Computer Science.
Week 3. Proofs nets for structured grammatical resources
- Michael Moortgat, 1999,
Labelled deduction in the composition of grammatical form and meaning.
In Reyle e.a. (eds.) Festschrift Dov Gabbay.
- A simple introduction to Richard Moot's proofnets for
multimodal categorial grammar can be found in Moortgat and Moot's
paper for CLIN 2000.
There is a mid-course take-home quiz to test your understanding of
the technical material so far.
From this point on, the course can move in a number of directions,
depending on the interests of the participants. Some possible topics
for further exploration:
Proof nets and incremental processing
Incremental parsing for pregroup grammars
- Joachim Lambek, 1999, Type grammar revisited.
Proceedings LACL97. Springer Lecture Notes in Computer Science 1582.
- Willemijn Vermaat, 1999, The minimalist move operation in a
deductive perspective. In Retoré and Stabler (eds.) Resource
Logics and Minimalist Grammar. Proceedings ESSLLI'99 Workshop.
- Willemijn Vermaat, 2002, Inflection: MG versus TLG. Slides van een
- Ed Stabler, 1998, Derivational Minimalism. Proceedings LACL'97,
Springer LNAI 1328.
The proof-net facilities of GRAIL serve as course-ware for
this module. You need an account on salto.let.uu.nl to make use
of the GUI. Here are some useful links.
- Michael Moortgat 2001, Structural equations in language learning.
Proceedings LACL 2001, Springer Lecture Notes in Artifical Intelligence 2099,
pp 1-16. (PDF)
Back to the top
- Marthe Dekker (pdf)
- Eric Auer (pdf)
- Sietske Gorter (pdf)