{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,4]],"date-time":"2025-04-04T21:24:04Z","timestamp":1743801844657},"publisher-location":"Berlin, Heidelberg","reference-count":18,"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_6","type":"book-chapter","created":{"date-parts":[[2007,8,14]],"date-time":"2007-08-14T06:57:56Z","timestamp":1187074676000},"page":"66-79","source":"Crossref","is-referenced-by-count":12,"title":["Biform Theories in Chiron"],"prefix":"10.1007","author":[{"given":"William M.","family":"Farmer","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"6_CR1","doi-asserted-by":"publisher","first-page":"2351","DOI":"10.1098\/rsta.2005.1650","volume":"363","author":"H. Barendregt","year":"2005","unstructured":"Barendregt, H., Wiedijk, F.: The challenge of computer mathematics. Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences\u00a0363, 2351\u20132375 (2005)","journal-title":"Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences"},{"key":"6_CR2","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":"6_CR3","unstructured":"Calculemus Project: Systems for Integrated Computation and Deduction. Web site at \n                    \n                      http:\/\/www.calculemus.net\/"},{"key":"6_CR4","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1145\/1005285.1005298","volume-title":"ISSAC 2004","author":"J. Carette","year":"2004","unstructured":"Carette, J.: Understanding expression simplification. In: Gutierrez, J. (ed.) ISSAC 2004. Proceedings of the 2004 International Symposium on Symbolic and Algebraic Computation, pp. 72\u201379. ACM Press, New York (2004)"},{"key":"6_CR5","series-title":"LNCS (LNAI)","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73086-6_2","volume-title":"Towards Mechanized Mathematical Assistants","author":"J. Carette","year":"2007","unstructured":"Carette, J., Farmer, W.M., Sorge, V.: A rational reconstruction of a system for experimental mathematics. In: Kauers, M., Windsteiger, W. (eds.) Towards Mechanized Mathematical Assistants. LNCS (LNAI), vol.\u00a04573, Springer, Heidelberg (2007)"},{"key":"6_CR6","unstructured":"Carette, J., Farmer, W.M., Wajs, J.: Trustable communication between mathematics systems. In: Hardin, T., Rioboo, R. (eds.) Calculemus 2003, pp. 58\u201368, Rome, Italy, Aracne (2003)"},{"key":"6_CR7","unstructured":"Farmer, W.M.: Chiron: A multi-paradigm logic. Studies in Logic, Grammar and Rhetoric. Special issue: Matuszewski, R., Rudnicki, P., Zalewska, A. (eds.) From Insight to Proof, forthcoming"},{"key":"6_CR8","unstructured":"Farmer, W.M.: The seven virtues of simple type theory. SQRL Report No.\u00a018, McMaster University, 2003. Revised (2006)"},{"key":"6_CR9","unstructured":"Farmer, W.M.: Chiron: A set theory with types, undefinedness, quotation, and evaluation. SQRL Report No.\u00a038, McMaster University (2007)"},{"key":"6_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1007\/10721959_8","volume-title":"Automated Deduction - CADE-17","author":"W.M. Farmer","year":"2000","unstructured":"Farmer, W.M., von Mohrenschildt, M.: Transformers for symbolic computation and formal deduction. In: Colton, S., Martin, U., Sorge, V. (eds.) Automated Deduction - CADE-17. LNCS, vol.\u00a01831, pp. 36\u201345. Springer, Heidelberg (2000)"},{"key":"6_CR11","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":"6_CR12","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/BF01700692","volume":"38","author":"K. G\u00f6del","year":"1931","unstructured":"G\u00f6del, K.: \u00dcber formal unentscheidbare S\u00e4tze der Principia Mthematica und verwandter Systeme I. Monatshefte f\u00fcr Mathematik und Physik\u00a038, 173\u2013198 (1931)","journal-title":"Monatshefte f\u00fcr Mathematik und Physik"},{"key":"6_CR13","volume-title":"Annals of Mathematical Studies","author":"K. G\u00f6del","year":"1940","unstructured":"G\u00f6del, K.: The Consistency of the Axiom of Choice and the Generalized Continuum Hypothesis with the Axioms of Set Theory. In: Annals of Mathematical Studies, vol.\u00a03, Princeton University Press, Princeton (1940)"},{"key":"6_CR14","unstructured":"Harrison, J.: Metatheory and reflection in theorem proving: A survey and critique. Technical Report CRC-053, SRI Cambridge, Millers Yard, Cambridge, UK (1995), available at \n                    \n                      http:\/\/www.cl.cam.ac.uk\/jrh13\/papers\/reflect.ps.gz"},{"key":"6_CR15","unstructured":"MathScheme: An Integrated Framework for Computer Algebra and Computer Theorem Proving, Web site at \n                    \n                      http:\/\/www.imps.mcmaster.ca\/mathscheme\/"},{"key":"6_CR16","volume-title":"Introduction to Mathematical Logic","author":"E. Mendelson","year":"1997","unstructured":"Mendelson, E.: Introduction to Mathematical Logic, vol.\u00a04. Chapman & Hall\/CRC, Sydney (1997)"},{"key":"6_CR17","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1145\/1088454.1088456","volume-title":"MERLIN 2005","author":"A. Nogin","year":"2005","unstructured":"Nogin, A., Kopylov, A., Yu, X., Hickey, J.: A computational approach to reflective meta-reasoning about languages with bindings. In: Momigliano, A., Pollack, R. (eds.) MERLIN 2005. Proceedings of the Third ACM SIGPLAN Workshop on Mechanized Reasoning about Languages with Variable Binding. An extended version is available as a California Institute of Technology technical report, CaltechCSTR:2005.003, pp. 2\u201312. ACM Press, New York (2005)"},{"key":"6_CR18","unstructured":"RISC Research Institute for Symbolic Computation, Web site at \n                    \n                      http:\/\/www.risc.uni-linz.ac.at\/\/"}],"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_6.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T05:59:52Z","timestamp":1619503192000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73086-6_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540730835","9783540730866"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73086-6_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}