{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,13]],"date-time":"2026-07-13T23:27:04Z","timestamp":1783985224563,"version":"3.55.0"},"reference-count":32,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2016,6,11]],"date-time":"2016-06-11T00:00:00Z","timestamp":1465603200000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100000735","name":"University of Cambridge","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100000735","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2017,2]]},"DOI":"10.1007\/s10817-016-9377-1","type":"journal-article","created":{"date-parts":[[2016,6,11]],"date-time":"2016-06-11T03:58:18Z","timestamp":1465617498000},"page":"253-291","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":33,"title":["A Fully Automatic Theorem Prover with Human-Style Output"],"prefix":"10.1007","volume":"58","author":[{"given":"M.","family":"Ganesalingam","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"W. T.","family":"Gowers","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2016,6,11]]},"reference":[{"key":"9377_CR1","volume-title":"Logics of Conversation","author":"N Asher","year":"2003","unstructured":"Asher, N., Lascarides, A.: Logics of Conversation. Cambridge University Press, Cambridge (2003)"},{"key":"9377_CR2","doi-asserted-by":"crossref","unstructured":"Ballantyne, A.M., Bledsoe, W.W.: Automatic proofs of theorems in analysis using non-standard techniques. J. ACM 24(3), 353\u2013374 (1977)","DOI":"10.1145\/322017.322018"},{"key":"9377_CR3","doi-asserted-by":"crossref","unstructured":"Beeson, M.: Automatic generation of epsilon-delta proofs of continuity. In: Calmet, J., Plaza, J.A. (eds.) Proceedings of the International Conference on Artificial Intelligence and Symbolic Computation (AISC \u201998), pp. 67\u201383. Springer, London, UK (1998)","DOI":"10.1007\/BFb0055903"},{"issue":"4","key":"9377_CR4","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1006\/jsco.2000.0465","volume":"32","author":"M Beeson","year":"2001","unstructured":"Beeson, M.: Automatic derivation of the irrationality of e. J. Symbol. Comput. 32(4), 333\u2013349 (2001)","journal-title":"J. Symbol. Comput."},{"issue":"1","key":"9377_CR5","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1016\/0004-3702(71)90004-X","volume":"2","author":"WW Bledsoe","year":"1971","unstructured":"Bledsoe, W.W.: Splitting and reduction heuristics in automatic theorem proving. Artif. Intell. 2(1), 55\u201377 (1971)","journal-title":"Artif. Intell."},{"issue":"1","key":"9377_CR6","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0004-3702(77)90012-1","volume":"9","author":"WW Bledsoe","year":"1977","unstructured":"Bledsoe, W.W.: Non-resolution theorem proving. Artif. Intell. 9(1), 1\u201335 (1977)","journal-title":"Artif. Intell."},{"key":"9377_CR7","unstructured":"Bledsoe, W.W.: Set variables. In: Proceedings of the 5th International Joint Conference on Artificial Intelligence-Volume 1, pp. 501\u2013510. Morgan Kaufmann Publishers Inc., San Francisco, CA. http:\/\/dl.acm.org\/citation.cfm?id=1624548 (1977)"},{"key":"9377_CR8","unstructured":"Bledsoe, W.W.: Using examples to generate instantiations for set variables. In: Proceedings of IJCAI, vol.\u00a083, pp. 892\u2013901 (1983)"},{"issue":"1","key":"9377_CR9","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1016\/0303-2647(94)01453-E","volume":"34","author":"WW Bledsoe","year":"1995","unstructured":"Bledsoe, W.W.: A precondition prover for analogy. BioSystems 34(1), 225\u2013247 (1995)","journal-title":"BioSystems"},{"key":"9377_CR10","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1016\/0004-3702(72)90041-0","volume":"3","author":"WW Bledsoe","year":"1972","unstructured":"Bledsoe, W.W., Boyer, R.S., Henneman, W.H.: Computer proofs of limit theorems. Artif. Intell. 3, 27\u201360 (1972)","journal-title":"Artif. Intell."},{"key":"9377_CR11","doi-asserted-by":"crossref","unstructured":"Bledsoe, W.W., Hodges, R.: A survey of automated deduction. In: Shrobe, H. (ed.) Exploring Artificial Intelligence, pp. 483\u2013541. Morgan Kaufmann Publishers Inc., San Mateo, CA (1988)","DOI":"10.1016\/B978-0-934613-67-5.50017-4"},{"key":"9377_CR12","volume-title":"A Computational Logic","author":"RS Boyer","year":"1979","unstructured":"Boyer, R.S., Moore, J.S.: A Computational Logic. Academic Press, ACM Monograph, Cambridge (1979)"},{"issue":"4","key":"9377_CR13","doi-asserted-by":"crossref","first-page":"470","DOI":"10.1016\/j.jal.2005.10.006","volume":"4","author":"B Buchberger","year":"2006","unstructured":"Buchberger, B., Cr\u01ceciun, A., Jebelean, T., Kov\u00e1cs, L., Kutsia, T., Nakagawa, K., Piroi, F., Popov, N., Robu, J., Rosenkranz, M., et al.: Theorema: towards computer-aided mathematical theory exploration. J. Appl. Log. 4(4), 470\u2013504 (2006)","journal-title":"J. Appl. Log."},{"issue":"1","key":"9377_CR14","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/s10472-011-9248-8","volume":"61","author":"A Bundy","year":"2011","unstructured":"Bundy, A.: Automated theorem provers: a practical tool for the working mathematician? Ann. Math. Artif. Intell. 61(1), 3\u201314 (2011)","journal-title":"Ann. Math. Artif. Intell."},{"key":"9377_CR15","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-55602-8_220","volume-title":"Analytica\u2014A theorem prover in Mathematica","author":"E Clarke","year":"1992","unstructured":"Clarke, E., Zhao, X.: Analytica\u2014A theorem prover in Mathematica. Springer, Berlin (1992)"},{"key":"9377_CR16","unstructured":"Felty, A., Miller, D.: Proof explanation and revision. Technical Report MS-CIS-88-17, University of Pennsylvania (1987)"},{"key":"9377_CR17","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-37012-0","volume-title":"The Language of Mathematics","author":"M Ganesalingam","year":"2013","unstructured":"Ganesalingam, M.: The Language of Mathematics. Springer, Berlin (2013)"},{"key":"9377_CR18","unstructured":"Gonthier, G.: A computer-checked proof of the four colour theorem. http:\/\/research.microsoft.com\/en-US\/people\/gonthier\/4colproof.pdf"},{"key":"9377_CR19","doi-asserted-by":"crossref","first-page":"163","DOI":"10.1007\/978-3-642-39634-2_14","volume-title":"Interactive Theorem Proving","author":"G Gonthier","year":"2013","unstructured":"Gonthier, G., Asperti, A., Avigad, J., Bertot, Y., Cohen, C., Garillot, F., Le Roux, S., Mahboubi, A., O\u2019Connor, R., Biha, S.O., Pasca, I., Rideau, L., Solovyev, A., Tassi, E., Th\u00e9ry, L.: A machine-checked proof of the odd order theorem. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) Interactive Theorem Proving, pp. 163\u2013179. Springer, Berlin (2013)"},{"key":"9377_CR20","first-page":"41","volume-title":"Syntax and Semantics","author":"HP Grice","year":"1975","unstructured":"Grice, H.P.: Logic and conversation. In: Cole, P., Morgan, J.L. (eds.) Syntax and Semantics, vol. 3, pp. 41\u201358. Academic Press, New York (1975)"},{"key":"9377_CR21","unstructured":"Hales, T., Adams, M., Bauer, G., Dang, D.T., Harrison, J., Hoang, T.L., Kaliszyk, C., Magron, V., McLaughlin, S., Nguyen, T.T., Nguyen, T.Q., Nipkow, T., Obua, S., Pleso, J., Rute, J., Solovyev, A., Ta, A.H.T., Tran, T.N., Trieu, D.T., Urban, J., Vu, K.K., Zumkeller, R.: A formal proof of the kepler conjecture. http:\/\/arxiv.org\/abs\/1501.02155 (2015)"},{"key":"9377_CR22","unstructured":"Holland-Minkley, A.M., Barzilay, R., Constable, R.L.: Verbalization of high-level formal proofs. In: Proceedings of Sixteenth National Conference on Artificial Intelligence, pp. 277\u2013284 (1999)"},{"key":"9377_CR23","unstructured":"Humayoun, M., Raffalli, C.: MathNat\u2014Mathematical text in a controlled natural language. J. Res. Comput. Sci.\u2014Spec. Issue: Nat. Lang. Process. Appl. 46, 293\u2013307 (2010)"},{"key":"9377_CR24","unstructured":"Knott, A.: A data-driven methodology for motivating a set of coherence relations. Ph.D. thesis, University of Edinburgh (1996)"},{"key":"9377_CR25","unstructured":"Kuhlwein, D., Cramer, M., Koepke, P., Schr\u00f6der, B.: The Naproche system. http:\/\/www.naproche.net\/downloads\/2009\/emergingsystems.pdf (2009)"},{"key":"9377_CR26","doi-asserted-by":"crossref","unstructured":"Mancosu, P. (ed.): Mathematical explanation: why it matters. In: The Philosophy of Mathematical Practice, pp. 134\u2013149. Oxford University Press, Oxford (2008)","DOI":"10.1093\/acprof:oso\/9780199296453.003.0006"},{"issue":"3","key":"9377_CR27","doi-asserted-by":"crossref","first-page":"272","DOI":"10.1037\/0022-0663.77.3.272","volume":"77","author":"E Owen","year":"1985","unstructured":"Owen, E., Sweller, J.: What do students learn while solving mathematics problems? J. Educ. Psychol. 77(3), 272\u2013284 (1985)","journal-title":"J. Educ. Psychol."},{"key":"9377_CR28","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511526602","volume-title":"Logic and Computation: Interactive Proof with Cambridge LCF","author":"LC Paulson","year":"1987","unstructured":"Paulson, L.C.: Logic and Computation: Interactive Proof with Cambridge LCF. Cambridge University Press, Cambridge (1987)"},{"key":"9377_CR29","doi-asserted-by":"crossref","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)"},{"issue":"4","key":"9377_CR30","doi-asserted-by":"crossref","first-page":"639","DOI":"10.1037\/0096-3445.112.4.639","volume":"112","author":"J Sweller","year":"1983","unstructured":"Sweller, J., Mawer, R.F., Ward, M.R.: Development of expertise in mathematical problem solving. J. Exp. Psychol. Gen. 112(4), 639\u2013661 (1983)","journal-title":"J. Exp. Psychol. Gen."},{"issue":"2","key":"9377_CR31","first-page":"136","volume":"6","author":"A Trybulec","year":"1978","unstructured":"Trybulec, A.: The Mizar-QC\/6000 logic information language. Bull. Assoc. Lit. Linguist. Comput. 6(2), 136\u2013140 (1978)","journal-title":"Bull. Assoc. Lit. Linguist. Comput."},{"issue":"3","key":"9377_CR32","first-page":"120","volume":"7","author":"K Vershinin","year":"2000","unstructured":"Vershinin, K., Paskevich, A.: Forthel\u2014the language of formal theories. Int. J. Inf. Theor. Appl. 7(3), 120\u2013126 (2000)","journal-title":"Int. J. Inf. Theor. Appl."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-016-9377-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-016-9377-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-016-9377-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-016-9377-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,24]],"date-time":"2017-06-24T12:11:45Z","timestamp":1498306305000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-016-9377-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,6,11]]},"references-count":32,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2017,2]]}},"alternative-id":["9377"],"URL":"https:\/\/doi.org\/10.1007\/s10817-016-9377-1","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,6,11]]}}}