Skip to main content
SpringerLink
Log in

The Grail Theorem Prover: Type Theory for Syntax and Semantics

  • Chapter
  • First Online:
Modern Perspectives in Type-Theoretical Semantics

Part of the book series: Studies in Linguistics and Philosophy ((SLAP,volume 98))

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

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 89.00
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 119.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD 119.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

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

    From the point of view of linear logic, we stay within the purely multiplicative fragment, which is simplest proof-theoretically.

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

    Google Scholar 

  • Asher, N. (2011). Lexical meaning in context: A web of words. Cambridge: Cambridge University Press.

    Book  Google Scholar 

  • Bar-Hillel, Y. (1953). A quasi-arithmetical notation for syntactic description. Language, 29(1), 47–58.

    Article  Google Scholar 

  • Barker, C., & Shan, C. (2014). Continuations and natural language. Oxford studies in theoretical linguistics. Oxford: Oxford University Press.

    Google Scholar 

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

    Google Scholar 

  • Chatzikyriakidis, S. (2015). Natural language reasoning using Coq: Interaction and automation. In Proceedings of Traitement Automatique des Langues Naturelles (TALN 2015).

    Google Scholar 

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

    Google Scholar 

  • Danos, V., & Regnier, L. (1989). The structure of multiplicatives. Archive for Mathematical Logic, 28, 181–203.

    Article  Google Scholar 

  • Girard, J. Y. (1987). Linear logic. Theoretical Computer Science, 50, 1–102.

    Article  Google Scholar 

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

    Google Scholar 

  • Girard, J. Y., Lafont, Y., & Regnier, L. (Eds.). (1995).   Advances in linear logic. London mathematical society lecture notes. Cambridge: Cambridge University Press.

    Google Scholar 

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

    Google Scholar 

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

    Google Scholar 

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

    Google Scholar 

  • Lambek, J. (1958). The mathematics of sentence structure. American Mathematical Monthly, 65, 154–170.

    Article  Google Scholar 

  • Luo, Z. (2012a). Common nouns as types. Logical aspects of computational linguistics (LACL2012) (Vol. 7351). Lecture notes in artificial intelligence. New York: Springer.

    Google Scholar 

  • Luo, Z. (2012b). Formal semantics in modern type theories with coercive subtyping. Linguistics and Philosophy, 35(6), 491–513.

    Google Scholar 

  • Luo, Z. (2015). A Lambek calculus with dependent types. In Types for Proofs and Programs (TYPES 2015), Tallinn.

    Google Scholar 

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

    Google Scholar 

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

    Google Scholar 

  • Montague, R. (1970). Universal grammar. Theoria, 36(3), 373–398.

    Article  Google Scholar 

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

    Google Scholar 

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

    Google Scholar 

  • Moortgat, M., & Oehrle, R. T. (1994). Adjacency, dependency and order. In Proceedings 9th Amsterdam Colloquium (pp. 447–466).

    Google Scholar 

  • Moot, R. (2008). Filtering axiom links for proof nets. Technical report, CNRS and Bordeaux University.

    Google Scholar 

  • Moot, R. (2010). Wide-coverage French syntax and semantics using Grail. In Proceedings of Traitement Automatique des Langues Naturelles (TALN), Montreal, system Demo.

    Google Scholar 

  • Moot, R. (2012). Wide-coverage semantics for spatio-temporal reasoning. Traitement Automatique des Languages, 53(2), 115–142.

    Google Scholar 

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

    Article  Google Scholar 

  • Moot, R., & Puite, Q. (2002). Proof nets for the multimodal Lambek calculus. Studia Logica, 71(3), 415–442.

    Article  Google Scholar 

  • Moot, R., & Retoré, C. (2011). Second order lambda calculus for meaning assembly: On the logical syntax of plurals. In Computing Natural Reasoning (COCONAT), Tilburg.

    Google Scholar 

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

    Google Scholar 

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

    Google Scholar 

  • Murawski, A. S., & Ong, C. H. L. (2000). Dominator trees and fast verification of proof nets. Logic in Computer Science (pp. 181–191).

    Google Scholar 

  • Oehrle, R. T. (1994). Term-labeled categorial type systems. Linguistics & Philosophy, 17(6), 633–678.

    Article  Google Scholar 

  • Pentus, M. (1997). Product-free Lambek calculus and context-free grammars. Journal of Symbolic Logic, 62, 648–660.

    Article  Google Scholar 

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

    Google Scholar 

  • Pustejovsky, J. (1995). The generative lexicon. Cambridge: M.I.T Press.

    Google Scholar 

  • Ranta, A. (1991). Intuitionistic categorial grammar. Linguistics and Philosophy, 14(2), 203–239.

    Article  Google Scholar 

  • Shieber, S. (1985). Evidence against the context-freeness of natural language. Linguistics & Philosophy, 8, 333–343.

    Google Scholar 

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

    Google Scholar 

  • van Benthem, J. (1995). Language in action: Categories. Lambdas and dynamic logic. Cambridge, Massachusetts: MIT Press.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. CNRS, LaBRI, Bordeaux University, 351 cours de la Libération, 33405, Talence, France

    Richard Moot

  2. LIRMM, Montpellier University, 161 rue Ada, 34095, Montpellier Cedex 5, France

    Richard Moot

Authors
  1. Richard Moot
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Richard Moot .

Editor information

Editors and Affiliations

  1. University of Gothenburg, Sweden & Open University Cyprus, Gothenburg, Sweden

    Stergios Chatzikyriakidis

  2. Dept. of Computer Science, University of London Royal Holloway, London, United Kingdom

    Zhaohui Luo

Rights and permissions

Reprints 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)

Publish with us

Policies and ethics

Search

Navigation