{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,27]],"date-time":"2026-03-27T19:25:29Z","timestamp":1774639529846,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":34,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783662538258","type":"print"},{"value":"9783662538265","type":"electronic"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2016,11,10]],"date-time":"2016-11-10T00:00:00Z","timestamp":1478736000000},"content-version":"vor","delay-in-days":314,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>In this paper we discuss the use of interactive theorem provers (also called proof assistants) in the study of natural language semantics. It is shown that these provide useful platforms for NL semantics and reasoning on the one hand, and allow experiments to be performed on various frameworks and new theories, on the other. In particular, we show how to use Coq, a prominent type theory based proof assistant, to encode type theoretical semantics of various NL phenomena. In this respect, we can encode the NL semantics based on type theory for quantifiers, adjectives, common nouns, and tense, among others, and it is shown that Coq is a powerful engine for checking the formal validity of these accounts as well as a powerful reasoner about the implemented semantics. We further show some toy semantic grammars for formal semantic systems, like the Montagovian Generative Lexicon, Type Theory with Records and neo-Davidsonian semantics. It is also explained that experiments on new theories can be done as well, testing their validity and usefulness. Our aim is to show the importance of using proof assistants as useful tools in natural language reasoning and verification and argue for their wider application in the field.<\/jats:p>","DOI":"10.1007\/978-3-662-53826-5_6","type":"book-chapter","created":{"date-parts":[[2016,11,9]],"date-time":"2016-11-09T11:59:48Z","timestamp":1478692788000},"page":"85-98","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Proof Assistants for Natural Language Semantics"],"prefix":"10.1007","author":[{"given":"Stergios","family":"Chatzikyriakidis","sequence":"first","affiliation":[]},{"given":"Zhaohui","family":"Luo","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,11,10]]},"reference":[{"key":"6_CR1","unstructured":"Agda proof assistant (2008). http:\/\/appserv.cs.chalmers.se\/users\/ulfn\/wiki\/agda.php"},{"key":"6_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1007\/978-3-662-43742-1_2","volume-title":"Logical Aspects of Computational Linguistics","author":"D Bekki","year":"2014","unstructured":"Bekki, D.: Representing anaphora with dependent types. In: Asher, N., Soloviev, S. (eds.) LACL 2014. LNCS, vol. 8535, pp. 14\u201329. Springer, Heidelberg (2014)"},{"key":"6_CR3","volume-title":"Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism","author":"N de Bruijn","year":"1980","unstructured":"de Bruijn, N.: A survey of the project AUTOMATH. In: Hindley, J., Seldin, J., To, H.B. (eds.) Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism. Academic Press, Cambridge (1980)"},{"key":"6_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1007\/978-3-642-39998-5_10","volume-title":"Formal Grammar","author":"S Chatzikyriakidis","year":"2013","unstructured":"Chatzikyriakidis, S., Luo, Z.: Adjectives in a modern type-theoretical setting. In: Morrill, G., Nederhof, M.-J. (eds.) FG 2012\u20132013. LNCS, vol. 8036, pp. 159\u2013174. Springer, Heidelberg (2013). doi:10.1007\/978-3-642-39998-5_10"},{"issue":"4","key":"6_CR5","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1007\/s10849-014-9208-x","volume":"23","author":"S Chatzikyriakidis","year":"2014","unstructured":"Chatzikyriakidis, S., Luo, Z.: Natural language inference in Coq. J. Log. Lang. Inf. 23(4), 441\u2013480 (2014)","journal-title":"J. Log. Lang. Inf."},{"key":"6_CR6","doi-asserted-by":"crossref","unstructured":"Chatzikyriakidis, S., Luo, Z.: Natural language reasoning using proof-assistant technology: rich typing and beyond. In: Proceedings of EACL 2014 (2014)","DOI":"10.3115\/v1\/W14-1405"},{"key":"6_CR7","unstructured":"Chatzikyriakidis, S., Luo, Z.: Using signatures in type theory to represent situations. In: Logic and Engineering of Natural Language Semantics 11, Tokyo (2014)"},{"key":"6_CR8","doi-asserted-by":"crossref","unstructured":"Chatzikyriakidis, S., Luo, Z.: On the interpretation of common nouns: types v.s. predicates. In: Chatzikyriakidis, S., Luo, Z. (eds.) Modern Perspectives in Type Theoretical Semantics. Studies of Linguistics and Philosophy, Springer, Heidelberg (2016, to appear)","DOI":"10.1007\/978-3-319-50422-3_3"},{"issue":"2","key":"6_CR9","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1093\/logcom\/exi004","volume":"15","author":"R Cooper","year":"2005","unstructured":"Cooper, R.: Records and record types in semantic theory. J. Log. Comput. 15(2), 99\u2013112 (2005)","journal-title":"J. Log. Comput."},{"key":"6_CR10","unstructured":"Cooper, R., Ginzburg, J.: A compositional situation semantics for attitude reports. In: Selignmann, J., Westerstahl, D. (eds.) Logic, Language and Computation, CSLI (1996)"},{"key":"6_CR11","volume-title":"The Coq Proof Assistant Reference Manual (Version 8.1)","author":"The Coq Team","year":"2007","unstructured":"The Coq Team: The Coq Proof Assistant Reference Manual (Version 8.1). Inria, Rennes (2007)"},{"key":"6_CR12","unstructured":"Girard, J.Y.: Interpr\u00e9tation fonctionelle et \u00e9limination des coupures de l\u2019arithm\u00e9tique d\u2019ordre sup\u00e9rieur. Ph.D. thesis, Universit\u00e9 Paris VII (1972)"},{"key":"6_CR13","unstructured":"Gonthier, G.: A computer-checked proof of the Four Colour Theorem (2005). http:\/\/research.microsoft.com\/~gonthier\/4colproof.pdf"},{"key":"6_CR14","doi-asserted-by":"crossref","unstructured":"Kahle, R., Schroeder-Heister, P. (eds.): Proof-Theoretic Semantics. Special Issue of Synthese 148(3), 503\u2013743 (2006)","DOI":"10.1007\/s11229-004-6292-5"},{"key":"6_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/978-3-642-14052-5_22","volume-title":"Interactive Theorem Proving","author":"C Keller","year":"2010","unstructured":"Keller, C., Werner, B.: Importing HOL light into Coq. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 307\u2013322. Springer, Heidelberg (2010). doi:10.1007\/978-3-642-14052-5_22"},{"key":"6_CR16","series-title":"Studies in Linguistics and Philosophy","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/978-94-011-4231-1_14","volume-title":"Computing Meaning","author":"E Krahmer","year":"1999","unstructured":"Krahmer, E., Piwek, P.: Presupposition projection as proof construction. In: Bunt, H., Muskens, R. (eds.) Computing Meaning. SLP, vol. 73, pp. 281\u2013300. Springer, Dordrecht (1999)"},{"key":"6_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"138","DOI":"10.1007\/978-3-662-43742-1_11","volume-title":"Logical Aspects of Computational Linguistics","author":"GE Lungu","year":"2014","unstructured":"Lungu, G.E., Luo, Z.: Monotonicity reasoning in formal semantics based on modern type theories. In: Asher, N., Soloviev, S. (eds.) LACL 2014. LNCS, vol. 8538, pp. 138\u2013148. Springer, Heidelberg (2014)"},{"key":"6_CR18","doi-asserted-by":"crossref","DOI":"10.1093\/oso\/9780198538356.001.0001","volume-title":"Computation and Reasoning: A Type Theory for Computer Science","author":"Z Luo","year":"1994","unstructured":"Luo, Z.: Computation and Reasoning: A Type Theory for Computer Science. Oxford University Press, Oxford (1994)"},{"key":"6_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/3-540-63172-0_45","volume-title":"Computer Science Logic","author":"Z Luo","year":"1997","unstructured":"Luo, Z.: Coercive subtyping in type theory. In: Dalen, D., Bezem, M. (eds.) CSL 1996. LNCS, vol. 1258, pp. 275\u2013296. Springer, Heidelberg (1997). doi:10.1007\/3-540-63172-0_45"},{"key":"6_CR20","doi-asserted-by":"crossref","unstructured":"Luo, Z.: Type-theoretical semantics with coercive subtyping. In: Semantics and Linguistic Theory 20 (SALT20), Vancouver (2010)","DOI":"10.3765\/salt.v20i0.2580"},{"key":"6_CR21","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1007\/978-3-642-22221-4_11","volume-title":"Logical Aspects of Computational Linguistics","author":"Z Luo","year":"2011","unstructured":"Luo, Z.: Contextual analysis of word meanings in type-theoretical semantics. In: Pogodalla, S., Prost, J.-P. (eds.) LACL 2011. LNCS (LNAI), vol. 6736, pp. 159\u2013174. Springer, Heidelberg (2011). doi:10.1007\/978-3-642-22221-4_11"},{"key":"6_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/978-3-642-31262-5_12","volume-title":"Logical Aspects of Computational Linguistics","author":"Z Luo","year":"2012","unstructured":"Luo, Z.: Common nouns as types. In: B\u00e9chet, D., Dikovsky, A. (eds.) LACL 2012. LNCS, vol. 7351, pp. 173\u2013185. Springer, Heidelberg (2012). doi:10.1007\/978-3-642-31262-5_12"},{"issue":"6","key":"6_CR23","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1007\/s10988-013-9126-4","volume":"35","author":"Z Luo","year":"2012","unstructured":"Luo, Z.: Formal semantics in modern type theories with coercive subtyping. Linguist. Philos. 35(6), 491\u2013513 (2012)","journal-title":"Linguist. Philos."},{"key":"6_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1007\/978-3-662-43742-1_14","volume-title":"Logical Aspects of Computational Linguistics","author":"Z Luo","year":"2014","unstructured":"Luo, Z.: Formal semantics in modern type theories: is it model-theoretic, proof-theoretic, or both? In: Asher, N., Soloviev, S. (eds.) LACL 2014. LNCS, vol. 8535, pp. 177\u2013188. Springer, Heidelberg (2014)"},{"key":"6_CR25","unstructured":"Luo, Z., Soloviev, S.: Dependent event types (abstract). In: LACL 2016 (2016)"},{"key":"6_CR26","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1016\/j.ic.2012.10.020","volume":"223","author":"Z Luo","year":"2012","unstructured":"Luo, Z., Soloviev, S., Xue, T.: Coercive subtyping: theory and implementation. Inf. Comput. 223, 18\u201342 (2012)","journal-title":"Inf. Comput."},{"key":"6_CR27","volume-title":"Events in the Semantics of English","author":"T Parsons","year":"1990","unstructured":"Parsons, T.: Events in the Semantics of English. MIT Press, Cambridge (1990)"},{"key":"6_CR28","unstructured":"The Univalent Foundations Program: Homotopy type theory: univalent foundations of mathematics. Technical report, Institute for Advanced Study (2013)"},{"key":"6_CR29","volume-title":"Type-Theoretical Grammar","author":"A Ranta","year":"1994","unstructured":"Ranta, A.: Type-Theoretical Grammar. Oxford University Press, Oxford (1994)"},{"key":"6_CR30","unstructured":"Retor\u00e9, C.: The montagovian generative lexicon Tyn: a type theoretical framework for natural language semantics. In: Matthes, R., Schubert, A. (eds.) 19th International Conference on Types for Proofs and Programs (TYPES 2013), vol. 26, pp. 202\u2013229 (2013)"},{"key":"6_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"408","DOI":"10.1007\/3-540-06859-7_148","volume-title":"Programming Symposium","author":"JC Reynolds","year":"1974","unstructured":"Reynolds, J.C.: Towards a theory of type structure. In: Robinet, B. (ed.) Programming Symposium. LNCS, vol. 19, pp. 408\u2013425. Springer, Heidelberg (1974). doi:10.1007\/3-540-06859-7_148"},{"issue":"3","key":"6_CR32","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1093\/jos\/ffs012","volume":"30","author":"G Sassoon","year":"2013","unstructured":"Sassoon, G.: A typology of multidimensional adjectives. J. Semant. 30(3), 335\u2013380 (2013)","journal-title":"J. Semant."},{"key":"6_CR33","unstructured":"Tanaka, R., Mineshima, K., Bekki, D.: Factivity and presupposition in dependent type semantics. In: Type Theories and Lexical Semantics Workshop (2015)"},{"key":"6_CR34","doi-asserted-by":"publisher","first-page":"1278","DOI":"10.1017\/S0960129514000577","volume":"25","author":"V Voevodsky","year":"2015","unstructured":"Voevodsky, V.: Experimental library of univalent formalization of mathematics. Math. Struct. Comput. Sci. 25, 1278\u20131294 (2015)","journal-title":"Math. Struct. Comput. Sci."}],"container-title":["Lecture Notes in Computer Science","Logical Aspects of Computational Linguistics. Celebrating 20 Years of LACL (1996\u20132016)"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-53826-5_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,7]],"date-time":"2024-03-07T14:21:23Z","timestamp":1709821283000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-662-53826-5_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783662538258","9783662538265"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-53826-5_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"10 November 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"LACL","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Logical Aspects of Computational Linguistics","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Nancy","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2016","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"5 December 2016","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 December 2016","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"lacl2016","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/lacl.gforge.inria.fr\/lacl-2016\/index-presentation.html","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}