Docent
| Michael Moortgat |

moortgat@let.uu.nl | |

Courseware
| Richard Moot |

Richard.Moot@let.uu.nl |

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.

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
nets
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.

- 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.

- 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. (PDF)
- 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. (Postscript)

- 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. (Postscript, 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. (Postscript)

- Michael Moortgat, 1999, Labelled deduction in the composition of grammatical form and meaning. In Reyle e.a. (eds.) Festschrift Dov Gabbay. Kluwer, 1999. (Postscript)
- 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:- Mark Johnson (1998) Proof nets and the complexity of processing center embedded constructions. JoLLI 7:433-447.
- Glyn Morrill (2000) Incremental processing and acceptability. Computational Linguistics 26(3):319-338

- Joachim Lambek, 1999, Type grammar revisited. Proceedings LACL97. Springer Lecture Notes in Computer Science 1582. (PDF)

- 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. (PDF)
- Willemijn Vermaat, 2002, Inflection: MG versus TLG. Slides van een presentatie.
- Ed Stabler, 1998, Derivational Minimalism. Proceedings LACL'97, Springer LNAI 1328. (PDF)

- Michael Moortgat 2001, Structural equations in language learning. Proceedings LACL 2001, Springer Lecture Notes in Artifical Intelligence 2099, pp 1-16. (PDF)

- The GRAIL user manual (PDF).
- Richard Moot's contribution for `Calculemus and Types 98: User Interfaces for Theorem Provers' discusses the underlying computational architecture. (Postscript)