{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T20:25:22Z","timestamp":1761596722449,"version":"3.41.0"},"reference-count":16,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[1999,11,1]],"date-time":"1999-11-01T00:00:00Z","timestamp":941414400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[1999,11,1]],"date-time":"1999-11-01T00:00:00Z","timestamp":941414400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Journal of Automated Reasoning"],"published-print":{"date-parts":[[1999,11]]},"DOI":"10.1023\/a:1006269330992","type":"journal-article","created":{"date-parts":[[2002,12,22]],"date-time":"2002-12-22T01:20:41Z","timestamp":1040520041000},"page":"235-264","source":"Crossref","is-referenced-by-count":16,"title":["A Formal Proof of Sylow's Theorem"],"prefix":"10.1007","volume":"23","author":[{"given":"Florian","family":"Kamm\u00fcller","sequence":"first","affiliation":[]},{"given":"Lawrence C.","family":"Paulson","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"236899_CR1","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1016\/0890-5401(91)90066-B","volume":"91","author":"N. G. de Bruijn","year":"1991","unstructured":"de Bruijn, N. G.: Telescoping mappings in typed lambda calculus, Inform. and Comput.\n91 (1991), 189-204.","journal-title":"Inform. and Comput."},{"key":"236899_CR2","unstructured":"de Bruijn, N. G.: A survey of the project AUTOMATH, in J. P. Seldin and J. R. Hindley (eds.), To H. B. Curry: Essays on Combinatory Logic, Academic Press Limited, 1980, 579-606."},{"key":"236899_CR3","unstructured":"Dowek, G.: Naming and scoping in a mathematical vernacular, Technical Report 1283, INRIA, Rocquencourt, 1990."},{"key":"236899_CR4","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1007\/BF00881906","volume":"11","author":"W. M. Farmer","year":"1993","unstructured":"Farmer, W. M., Guttman, J. D. and Thayer, F. J.: IMPS: An Interactive Mathematical Proof System, J. Automated Reasoning\n11 (1993), 213-248.","journal-title":"J. Automated Reasoning"},{"key":"236899_CR5","doi-asserted-by":"crossref","unstructured":"Guttag, J. V. and Horning, J. J. (eds.): Larch: Languages and Tools for Formal Specification, Texts and Monographs in Comput. Sci., Springer-Verlag, 1993. With Stephen J. Garland, Kevin D. Jones, Andr\u00e9s Modet, and Jeannette M. Wing.","DOI":"10.1007\/978-1-4612-2704-5"},{"key":"236899_CR6","unstructured":"Gunter, E. L.: Doing algebra in simple type theory, Technical Report MS-CIS-89-38, Dep. of Computer and Information Science, University of Pennsylvania, 1989."},{"key":"236899_CR7","unstructured":"Herstein, I. N.: Topics in Algebra, Xerox, 1964."},{"key":"236899_CR8","unstructured":"The HOL System, Tutorial. Available on the Web as http:\/\/lal.cs.byu.edu\/lal\/holdoc\/tutorial.html."},{"key":"236899_CR9","doi-asserted-by":"crossref","unstructured":"Kamm\u00fcller, F. and Wenzel, M.: Locales - a sectioning concept for Isabelle, Technical Report 449, University of Cambridge, Computer Laboratory, 1998.","DOI":"10.1007\/3-540-48256-3_11"},{"key":"236899_CR10","unstructured":"Owre, S., Shankar, N. and Rushby, J. M.: The PVS specification language (Beta Release), Technical report, SRI International, 1993."},{"key":"236899_CR11","unstructured":"Paulson, L. C.: Isabelle: The next 700 theorem provers, in P. Odifreddi (ed.), Logic and Computer Science, Academic Press, 1990, pp. 361-386."},{"key":"236899_CR12","doi-asserted-by":"crossref","unstructured":"Paulson, L. C.: Isabelle: A Generic Theorem Prover, LNCS 828, Springer, 1994.","DOI":"10.1007\/BFb0030541"},{"key":"236899_CR13","doi-asserted-by":"crossref","unstructured":"Paulson, L. C.: First Isabelle user' workshop, Technical Report 379, Computer Laboratory, University of Cambridge, September 1995.","DOI":"10.1007\/BFb0030541"},{"key":"236899_CR14","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1007\/BF00283132","volume":"17","author":"L. C. Paulson","year":"1996","unstructured":"Paulson, L. C. and Grabczewski, K.: Mechanizing set theory, J. Automated Reasoning\n17 (1996), 291-323.","journal-title":"J. Automated Reasoning"},{"key":"236899_CR15","doi-asserted-by":"crossref","first-page":"401","DOI":"10.1007\/BF01240818","volume":"10","author":"H. Wielandt","year":"1959","unstructured":"Wielandt, H.: Ein Beweis f\u00fcr die Existenz der Sylowgruppen, Arch. Math.\n10 (1959), 401-402.","journal-title":"Arch. Math."},{"key":"236899_CR16","first-page":"251","volume":"6","author":"Y. Yu","year":"1990","unstructured":"Yu, Y.: Computer proofs in group theory, J. Automated Reasoning\n6 (1990), 251-286.","journal-title":"J. Automated Reasoning"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1006269330992.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1006269330992\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1006269330992.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:35:36Z","timestamp":1749123336000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1006269330992"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999,11]]},"references-count":16,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1999,11]]}},"alternative-id":["236899"],"URL":"https:\/\/doi.org\/10.1023\/a:1006269330992","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[1999,11]]}}}