{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,9]],"date-time":"2022-04-09T08:27:16Z","timestamp":1649492836704},"reference-count":22,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2015,9,15]],"date-time":"2015-09-15T00:00:00Z","timestamp":1442275200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2015,10]]},"DOI":"10.1007\/s10817-015-9338-0","type":"journal-article","created":{"date-parts":[[2015,9,15]],"date-time":"2015-09-15T21:43:36Z","timestamp":1442353416000},"page":"223-243","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Formal Proofs of Hypergeometric Sums"],"prefix":"10.1007","volume":"55","author":[{"given":"John","family":"Harrison","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,9,15]]},"reference":[{"key":"9338_CR1","first-page":"11","volume":"61","author":"R Ap\u00e9ry","year":"1979","unstructured":"Ap\u00e9ry, R.: Irrationalit\u00e9 de \u03b6(2) et \u03b6(3). Ast\u00e9risque 61, 11\u201313 (1979)","journal-title":"Ast\u00e9risque"},{"key":"9338_CR2","unstructured":"Artin, E.: The Gamma Function. Holt, Ronehart and Winton (1964). English translation by Michael Butler"},{"key":"9338_CR3","doi-asserted-by":"crossref","first-page":"268","DOI":"10.1112\/blms\/11.3.268","volume":"11","author":"F Beukers","year":"1979","unstructured":"Beukers, F.: A note on the irrationality of \u03b6(2) and \u03b6(3). Bull. Lond. Math. Soc. 11, 268\u2013272 (1979)","journal-title":"Bull. Lond. Math. Soc."},{"key":"9338_CR4","doi-asserted-by":"crossref","unstructured":"Chyzak, F., Mahboubi, A., Sibu-Pinote, T., Tassi, E.: A computer-algebra-based formal proof of the irrationality of \u03b6(3). To appear in ITP 2014 (2014)","DOI":"10.1007\/978-3-319-08970-6_11"},{"key":"9338_CR5","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1006\/jsco.2001.0457","volume":"32","author":"O Caprotti","year":"2001","unstructured":"Caprotti, O., Oostdijk, M.: Formal and efficient primality proofs by the use of computer algebra oracles. J. Symb. Comput. 32, 55\u201370 (2001)","journal-title":"J. Symb. Comput."},{"key":"9338_CR6","unstructured":"Cohen, H.: Number Theory volume II: Analytic and Modern Tools, volume 240 of Graduate Texts in Mathematics. Springer (2007)"},{"key":"9338_CR7","doi-asserted-by":"crossref","first-page":"1","DOI":"10.2307\/2975209","volume":"103","author":"D Fowler","year":"1996","unstructured":"Fowler, D.: The binomial coefficient function. Am. Math. Mon. 103, 1\u201317 (1996)","journal-title":"Am. Math. Mon."},{"key":"9338_CR8","doi-asserted-by":"crossref","first-page":"537","DOI":"10.1006\/jsco.1995.1064","volume":"20","author":"IM Gessel","year":"1995","unstructured":"Gessel, I.M.: Finding identities with the WZ method. J. Symb. Comput. 20, 537\u2013566 (1995)","journal-title":"J. Symb. Comput."},{"key":"9338_CR9","first-page":"489","volume":"1","author":"PE Gibbs","year":"2010","unstructured":"Gibbs, P.E.: Crackpots who were right II. Prespacetime J. 1, 489\u2013497 (2010)","journal-title":"Prespacetime J."},{"key":"9338_CR10","doi-asserted-by":"crossref","first-page":"40","DOI":"10.1073\/pnas.75.1.40","volume":"75","author":"WR Gosper","year":"1978","unstructured":"Gosper, W.R.: Decision procedure for indefinite hypergeometric summation. Proc. Natl. Acad. Sci. U.S.A. 75, 40\u201342 (1978)","journal-title":"Proc. Natl. Acad. Sci. U.S.A."},{"key":"9338_CR11","doi-asserted-by":"crossref","unstructured":"Gr\u00e9goire, B., Th\u00e9ry, L., Wener, B.: A computational approach to Pocklington certificates in type theory. In: Proceedings of the 8th International Symposium on Functional and Logic Programming, volume 3945 of Lecture Notes in Computer Science, pp. 97\u2013113. Springer-Verlag (2006)","DOI":"10.1007\/11737414_8"},{"key":"9338_CR12","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1023\/A:1006023127567","volume":"21","author":"J Harrison","year":"1998","unstructured":"Harrison, J., Th\u00e9ry, L.: A sceptic\u2019s approach to combining HOL and Maple. J. Autom. Reason. 21, 279\u2013294 (1998)","journal-title":"J. Autom. Reason."},{"key":"9338_CR13","doi-asserted-by":"crossref","unstructured":"Lang, S.: Complex Analysis. Graduate Texts in Mathematics, 3rd edition. Springer (1993)","DOI":"10.1007\/978-1-4612-0897-6_1"},{"key":"9338_CR14","doi-asserted-by":"crossref","first-page":"505","DOI":"10.2307\/2975078","volume":"104","author":"I Nemes","year":"1997","unstructured":"Nemes, I., Petkovs\u0307ek, M., Wilf, H., Zeilberger, D.: How to do your monthly problems with your computer. Am. Math. Mon. 104, 505\u2013519 (1997)","journal-title":"Am. Math. Mon."},{"key":"9338_CR15","doi-asserted-by":"crossref","unstructured":"Petkovs\u0307ek, M., Wilf, H.S., Zeilberger, D.: A = B. A K Peters (1996)","DOI":"10.1201\/9781439864500"},{"key":"9338_CR16","doi-asserted-by":"crossref","unstructured":"Carsten Schneider: Ap\u00e9ry\u2019s double sum is plain sailing indeed. Electron. J. Comb., 14 (2007)","DOI":"10.37236\/1006"},{"key":"9338_CR17","doi-asserted-by":"crossref","unstructured":"Siddique, U, Hasan, O.: On the formalization of the gamma function in HOL. J. Autom. Reason., 407\u2013429 (2014)","DOI":"10.1007\/s10817-014-9311-3"},{"key":"9338_CR18","doi-asserted-by":"crossref","unstructured":"Stanley, R.P.: Enumerative Combinatorics, vol. 2. Cambridge University Press (1999)","DOI":"10.1017\/CBO9780511609589"},{"key":"9338_CR19","first-page":"319","volume-title":"Proceedings of the 20th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2007, volume 4732 of Lecture Notes in Computer Science","author":"L Th\u00e9ry","year":"2007","unstructured":"Th\u00e9ry, L., Hanrot, G.: Primality proving with elliptic curves. In: Schneider, K., Brandt, J. (eds.) Proceedings of the 20th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2007, volume 4732 of Lecture Notes in Computer Science, pp 319\u2013333. Springer, Kaiserslautern, Germany (2007)"},{"key":"9338_CR20","doi-asserted-by":"crossref","first-page":"195","DOI":"10.1007\/BF03028234","volume":"1","author":"AJ van der Poorten","year":"1979","unstructured":"van der Poorten, A.J.: A proof that Euler missed: Ap\u00e9ry\u2019s proof of the irrationality of \u03b6(3), an informal report. Math. Intell. 1, 195\u2013303 (1979)","journal-title":"Math. Intell."},{"key":"9338_CR21","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1090\/S0894-0347-1990-1007910-7","volume":"3","author":"HS Wilf","year":"1990","unstructured":"Wilf, H.S., Zeilberger, D.: Rational functions certify combinatorial identities. J. Am. Math. Soc. 3, 147\u2013158 (1990)","journal-title":"J. Am. Math. Soc."},{"key":"9338_CR22","doi-asserted-by":"crossref","unstructured":"Zeilberger, D.: A holonomic systems approach to special functions identities. J. Comput. Appl. Math. 32, 321\u2013368","DOI":"10.1016\/0377-0427(90)90042-X"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-015-9338-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-015-9338-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-015-9338-0","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,9,8]],"date-time":"2020-09-08T10:26:09Z","timestamp":1599560769000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-015-9338-0"}},"subtitle":["Dedicated to the memory of Andrzej Trybulec"],"short-title":[],"issued":{"date-parts":[[2015,9,15]]},"references-count":22,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2015,10]]}},"alternative-id":["9338"],"URL":"https:\/\/doi.org\/10.1007\/s10817-015-9338-0","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,9,15]]}}}