Abstract
Type-logical grammars use a foundation of logic and type theory to model natural language. These grammars have been particularly successful giving an account of several well-known phenomena on the syntax-semantics interface, such as quantifier scope and its interaction with other phenomena. This chapter gives a high-level description of a family of theorem provers designed for grammar development in a variety of modern type-logical grammars. We discuss automated theorem proving for type-logical grammars from the perspective of proof nets, a graph-theoretic way to represent (partial) proofs during proof search.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
This is rather different from Montague’s use of the term “Universal Grammar” (Montague 1970). In Montague’s sense, the different components of a type-logical grammar together would be an instantiation of Universal Grammar.
- 2.
Many authors use a single designated goal formula, typically s, as is standard in formal language theory. I prefer this slightly more general setup, since it allows us to distinguish between, for example, declarative sentences, imperatives, yes/no questions, wh questions, etc., both syntactically and semantically.
- 3.
We have used the standard convention in Montague grammar of writing \((p\, x)\) as p(x) and \(((p\,y)\,x)\) as p(x, y), for a predicate symbol p.
- 4.
We can also allow unary branches (and, more generally n-ary branches) and the corresponding logical connectives. The unary connectives \(\Diamond \) and \(\Box \) are widely used, but, since they will only play a marginal role in what follows, I will not present them to keep the current presentation simple. However, they form an essential part of the analysis of many phenomena and are consequently available in the implementation.
- 5.
We make a slight simplification here. A single vertex abstract proof structure can have both a hypothesis and a conclusion without these two formulas necessarily being identical, e.g. for sequents like \((a/b)\bullet b\vdash a\). Such a sequent would correspond to the abstract proof structure \(\overset{(a/b)\bullet b}{\underset{a}{\cdot }}\). So, formally, both the hypotheses and the conclusions of an abstract proof structure are assigned a formula and when a node is both a hypothesis and a conclusion it can be assigned two different formulas. In order not to make the notation of abstract proof structure more complex, we will stay with the simpler notation. Moot and Puite (2002) present the full details.
- 6.
From the point of view of linear logic, we stay within the purely multiplicative fragment, which is simplest proof-theoretically.
- 7.
Lexical ambiguity is a major problem for automatically extracted wide-coverage grammars as well, though standard statistical methods can help alleviate this problem (Moot 2010).
- 8.
As discussed in Sect. 4.1, the multimodal theorem prover allows the grammar writer to specify first-order approximations of specific formulas. So underneath the surface of Grail there is some first-order reasoning going on as well.
References
Ajdukiewicz, K. (1935). Die syntaktische Konnexität. Studies in Philosophy, 1, 1–27.
Asher, N. (2011). Lexical meaning in context: A web of words. Cambridge: Cambridge University Press.
Bar-Hillel, Y. (1953). A quasi-arithmetical notation for syntactic description. Language, 29(1), 47–58.
Barker, C., & Shan, C. (2014). Continuations and natural language. Oxford studies in theoretical linguistics. Oxford: Oxford University Press.
Bassac, C., Mery, B., & Retoré, C. (2010). Towards a type-theoretical account of lexical semantics. Journal of Logic, Language and Information, 19(2), 229–245. doi:10.1007/s10849-009-9113-x.
Carpenter, B. (1994). A natural deduction theorem prover for type-theoretic categorial grammars. Technical report, Carnegie Mellon Laboratory for Computational Linguistics, Pittsburgh, Pennsylvania.
Chatzikyriakidis, S. (2015). Natural language reasoning using Coq: Interaction and automation. In Proceedings of Traitement Automatique des Langues Naturelles (TALN 2015).
Danos, V. (1990). La logique linéaire appliquée à l’étude de divers processus de normalisation (principalement du \(\lambda \)-calcul). Ph.D. thesis, University of Paris VII.
Danos, V., & Regnier, L. (1989). The structure of multiplicatives. Archive for Mathematical Logic, 28, 181–203.
Girard, J. Y. (1987). Linear logic. Theoretical Computer Science, 50, 1–102.
Girard, J. Y. (1991). Quantifiers in linear logic II. In G. Corsi & G. Sambin (Eds.), Nuovi problemi della logica e della filosofia della scienza, CLUEB, Bologna, Italy, vol II, Proceedings of the Conference with the Same Name, Viareggio, Italy, January 1990.
Girard, J. Y., Lafont, Y., & Regnier, L. (Eds.). (1995). Advances in linear logic. London mathematical society lecture notes. Cambridge: Cambridge University Press.
Guerrini, S. (1999). Correctness of multiplicative proof nets is linear. In Fourteenth Annual IEEE Symposium on Logic in Computer Science, IEEE Computer Science Society (pp. 454–263).
Huijbregts, R. (1984). The weak inadequacy of context-free phrase structure grammars. In G. de Haan, M. Trommelen, & W. Zonneveld (Eds.), Van Periferie naar Kern. Dordrecht: Foris.
Knuth, D. E. (2000). Dancing links. arXiv:cs/0011047.
Kubota, Y., & Levine, R. (2012). Gapping as like-category coordination. In D. Béchet & A. Dikovsky (Eds.), Logical aspects of computational linguistics (Vol. 7351, pp. 135–150). Lecture notes in computer science. Nantes: Springer.
Lambek, J. (1958). The mathematics of sentence structure. American Mathematical Monthly, 65, 154–170.
Luo, Z. (2012a). Common nouns as types. Logical aspects of computational linguistics (LACL2012) (Vol. 7351). Lecture notes in artificial intelligence. New York: Springer.
Luo, Z. (2012b). Formal semantics in modern type theories with coercive subtyping. Linguistics and Philosophy, 35(6), 491–513.
Luo, Z. (2015). A Lambek calculus with dependent types. In Types for Proofs and Programs (TYPES 2015), Tallinn.
Mery, B., Moot, R., & Retoré, C. (2013). Plurals: Individuals and sets in a richly typed semantics. In The Tenth International Workshop of Logic and Engineering of Natural Language Semantics 10 (LENLS10).
Mineshima, K., Martínez-Gómez, P., Miyao, Y., & Bekki, D. (2015). Higher-order logical inference with compositional semantics. In Proceedings of Empirical Method for Natural Language Processing (EMNLP 2015).
Montague, R. (1970). Universal grammar. Theoria, 36(3), 373–398.
Montague, R. (1974). The proper treatment of quantification in ordinary English. In R. Thomason (Ed.), Formal philosophy. Selected papers of Richard Montague. New Haven: Yale University Press.
Moortgat, M. (2011). Categorial type logics. In J. van Benthem & A. ter Meulen (Eds.), Handbook of logic and language (pp. 95–179). Amsterdam: North-Holland Elsevier.
Moortgat, M., & Oehrle, R. T. (1994). Adjacency, dependency and order. In Proceedings 9th Amsterdam Colloquium (pp. 447–466).
Moot, R. (2008). Filtering axiom links for proof nets. Technical report, CNRS and Bordeaux University.
Moot, R. (2010). Wide-coverage French syntax and semantics using Grail. In Proceedings of Traitement Automatique des Langues Naturelles (TALN), Montreal, system Demo.
Moot, R. (2012). Wide-coverage semantics for spatio-temporal reasoning. Traitement Automatique des Languages, 53(2), 115–142.
Moot, R. (2015a). Grail. https://github.com/RichardMoot/Grail, mature and flexible parser for multimodal grammars.
Moot, R. (2015b). Grail light. https://github.com/RichardMoot/GrailLight, fast, lightweight version of the Grail parser.
Moot, R. (2015c). Linear one: A theorem prover for first-order linear logic. https://github.com/RichardMoot/LinearOne.
Moot, R., & Piazza, M. (2001). Linguistic applications of first order multiplicative linear logic. Journal of Logic, Language and Information, 10(2), 211–232.
Moot, R., & Puite, Q. (2002). Proof nets for the multimodal Lambek calculus. Studia Logica, 71(3), 415–442.
Moot, R., & Retoré, C. (2011). Second order lambda calculus for meaning assembly: On the logical syntax of plurals. In Computing Natural Reasoning (COCONAT), Tilburg.
Moot, R., & Retoré, C. (2012). The logic of categorial grammars: A deductive account of natural language syntax and semantics (Vol. 6850). Lecture notes in artificial intelligence. New York: Springer.
Moot, R., Schrijen, X., Verhoog, G. J., Moortgat, M. (2015). Grail0: A theorem prover for multimodal categorial grammars. https://github.com/RichardMoot/Grail0.
Morrill, G., Valentín, O., & Fadda, M. (2011). The displacement calculus. Journal of Logic, Language and Information, 20(1), 1–48.
Murawski, A. S., & Ong, C. H. L. (2000). Dominator trees and fast verification of proof nets. Logic in Computer Science (pp. 181–191).
Oehrle, R. T. (1994). Term-labeled categorial type systems. Linguistics & Philosophy, 17(6), 633–678.
Pentus, M. (1997). Product-free Lambek calculus and context-free grammars. Journal of Symbolic Logic, 62, 648–660.
Pogodalla, S., & Pompigne, F. (2012). Controlling extraction in abstract categorial grammars. In P. de Groote & M. J. Nederhof (Eds.), Proceedings of formal grammar 2010–2011 (Vol. 7395, pp. 162–177). LNCS. New York: Springer.
Pustejovsky, J. (1995). The generative lexicon. Cambridge: M.I.T Press.
Ranta, A. (1991). Intuitionistic categorial grammar. Linguistics and Philosophy, 14(2), 203–239.
Shieber, S. (1985). Evidence against the context-freeness of natural language. Linguistics & Philosophy, 8, 333–343.
Valentín, O. (2014). The hidden structural rules of the discontinuous Lambek calculus. In C. Casadio, B. Coecke, M. Moortgat, & P. Scott (Eds.), Categories and types in logic, language, and physics: Essays dedicated to Jim Lambek on the occasion of this 90th birthday (Vol. 8222, pp. 402–420). Lecture notes in artificial intelligence. New York: Springer.
van Benthem, J. (1995). Language in action: Categories. Lambdas and dynamic logic. Cambridge, Massachusetts: MIT Press.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this chapter
Cite this chapter
Moot, R. (2017). The Grail Theorem Prover: Type Theory for Syntax and Semantics. In: Chatzikyriakidis, S., Luo, Z. (eds) Modern Perspectives in Type-Theoretical Semantics. Studies in Linguistics and Philosophy, vol 98. Springer, Cham. https://doi.org/10.1007/978-3-319-50422-3_10
Download citation
DOI: https://doi.org/10.1007/978-3-319-50422-3_10
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-50420-9
Online ISBN: 978-3-319-50422-3
eBook Packages: Social SciencesSocial Sciences (R0)