Proof nets for the multimodal Lambek calculus: From theory to a wide-coverage categorial parser

Abstract

In this chapter, we will extend the proof nets of the previous chapter to the multimodal Lambek calculus discussed in Chapter 5. This means incorporating non-associativity, mode information, unary connectives and structural rules in the proof nets. Fortunately, we will see that there is a single proof net calculus which can handle all these extensions together. The resulting proof nets will be two sided and have a more procedural correctness condition in the form of graph contractions. This correctness condition will also have a modular nature, due to the fact that different grammars may allow different classes of structural rules. These multimodal proof nets form the basis of an implementation and we will discuss the Grail theorem prover in Section 7.2. © 2012 Springer-Verlag Berlin Heidelberg.