{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,31]],"date-time":"2025-08-31T10:24:46Z","timestamp":1756635886659,"version":"3.37.3"},"reference-count":15,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2016,10,4]],"date-time":"2016-10-04T00:00:00Z","timestamp":1475539200000},"content-version":"unspecified","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":[[2017,8]]},"DOI":"10.1007\/s10817-016-9387-z","type":"journal-article","created":{"date-parts":[[2016,10,4]],"date-time":"2016-10-04T12:51:59Z","timestamp":1475585519000},"page":"267-286","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Fermat, Euler, Wilson - Three Case Studies in Number Theory"],"prefix":"10.1007","volume":"59","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9382-5399","authenticated-orcid":false,"given":"Christoph","family":"Walther","sequence":"first","affiliation":[]},{"given":"Nathan","family":"Wasser","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,10,4]]},"reference":[{"key":"9387_CR1","unstructured":"http:\/\/verifun.de"},{"key":"9387_CR2","unstructured":"Boyer, R.S., Moore, JS.: A Computational Logic. Academic Press, New York (1979)"},{"key":"9387_CR3","unstructured":"Boyer, R.S., Moore, JS.: Proof checking the RSA public key encryption algorithm. Am. Math. Mon. 91(3), 181\u2013189 (1984)"},{"key":"9387_CR4","doi-asserted-by":"crossref","unstructured":"Boyer, R.S., Moore, JS.: A theorem prover for a computational logic (keynote address). In: Proceedings of 10th International Conference on Automated Deduction (CADE-10). Lecture Notes in Computer Science, vol. 449, pp. 1\u201315, Kaiserslautern (1990)","DOI":"10.1007\/3-540-52885-7_75"},{"key":"9387_CR5","unstructured":"Boyer, R.S., Moore, JS.: On the difficulty of automating inductive reasoning. Remarks made at a CADE-11 Workshop on Inductive Reasoning, Saratoga Springs (1992)"},{"key":"9387_CR6","unstructured":"Dickson, L.E.: History of the theory of numbers. In: Divisibility and Primality. vol 1, Carnegie Institution of Washington, Publication No. 256, Washington (1919)"},{"key":"9387_CR7","doi-asserted-by":"crossref","unstructured":"Rasmussen, T.M.: An inductive approach to formalizing notions of number theory proofs. In: Computer Mathematics: Proceedings of the 5th Asian Symposium (ASCM 2001), Matsuyama, Japan pp. 131\u2013140 (2001)","DOI":"10.1142\/9789812799661_0014"},{"key":"9387_CR8","volume-title":"Elementary Number Theory and Its Applications","author":"KH Rosen","year":"2005","unstructured":"Rosen, K.H.: Elementary Number Theory and Its Applications, 5th edn. Pearson Addison Wesley, Boston (2005)","edition":"5"},{"issue":"2","key":"9387_CR9","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1007\/BF00244993","volume":"1","author":"DM Russinoff","year":"1985","unstructured":"Russinoff, D.M.: An experiment with the Boyer\u2013Moore theorem prover: A proof of Wilson\u2019s theorem. J. Autom. Reason. 1(2), 121\u2013139 (1985)","journal-title":"J. Autom. Reason."},{"issue":"1","key":"9387_CR10","doi-asserted-by":"crossref","first-page":"101","DOI":"10.1016\/0004-3702(94)90063-9","volume":"71","author":"C Walther","year":"1994","unstructured":"Walther, C.: On proving the termination of algorithms by machine. Artif. Intell. 71(1), 101\u2013157 (1994)","journal-title":"Artif. Intell."},{"issue":"1","key":"9387_CR11","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1023\/B:JARS.0000021872.64036.41","volume":"32","author":"C Walther","year":"2004","unstructured":"Walther, C., Schweitzer, S.: Verification in the classroom. J. Autom. Reason. 32(1), 35\u201373 (2004)","journal-title":"J. Autom. Reason."},{"key":"9387_CR12","unstructured":"Walther, C., Schweitzer, S.: A pragmatic approach to equality reasoning. Technical Report VFR 06\/02, Technische Universit\u00e4t Darmstadt, pp. 1\u201319 (2006) (available from [1])"},{"key":"9387_CR13","unstructured":"https:\/\/coq.inria.fr"},{"key":"9387_CR14","unstructured":"https:\/\/github.com\/jrh13\/hol-light"},{"key":"9387_CR15","unstructured":"https:\/\/isabelle.in.tum.de"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-016-9387-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-016-9387-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-016-9387-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,14]],"date-time":"2019-09-14T03:47:55Z","timestamp":1568432875000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-016-9387-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,10,4]]},"references-count":15,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2017,8]]}},"alternative-id":["9387"],"URL":"https:\/\/doi.org\/10.1007\/s10817-016-9387-z","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2016,10,4]]}}}