{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:31:28Z","timestamp":1725489088025},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540730835"},{"type":"electronic","value":"9783540730866"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-73086-6_2","type":"book-chapter","created":{"date-parts":[[2007,8,14]],"date-time":"2007-08-14T10:57:56Z","timestamp":1187089076000},"page":"13-26","source":"Crossref","is-referenced-by-count":3,"title":["A Rational Reconstruction of a System for Experimental Mathematics"],"prefix":"10.1007","author":[{"given":"Jacques","family":"Carette","sequence":"first","affiliation":[]},{"given":"William M.","family":"Farmer","sequence":"additional","affiliation":[]},{"given":"Volker","family":"Sorge","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"2_CR1","doi-asserted-by":"crossref","unstructured":"Armando, A., Ranise, S.: From integrated reasoning specialists to \u201cplug-and-play\u201d reasoning components. In: Calmet and Plaza [5], pp. 42\u201354","DOI":"10.1007\/BFb0055901"},{"key":"2_CR2","unstructured":"Armando, A., Zini, D.: Towards Interoperable Mechanized Reasoning Systems: the Logic Broker Architecture. In: AI*IA Notizie Anno XIII, Parma, Italy, vol. 3, pp. 70\u201375 (2000)"},{"key":"2_CR3","doi-asserted-by":"crossref","unstructured":"Bertoli, P.G., Calmet, J., Giunchiglia, F., Homann, K.: Specification and Integration of Theorem Provers and Computer Algebra Systems. In: Calmet and Plaza [5], pp. 94\u2013106","DOI":"10.1007\/BFb0055905"},{"key":"2_CR4","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., Kovacs, L., Kutsia, T., Nakagawa, K., Piroi, F., Popov, N., Robu, J., Rosenkranz, M., Windsteiger, W.: Theorema: Towards computer-aided mathematical theory exploration. Journal of Applied Logic\u00a04, 470\u2013504 (2006)","journal-title":"Journal of Applied Logic"},{"key":"2_CR5","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Artificial Intelligence and Symbolic Computation","year":"1998","unstructured":"Calmet, J., Plaza, J. (eds.): AISC 1998. LNCS (LNAI), vol.\u00a01476. Springer, Heidelberg (1998)"},{"key":"2_CR6","unstructured":"Carette, J., Farmer, W.M., Wajs, J.: Trustable communication between mathematical systems. In: Proc. of Calculemus 2003, pp. 58\u201368 (2003)"},{"key":"2_CR7","doi-asserted-by":"publisher","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A. Church","year":"1940","unstructured":"Church, A.: A Formulation of the Simple Theory of Types. Journal of Symbolic Logic\u00a05, 56\u201368 (1940)","journal-title":"Journal of Symbolic Logic"},{"key":"2_CR8","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"400","DOI":"10.1007\/978-3-540-25984-8_30","volume-title":"Automated Reasoning","author":"S. Colton","year":"2004","unstructured":"Colton, S., Meier, A., Sorge, V., McCasland, R.: Automatic generation of classification theorems for finite algebras. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS (LNAI), vol.\u00a03097, pp. 400\u2013414. Springer, Heidelberg (2004)"},{"issue":"2","key":"2_CR9","doi-asserted-by":"publisher","first-page":"511","DOI":"10.2307\/1995510","volume":"151","author":"E. Falconer","year":"1970","unstructured":"Falconer, E.: Isotopy Invariants in Quasigroups. Transactions of the American Mathematical Society\u00a0151(2), 511\u2013526 (1970)","journal-title":"Transactions of the American Mathematical Society"},{"issue":"3","key":"2_CR10","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1023\/A:1006437704595","volume":"26","author":"W.M. Farmer","year":"2001","unstructured":"Farmer, W.M.: STMM: A set theory for mechanized mathematics. J. Autom. Reasoning\u00a026(3), 269\u2013289 (2001)","journal-title":"J. Autom. Reasoning"},{"key":"2_CR11","series-title":"LNAI","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73086-6_6","volume-title":"Towards Mechanized Mathematical Assistants","author":"W.M. Farmer","year":"2007","unstructured":"Farmer, W.M.: Biform theories in Chiron. In: Kauers, M., Windsteiger, W. (eds.) Towards Mechanized Mathematical Assistants. LNCS (LNAI), vol.\u00a04573, Springer, Heidelberg (2007)"},{"key":"2_CR12","unstructured":"Farmer, W.M., von Mohrenschildt, M.: Transformers for symbolic computation and formal deduction. In: Colton, S., Martin, U., Sorge, V. (eds.) CADE-17 Workshop on the Role of Automated Deduction in Mathematics, pp. 36\u201345 (2000)"},{"key":"2_CR13","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1023\/A:1022971915900","volume":"38","author":"W.M. Farmer","year":"2003","unstructured":"Farmer, W.M., von Mohrenschildt, M.: An overview of a formal framework for managing mathematics. Annals of Mathematics and Artificial Intelligence\u00a038, 165\u2013191 (2003)","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"2_CR14","series-title":"Lecture Notes in Artificial Intelligence","first-page":"36","volume-title":"Automatic construction and verification of isotopy invariants","author":"V. Sorge","year":"2006","unstructured":"Sorge, V., Meier, A., McCasland, R., Colton, S.: Automatic construction and verification of isotopy invariants. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, pp. 36\u201351. Springer, Heidelberg (2006)"},{"key":"2_CR15","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Automated Deduction - CADE-18","author":"J. Zimmer","year":"2002","unstructured":"Zimmer, J., Kohlhase, M.: System Description: The MathWeb Software Bus for Distributed Mathematical Reasoning. In: Voronkov, A. (ed.) Automated Deduction - CADE-18. LNCS (LNAI), vol.\u00a02392, Springer, Heidelberg (2002)"}],"container-title":["Lecture Notes in Computer Science","Towards Mechanized Mathematical Assistants"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-73086-6_2.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T09:59:44Z","timestamp":1619517584000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73086-6_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540730835","9783540730866"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73086-6_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}