{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,18]],"date-time":"2026-04-18T22:57:45Z","timestamp":1776553065164,"version":"3.51.2"},"publisher-location":"Berlin, Heidelberg","reference-count":60,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642224379","type":"print"},{"value":"9783642224386","type":"electronic"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-22438-6_3","type":"book-chapter","created":{"date-parts":[[2011,7,18]],"date-time":"2011-07-18T18:21:44Z","timestamp":1311013304000},"page":"5-25","source":"Crossref","is-referenced-by-count":17,"title":["Translating between Language and Logic: What Is Easy and What Is Difficult"],"prefix":"10.1007","author":[{"given":"Aarne","family":"Ranta","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"3_CR1","unstructured":"Wolfram Research, I.: Mathematica Homepage (2000), http:\/\/www.wolfram.com\/products\/mathematica\/"},{"key":"3_CR2","unstructured":"Bobrow, D.G.: Natural Language Input for a Computer Problem Solving System. PhD thesis, Massachusetts Institute of Technology (1964)"},{"key":"3_CR3","doi-asserted-by":"publisher","first-page":"865","DOI":"10.1016\/S0049-237X(08)70231-3","volume-title":"Selected Papers on Automath","author":"N.G. Bruijn de","year":"1994","unstructured":"de Bruijn, N.G.: Mathematical Vernacular: a Language for Mathematics with Typed Sets. In: Nederpelt, R. (ed.) Selected Papers on Automath, pp. 865\u2013935. North-Holland Publishing Company, Amsterdam (1994)"},{"key":"3_CR4","doi-asserted-by":"crossref","unstructured":"Trybulec, A.: The Mizar Homepage (2006), http:\/\/mizar.org\/","DOI":"10.1007\/11542384_4"},{"key":"3_CR5","series-title":"Lecture Notes in Computer Science","volume-title":"Automated Deduction - CADE-14","author":"C. Benzm\u00fcller","year":"1997","unstructured":"Benzm\u00fcller, C., Cheikhrouhou, L., Fehrer, D., Fiedler, A., Huang, K.M., Kohlhase, M., Konrad, K., Melis, E., Meier, A., Schaarschmidt, W., Siekmann, J., Sorge, V.: Omega: Towards a mathematical assistant. In: McCune, W. (ed.) CADE 1997. LNCS, vol.\u00a01249, Springer, Heidelberg (1997)"},{"key":"3_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/3-540-48256-3_12","volume-title":"Theorem Proving in Higher Order Logics","author":"M. Wenzel","year":"1999","unstructured":"Wenzel, M.: Isar - a generic interpretative approach to readable formal proof documents. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Th\u00e9ry, L. (eds.) TPHOLs 1999. LNCS, vol.\u00a01690, pp. 167\u2013184. Springer, Heidelberg (1999)"},{"key":"3_CR7","unstructured":"Zinn, C.: Understanding Informal Mathematical Discourse. PhD thesis, Department of Computer Science, University of Erlangen-N\u00fcrnberg (2010)"},{"issue":"4","key":"3_CR8","doi-asserted-by":"publisher","first-page":"470","DOI":"10.1016\/j.jal.2005.10.006","volume":"4","author":"B. Buchberger","year":"2006","unstructured":"Buchberger, B., Craciun, A., Jebelean, T., Kov\u00e1cs, L., Kutsia, T., Nakagawa, K., Piroi, F., Popov, N., Robu, J., Rosenkranz, M.: Theorema: Towards computer-aided mathematical theory exploration. J. Applied Logic\u00a04(4), 470\u2013504 (2006)","journal-title":"J. Applied Logic"},{"key":"3_CR9","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1016\/j.entcs.2008.03.063","volume":"205","author":"F. Kamareddine","year":"2008","unstructured":"Kamareddine, F., Wells, J.B.: Computerizing Mathematical Text with MathLang. Electr. Notes Theor. Comput. Sci.\u00a0205, 5\u201330 (2008)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"3_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"170","DOI":"10.1007\/978-3-642-14418-9_11","volume-title":"Controlled Natural Language","author":"M. Cramer","year":"2010","unstructured":"Cramer, M., Fisseni, B., Koepke, P., K\u00fchlwein, D., Schr\u00f6der, B., Veldman, J.: The Naproche Project Controlled Natural Language Proof Checking of Mathematical Texts. In: Fuchs, N.E. (ed.) CNL 2009. LNCS, vol.\u00a05972, pp. 170\u2013186. Springer, Heidelberg (2010)"},{"key":"3_CR11","unstructured":"Neumaier, A.: FMathL - Formal Mathematical Language (2009), http:\/\/www.mat.univie.ac.at\/~neum\/FMathL.html"},{"issue":"2","key":"3_CR12","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1017\/S0956796803004738","volume":"14","author":"A. Ranta","year":"2004","unstructured":"Ranta, A.: Grammatical Framework: A Type-Theoretical Grammar Formalism. The Journal of Functional Programming\u00a014(2), 145\u2013189 (2004), http:\/\/www.cse.chalmers.se\/~aarne\/articles\/gf-jfp.pdf","journal-title":"The Journal of Functional Programming"},{"key":"3_CR13","volume-title":"Grammatical Framework: Programming with Multilingual Grammars","author":"A. Ranta","year":"2011","unstructured":"Ranta, A.: Grammatical Framework: Programming with Multilingual Grammars. CSLI Publications, Stanford (2011) ISBN-10: 1-57586-626-9 (Paper), 1-57586-627-7 (Cloth)"},{"key":"3_CR14","unstructured":"Ranta, A.: Grammatical Framework: A Hands-On Introduction. CADE-23 Tutorial, Wroclaw (2011), http:\/\/www.grammaticalframework.org\/gf-cade-2011\/"},{"key":"3_CR15","unstructured":"Peyton Jones, S.: Haskell 98 language and libraries: the Revised Report (2003), http:\/\/www.haskell.org\/haskellwiki\/Language_and_library_specification"},{"key":"3_CR16","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1016\/0304-3975(91)90374-B","volume":"88","author":"H. Seki","year":"1991","unstructured":"Seki, H., Matsumura, T., Fujii, M., Kasami, T.: On multiple context-free grammars. Theoretical Computer Science\u00a088, 191\u2013229 (1991)","journal-title":"Theoretical Computer Science"},{"key":"3_CR17","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1017\/CBO9780511770524.014","volume-title":"From Semantics to Computer Science. Essays in Honour of Gilles Kahn","author":"A. Ranta","year":"2009","unstructured":"Ranta, A.: Grammars as Software Libraries. In: Bertot, Y., Huet, G., L\u00e9vy, J.J., Plotkin, G. (eds.) From Semantics to Computer Science. Essays in Honour of Gilles Kahn, pp. 281\u2013308. Cambridge University Press, Cambridge (2009), http:\/\/www.cse.chalmers.se\/~aarne\/articles\/libraries-kahn.pdf"},{"key":"3_CR18","unstructured":"Ranta, A.: The GF Resource Grammar Library. Linguistics in Language Technology\u00a02 (2009), http:\/\/elanguage.net\/journals\/index.php\/lilt\/article\/viewFile\/214\/158"},{"key":"3_CR19","unstructured":"Caprotti, O.: WebALT! Deliver Mathematics Everywhere. In: Proceedings of SITE 2006, Orlando, March 20-24 (2006), http:\/\/webalt.math.helsinki.fi\/content\/e16\/e301\/e512\/PosterDemoWebALT_eng.pdf"},{"key":"3_CR20","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1145\/231191.231194","volume":"30","author":"J. Abbott","year":"1996","unstructured":"Abbott, J., D\u00edaz, A., Sutor, R.S.: A report on OpenMath: a protocol for the exchange of mathematical information. SIGSAM Bull\u00a030, 21\u201324 (1996)","journal-title":"SIGSAM Bull"},{"key":"3_CR21","unstructured":"Saludes, J., Xamb\u00f3, S.: MOLTO Mathematical Grammar Library (2010), http:\/\/www.molto-project.eu\/node\/1246"},{"key":"3_CR22","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1007\/11422532_4","volume-title":"Logical Aspects of Computational Linguistics","author":"D.A. Burke","year":"2005","unstructured":"Burke, D.A., Johannisson, K.: Translating Formal Software Specifications to Natural Language \/ A Grammer-Based Approach. In: Blache, P., Stabler, E.P., Busquets, J.V., Moot, R. (eds.) LACL 2005. LNCS (LNAI), vol.\u00a03492, pp. 51\u201366. Springer, Heidelberg (2005), http:\/\/www.springerlink.com\/content\/?k=LNCS+3492"},{"issue":"5-6","key":"3_CR23","doi-asserted-by":"publisher","first-page":"567","DOI":"10.1017\/S0956796808006898","volume":"18","author":"B. Bringert","year":"2008","unstructured":"Bringert, B., Ranta, A.: A Pattern for Almost Compositional Functions. The Journal of Functional Programming\u00a018(5-6), 567\u2013598 (2008)","journal-title":"The Journal of Functional Programming"},{"key":"3_CR24","volume-title":"Formal Philosophy","author":"R. Montague","year":"1974","unstructured":"Montague, R.: Formal Philosophy. Yale University Press, New Haven (1974); Collected papers edited by Richmond Thomason"},{"issue":"2","key":"3_CR25","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1007\/BF00350139","volume":"4","author":"J. Barwise","year":"1981","unstructured":"Barwise, J., Cooper, R.: Generalized quantifiers and natural language. Linguistics and Philosophy\u00a04(2), 159\u2013219 (1981)","journal-title":"Linguistics and Philosophy"},{"key":"3_CR26","unstructured":"Sutcliffe, G., Benzm\u00fcller, C.: Automated Reasoning in Higher-Order Logic using the TPTP THF Infrastructure. Journal of Formalized Reasoning\u00a03 (2010)"},{"key":"3_CR27","volume-title":"Begriffsschrift","author":"G. Frege","year":"1879","unstructured":"Frege, G.: Begriffsschrift. Louis Nebert, Halle A\/S (1879)"},{"key":"3_CR28","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511519857","volume-title":"Building Natural Language Generation Systems","author":"E. Reiter","year":"2000","unstructured":"Reiter, E., Dale, R.: Building Natural Language Generation Systems. Cambridge University Press, Cambridge (2000)"},{"key":"3_CR29","doi-asserted-by":"crossref","unstructured":"Bos, J., Clark, S., Steedman, M., Curran, J.R., Hockenmaier, J.: Wide-Coverage Semantic Representations from a CCG Parser. In: Proceedings of the 20th International Conference on Computational Linguistics (COLING 2004), Geneva, Switzerland, pp. 1240\u20131246 (2004)","DOI":"10.3115\/1220355.1220535"},{"key":"3_CR30","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"404","DOI":"10.1007\/11736790_23","volume-title":"Machine Learning Challenges. Evaluating Predictive Uncertainty, Visual Object Classification, and Recognising Tectual Entailment","author":"J. Bos","year":"2006","unstructured":"Bos, J., Markert, K.: Recognising Textual Entailment with Robust Logical Inference. In: Qui\u00f1onero-Candela, J., Dagan, I., Magnini, B., d\u2019Alch\u00e9-Buc, F. (eds.) MLCW 2005. LNCS (LNAI), vol.\u00a03944, pp. 404\u2013426. Springer, Heidelberg (2006)"},{"key":"3_CR31","doi-asserted-by":"crossref","unstructured":"Angelov, K.: Incremental Parsing with Parallel Multiple Context-Free Grammars. In: Proceedings of EACL 2009, Athens (2009)","DOI":"10.3115\/1609067.1609074"},{"key":"3_CR32","unstructured":"Ganesalingam, M.: The Language of Mathematics. PhD thesis, Department of Computer Science, University of Cambridge (2010), http:\/\/people.pwf.cam.ac.uk\/mg262\/"},{"key":"3_CR33","volume-title":"The Lambda Calculus. Its Syntax and Semantics","author":"H. Barendregt","year":"1981","unstructured":"Barendregt, H.: The Lambda Calculus. Its Syntax and Semantics. North-Holland, Amsterdam (1981)"},{"key":"3_CR34","volume-title":"Type Theoretical Grammar","author":"A. Ranta","year":"1994","unstructured":"Ranta, A.: Type Theoretical Grammar. Oxford University Press, Oxford (1994)"},{"key":"3_CR35","unstructured":"Ljungl\u00f6f, P.: The Expressivity and Complexity of Grammatical Framework. PhD thesis, Dept. of Computing Science, Chalmers University of Technology and Gothenburg University (2004), http:\/\/www.cs.chalmers.se\/~peb\/pubs\/p04-PhD-thesis.pdf"},{"key":"3_CR36","unstructured":"Johannisson, K.: Formal and Informal Software Specifications. PhD thesis, Dept. of Computing Science, Chalmers University of Technology and Gothenburg University (2005)"},{"key":"3_CR37","unstructured":"Angelov, K., Enache, R.: Typeful Ontologies with Direct Multilingual Verbalization. In: Fuchs, N., Rosner, M. (eds.) CNL 2010, Controlled Natural Language (2010)"},{"key":"3_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/BFb0014048","volume-title":"Typed Lambda Calculi and Applications","author":"Y. Coscoy","year":"1995","unstructured":"Coscoy, Y., Kahn, G., Thery, L.: Extracting text from proofs. In: Dezani-Ciancaglini, M., Plotkin, G. (eds.) TLCA 1995. LNCS, vol.\u00a0902, pp. 109\u2013123. Springer, Heidelberg (1995)"},{"key":"3_CR39","unstructured":"Coscoy, Y.: Explication textuelle de preuves pour le calcul des constructions inductives. PhD thesis, Universit\u00e9 de Nice-Sophia-Antipolis (2000)"},{"key":"3_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/978-3-540-24849-1_24","volume-title":"Types for Proofs and Programs","author":"F. Wiedijk","year":"2004","unstructured":"Wiedijk, F.: Formal Proof Sketches. In: Berardi, S., Coppo, M., Damiani, F. (eds.) TYPES 2003. LNCS, vol.\u00a03085, pp. 378\u2013393. Springer, Heidelberg (2004)"},{"key":"3_CR41","volume-title":"Modern Compiler Implementation in ML","author":"A. Appel","year":"1998","unstructured":"Appel, A.: Modern Compiler Implementation in ML. Cambridge University Press, Cambridge (1998)"},{"issue":"2","key":"3_CR42","doi-asserted-by":"publisher","first-page":"358","DOI":"10.1090\/S0002-9947-1953-0053041-6","volume":"74","author":"H.G. Rice","year":"1953","unstructured":"Rice, H.G.: Classes of recursively enumerable sets and their decision problems. Transactions of the American Mathematical Society\u00a074(2), 358\u2013366 (1953)","journal-title":"Transactions of the American Mathematical Society"},{"key":"3_CR43","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/3-540-44404-1_6","volume-title":"Logic for Programming and Automated Reasoning","author":"T. Hallgren","year":"2000","unstructured":"Hallgren, T., Ranta, A.: An Extensible Proof Text Editor. In: Parigot, M., Voronkov, A. (eds.) LPAR 2000. LNCS (LNAI), vol.\u00a01955, pp. 70\u201384. Springer, Heidelberg (2000), http:\/\/www.cse.chalmers.se\/~aarne\/articles\/lpar2000.pdf"},{"key":"3_CR44","doi-asserted-by":"crossref","unstructured":"Dymetman, M., Lux, V., Ranta, A.: XML and multilingual document authoring: Convergent trends. In: Proc. Computational Linguistics COLING, Saarbr\u00fccken, Germany, pp. 243\u2013249. International Committee on Computational Linguistics (2000)","DOI":"10.3115\/990820.990856"},{"key":"3_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1007\/3-540-61780-9_73","volume-title":"Types for Proofs and Programs","author":"A. Ranta","year":"1996","unstructured":"Ranta, A.: Context-relative syntactic categories and the formalization of mathematical text. In: Berardi, S., Coppo, M. (eds.) TYPES 1995. LNCS, vol.\u00a01158, pp. 231\u2013248. Springer, Heidelberg (1996)"},{"key":"3_CR46","first-page":"5","volume":"138\/139","author":"A. Ranta","year":"1997","unstructured":"Ranta, A.: Structures grammaticales dans le fran\u00e7ais math\u00e9matique. Math\u00e9matiques, informatique et Sciences Humaines\u00a0138\/139, 5-56\u20135-36 (1997)","journal-title":"Math\u00e9matiques, informatique et Sciences Humaines"},{"key":"3_CR47","volume-title":"Intuitionistic Type Theory","author":"P. Martin-L\u00f6f","year":"1984","unstructured":"Martin-L\u00f6f, P.: Intuitionistic Type Theory. Bibliopolis, Napoli (1984)"},{"key":"3_CR48","series-title":"Lecture Notes in Computer Science","first-page":"213","volume-title":"Types for Proofs and Programs","author":"L. Magnusson","year":"1995","unstructured":"Magnusson, L., Nordstr\u00f6m, B.: The ALF proof editor and its proof engine. In: Types for Proofs and Programs, pp. 213\u2013237. Springer, Heidelberg (1994)"},{"key":"3_CR49","series-title":"LNCS","volume-title":"Verification of Object-Oriented Software: The KeY Approach","year":"2007","unstructured":"Beckert, B., H\u00e4hnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software. LNCS, vol.\u00a04334. Springer, Heidelberg (2007)"},{"key":"3_CR50","volume-title":"The Object Constraint Language: Precise Modelling with UML","author":"J. Warmer","year":"1999","unstructured":"Warmer, J., Kleppe, A.: The Object Constraint Language: Precise Modelling with UML. Addison-Wesley, London (1999)"},{"key":"3_CR51","unstructured":"Kamp, H., Crouch, R., van Genabith, J., Cooper, R., Poesio, M., van Eijck, J., Jaspars, J., Pinkal, M., Vestre, E., Pulman, S.: Specification of linguistic coverage. FRACAS Deliverable D2 (1994)"},{"key":"3_CR52","unstructured":"Bringert, B.: Semantics of the GF Resource Grammar Library. Report, Chalmers University (2008), http:\/\/www.cse.chalmers.se\/alumni\/bringert\/darcs\/mosg\/"},{"key":"3_CR53","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"104","DOI":"10.1007\/978-3-540-85658-0_3","volume-title":"Reasoning Web","author":"N.E. Fuchs","year":"2008","unstructured":"Fuchs, N.E., Kaljurand, K., Kuhn, T.: Attempto Controlled English for Knowledge Representation. In: Baroglio, C., Bonatti, P.A., Ma\u0142uszy\u0144ski, J., Marchiori, M., Polleres, A., Schaffert, S. (eds.) Reasoning Web. LNCS, vol.\u00a05224, pp. 104\u2013124. Springer, Heidelberg (2008)"},{"key":"3_CR54","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/978-3-642-14418-9_6","volume-title":"Controlled Natural Language","author":"K. Angelov","year":"2010","unstructured":"Angelov, K., Ranta, A.: Implementing Controlled Languages in GF. In: Fuchs, N.E. (ed.) CNL 2009. LNCS, vol.\u00a05972, pp. 82\u2013101. Springer, Heidelberg (2010)"},{"key":"3_CR55","unstructured":"Dean, M., Schreiber, G.: OWL Web Ontology Language Reference (2004), http:\/\/www.w3.org\/TR\/owl-ref\/"},{"key":"3_CR56","unstructured":"Gruzitis, N., Barzdins, G.: Towards a More Natural Multilingual Controlled Language Interface to OWL. In: 9th International Conference on Computational Semantics (IWCS), pp. 335\u2013339 (2011), http:\/\/www.aclweb.org\/anthology\/W\/W11\/W11-0138.pdf"},{"key":"3_CR57","first-page":"2","volume-title":"Proceedings of the International Conference on Formal Ontology in Information Systems (FOIS 2001)","author":"I. Niles","year":"2001","unstructured":"Niles, I., Pease, A.: Towards a standard upper ontology. In: Proceedings of the International Conference on Formal Ontology in Information Systems (FOIS 2001), vol.\u00a02001, pp. 2\u20139. ACM, New York (2001)"},{"key":"3_CR58","doi-asserted-by":"crossref","unstructured":"Humayoun, M., Raffalli, C.: MathNat - Mathematical Text in a Controlled Natural Language. Journal on Research in Computing Science\u00a066 (2010)","DOI":"10.1145\/1943628.1943665"},{"key":"3_CR59","unstructured":"Camilleri, J.J., Pace, G.J., Rosner.: In: Playing Nomic Using a Controlled Natural Language (2010), http:\/\/sunsite.informatik.rwth-aachen.de\/Publications\/CEUR-WS\/Vol-622\/paper7.pdf"},{"key":"3_CR60","unstructured":"Mitankin, P., Ilchev, A.: Knowledge Representation Infrastructure, MOLTO Deliverable D4.1(2010) http:\/\/www.molto-project.eu\/sites\/default\/files\/D4.1_0.pdf"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-23"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-22438-6_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,12]],"date-time":"2019-06-12T23:19:45Z","timestamp":1560381585000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-22438-6_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642224379","9783642224386"],"references-count":60,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-22438-6_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011]]}}}