{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,26]],"date-time":"2025-10-26T20:35:43Z","timestamp":1761510943079},"publisher-location":"Berlin, Heidelberg","reference-count":36,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642141270"},{"type":"electronic","value":"9783642141287"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-14128-7_12","type":"book-chapter","created":{"date-parts":[[2010,6,29]],"date-time":"2010-06-29T10:45:36Z","timestamp":1277808336000},"page":"132-146","source":"Crossref","is-referenced-by-count":12,"title":["Automated Reasoning and Presentation Support for Formalizing Mathematics in Mizar"],"prefix":"10.1007","author":[{"given":"Josef","family":"Urban","sequence":"first","affiliation":[]},{"given":"Geoff","family":"Sutcliffe","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"1","key":"12_CR1","first-page":"91","volume":"1","author":"G. Bancerek","year":"1990","unstructured":"Bancerek, G.: The Ordinal Numbers. Journal of Formalized Mathematics\u00a01(1), 91\u201396 (1990)","journal-title":"Journal of Formalized Mathematics"},{"key":"12_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1007\/3-540-36469-2_10","volume-title":"Mathematical Knowledge Management","author":"G. Bancerek","year":"2003","unstructured":"Bancerek, G., Rudnicki, P.: Information Retrieval in MML. In: Asperti, A., Buchberger, B., Davenport, J.H. (eds.) MKM 2003. LNCS, vol.\u00a02594, pp. 119\u2013132. Springer, Heidelberg (2003)"},{"key":"12_CR3","doi-asserted-by":"crossref","unstructured":"Benzm\u00fcller, C., Paulson, L.: Multimodal and Intuitionistic Logics in Simple Type Theory. Logic Journal of the IGPL (2010)","DOI":"10.1093\/jigpal\/jzp080"},{"key":"12_CR4","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1145\/1345169.1345176","volume-title":"Proceedings of the 2nd Workshop on Automated Formal Methods","author":"S. Conchon","year":"2007","unstructured":"Conchon, S., Contejean, E., Kanig, J., Lescuyer, S.: Lightweight Integration of the Ergo Theorem Prover Inside a Proof Assistant. In: Rushby, J., Shankar, N. (eds.) Proceedings of the 2nd Workshop on Automated Formal Methods, pp. 55\u201359. ACM Press, New York (2007)"},{"key":"12_CR5","unstructured":"Corbineau, P., Geuvers, H., Kaliszyk, C., McKinna, J., Wiedijk, F.: A Real Semantic Web for Mathematics Deserves a Real Semantics. In: Lange, C., Schaffert, S., Skaf-Molli, H., V\u00f6lkel, M. (eds.) Proceedings of the 3rd Semantic Wiki Workshop. CEUR Workshop Proceedings, vol.\u00a0360, pp. 62\u201366 (2008)"},{"key":"12_CR6","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/978-3-540-73086-6_19","volume-title":"Towards Mechanized Mathematical Assistants","author":"P. Corbineau","year":"2007","unstructured":"Corbineau, P., Kaliszyk, C.: Cooperative Repositories for Formal Proofs. In: Kauers, M., Kerber, M., Miner, R., Windsteiger, W. (eds.) MKM\/CALCULEMUS 2007. LNCS (LNAI), vol.\u00a04573, pp. 221\u2013234. Springer, Heidelberg (2007)"},{"issue":"7","key":"12_CR7","doi-asserted-by":"publisher","first-page":"1165","DOI":"10.1109\/TCAD.2008.923410","volume":"27","author":"V. D\u2019Silva","year":"2008","unstructured":"D\u2019Silva, V., Kroening, D., Weissenbacher, G.: A Survey of Automated Techniques for Formal Software Verification. IEEE Transactions on Computer-aided Design of Integrated Circuits and Systems\u00a027(7), 1165\u20131178 (2008)","journal-title":"IEEE Transactions on Computer-aided Design of Integrated Circuits and Systems"},{"issue":"11","key":"12_CR8","first-page":"1382","volume":"55","author":"G. Gonthier","year":"2008","unstructured":"Gonthier, G.: Formal Proof - The Four-Color Theorem. Notices of the American Mathematical Society\u00a055(11), 1382\u20131393 (2008)","journal-title":"Notices of the American Mathematical Society"},{"issue":"3","key":"12_CR9","doi-asserted-by":"publisher","first-page":"1065","DOI":"10.4007\/annals.2005.162.1065","volume":"162","author":"T. Hales","year":"2005","unstructured":"Hales, T.: A Proof of the Kepler Conjecture. Annals of Mathematics\u00a0162(3), 1065\u20131185 (2005)","journal-title":"Annals of Mathematics"},{"key":"12_CR10","unstructured":"Hales, T. (ed.): A Special Issue on Formal Proof, vol.\u00a055 (2008)"},{"key":"12_CR11","unstructured":"Hurd, J.: First-Order Proof Tactics in Higher-Order Logic Theorem Provers. In: Archer, M., Di Vito, B., Munoz, C. (eds.) Proceedings of the 1st International Workshop on Design and Application of Strategies\/Tactics in Higher Order Logics. number NASA\/CP-2003-212448 NASA Technical Reports, pp. 56\u201368 (2003)"},{"key":"12_CR12","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1145\/1629575.1629596","volume-title":"Proceedings of the 22nd ACM Symposium on Operating Systems Principles","author":"G. Klein","year":"2009","unstructured":"Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Winwood, S.: seL4: Formal Verification of an OS Kernel. In: Anderson, T. (ed.) Proceedings of the 22nd ACM Symposium on Operating Systems Principles, pp. 207\u2013220. ACM Press, New York (2009)"},{"issue":"3","key":"12_CR13","first-page":"407","volume":"2","author":"J. Kotowicz","year":"1991","unstructured":"Kotowicz, J., Raczkowski, K.: Real Function Differentiability - Part II. Formalized Mathematics\u00a02(3), 407\u2013411 (1991)","journal-title":"Formalized Mathematics"},{"issue":"3","key":"12_CR14","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1023\/A:1005843212881","volume":"19","author":"W.W. McCune","year":"1997","unstructured":"McCune, W.W.: Solution of the Robbins Problem. Journal of Automated Reasoning\u00a019(3), 263\u2013276 (1997)","journal-title":"Journal of Automated Reasoning"},{"issue":"3","key":"12_CR15","first-page":"73","volume":"5","author":"L. Paulson","year":"1999","unstructured":"Paulson, L.: A Generic Tableau Prover and its Integration with Isabelle. Artificial Intelligence\u00a05(3), 73\u201387 (1999)","journal-title":"Artificial Intelligence"},{"key":"12_CR16","unstructured":"Pease, A., Sutcliffe, G.: First Order Reasoning on a Large Ontology. In: Urban, J., Sutcliffe, G., Schulz, S. (eds.) Proceedings of the CADE-21 Workshop on Empirically Successful Automated Reasoning in Large Theories. CEUR Workshop Proceedings, vol.\u00a0257, pp. 59\u201369 (2007)"},{"key":"12_CR17","unstructured":"Phillips, J.D., Stanovsky, D.: Automated Theorem Proving in Loop Theory. In: Sutcliffe, G., Colton, S., Schulz, S. (eds.) Proceedings of the CICM Workshop on Empirically Successful Automated Reasoning in Mathematics. CEUR Workshop Proceedings, vol.\u00a0378, pp. 42\u201353 (2008)"},{"key":"12_CR18","first-page":"49","volume-title":"Proceedings of the 19th International FLAIRS Conference","author":"Y. Puzis","year":"2006","unstructured":"Puzis, Y., Gao, Y., Sutcliffe, G.: Automated Generation of Interesting Theorems. In: Sutcliffe, G., Goebel, R. (eds.) Proceedings of the 19th International FLAIRS Conference, pp. 49\u201354. AAAI Press, Menlo Park (2006)"},{"issue":"4","key":"12_CR19","first-page":"797","volume":"1","author":"K. Raczkowski","year":"1990","unstructured":"Raczkowski, K., Sadowski, P.: Real Function Differentiability. Formalized Mathematics\u00a01(4), 797\u2013801 (1990)","journal-title":"Formalized Mathematics"},{"issue":"2-3","key":"12_CR20","first-page":"111","volume":"15","author":"S. Schulz","year":"2002","unstructured":"Schulz, S.: E: A Brainiac Theorem Prover. AI Communications\u00a015(2-3), 111\u2013126 (2002)","journal-title":"AI Communications"},{"key":"12_CR21","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/978-3-642-04617-9_36","volume-title":"KI 2009: Advances in Artificial Intelligence","author":"M. Suda","year":"2009","unstructured":"Suda, M., Sutcliffe, G., Wischnewski, P., Lamotte-Schubert, M., de Melo, G.: External Sources of Axioms in Automated Theorem Proving. In: Mertsching, B., Hund, M., Aziz, Z. (eds.) KI 2009. LNCS (LNAI), vol.\u00a05803, pp. 281\u2013288. Springer, Heidelberg (2009)"},{"key":"12_CR22","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"406","DOI":"10.1007\/10721959_31","volume-title":"Automated Deduction - CADE-17","author":"G. Sutcliffe","year":"2000","unstructured":"Sutcliffe, G.: SystemOnTPTP. In: McAllester, D. (ed.) CADE 2000. LNCS (LNAI), vol.\u00a01831, pp. 406\u2013410. Springer, Heidelberg (2000)"},{"issue":"6","key":"12_CR23","doi-asserted-by":"publisher","first-page":"1053","DOI":"10.1142\/S0218213006003119","volume":"15","author":"G. Sutcliffe","year":"2006","unstructured":"Sutcliffe, G.: Semantic Derivation Verification. International Journal on Artificial Intelligence Tools\u00a015(6), 1053\u20131070 (2006)","journal-title":"International Journal on Artificial Intelligence Tools"},{"issue":"4","key":"12_CR24","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/s10817-009-9143-8","volume":"43","author":"G. Sutcliffe","year":"2009","unstructured":"Sutcliffe, G.: The TPTP Problem Library and Associated Infrastructure. The FOF and CNF Parts, v3.5.0. Journal of Automated Reasoning\u00a043(4), 337\u2013362 (2009)","journal-title":"Journal of Automated Reasoning"},{"key":"12_CR25","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/11814771_7","volume-title":"Automated Reasoning","author":"G. Sutcliffe","year":"2006","unstructured":"Sutcliffe, G., Schulz, S., Claessen, K., Van Gelder, A.: Using the TPTP Language for Writing Derivations and Finite Interpretations. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, pp. 67\u201381. Springer, Heidelberg (2006)"},{"key":"12_CR26","first-page":"341","volume-title":"Proceedings of the 12th International FLAIRS Conference","author":"G. Sutcliffe","year":"1999","unstructured":"Sutcliffe, G., Seyfang, D.: Smart Selective Competition Parallelism ATP. In: Kumar, A., Russell, I. (eds.) Proceedings of the 12th International FLAIRS Conference, pp. 341\u2013345. AAAI Press, Menlo Park (1999)"},{"key":"12_CR27","first-page":"105","volume-title":"Proceedings of the 22nd International FLAIRS Conference","author":"G. Sutcliffe","year":"2009","unstructured":"Sutcliffe, G., Yerikalapudi, A., Trac, S.: Multiple Answer Extraction for Question Answering with Automated Theorem Proving Systems. In: Guesgen, H., Lane, C. (eds.) Proceedings of the 22nd International FLAIRS Conference, pp. 105\u2013110. AAAI Press, Menlo Park (2009)"},{"key":"12_CR28","doi-asserted-by":"crossref","unstructured":"Trac, S., Puzis, Y., Sutcliffe, G.: An Interactive Derivation Viewer. In: Autexier, S., Benzm\u00fcller, C. (eds.) Proceedings of the 7th Workshop on User Interfaces for Theorem Provers, 3rd International Joint Conference on Automated Reasoning. Electronic Notes in Theoretical Computer Science, vol.\u00a0174, pp. 109\u2013123 (2006)","DOI":"10.1016\/j.entcs.2006.09.025"},{"key":"12_CR29","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"346","DOI":"10.1007\/11618027_23","volume-title":"Mathematical Knowledge Management","author":"J. Urban","year":"2006","unstructured":"Urban, J.: XML-izing Mizar: Making Semantic Processing and Presentaion of MML Easy. In: Kohlhase, M. (ed.) MKM 2005. LNCS (LNAI), vol.\u00a03863, pp. 346\u2013360. Springer, Heidelberg (2006)"},{"issue":"4","key":"12_CR30","doi-asserted-by":"publisher","first-page":"414","DOI":"10.1016\/j.jal.2005.10.004","volume":"4","author":"J. Urban","year":"2006","unstructured":"Urban, J.: MizarMode - An Integrated Proof Assistance Tool for the Mizar Way of Formalizing Mathematics. Journal of Applied Logic\u00a04(4), 414\u2013427 (2006)","journal-title":"Journal of Applied Logic"},{"issue":"1-2","key":"12_CR31","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/s10817-006-9032-3","volume":"37","author":"J. Urban","year":"2006","unstructured":"Urban, J.: MPTP 0.2: Design, Implementation, and Initial Experiments. Journal of Automated Reasoning\u00a037(1-2), 21\u201343 (2006)","journal-title":"Journal of Automated Reasoning"},{"key":"12_CR32","unstructured":"Urban, J.: Automated Reasoning for Mizar: Artificial Intelligence through Knowledge Exchange. In: Sutcliffe, G., Rudnicki, P., Schmidt, R., Konev, B., Schulz, S. (eds.) Proceedings of the LPAR Workshops: Knowledge Exchange: Automated Provers and Proof Assistants, and The 7th International Workshop on the Implementation of Logics. CEUR Workshop Proceedings, vol.\u00a0418, pp. 1\u201316 (2008)"},{"issue":"2","key":"12_CR33","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1007\/s11786-008-0053-7","volume":"2","author":"J. Urban","year":"2009","unstructured":"Urban, J., Sutcliffe, G.: ATP-based Cross Verification of Mizar Proofs: Method, Systems, and First Experiments. Journal of Mathematics in Computer Science\u00a02(2), 231\u2013251 (2009)","journal-title":"Journal of Mathematics in Computer Science"},{"key":"12_CR34","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1007\/978-3-540-71070-7_37","volume-title":"Automated Reasoning","author":"J. Urban","year":"2008","unstructured":"Urban, J., Sutcliffe, G., Pudlak, P., Vyskocil, J.: MaLARea SG1: Machine Learner for Automated Reasoning with Semantic Guidance. In: Baumgartner, P., Armando, A., Gilles, D. (eds.) IJCAR 2008. LNCS (LNAI), vol.\u00a05195, pp. 441\u2013456. Springer, Heidelberg (2008)"},{"issue":"31","key":"12_CR35","first-page":"121","volume":"18","author":"J. Urban","year":"2009","unstructured":"Urban, J., Sutcliffe, G., Trac, S., Puzis, Y.: Combining Mizar and TPTP Semantic Presentation and Verification Tools. Studies in Logic, Grammar and Rhetoric\u00a018(31), 121\u2013136 (2009)","journal-title":"Studies in Logic, Grammar and Rhetoric"},{"key":"12_CR36","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"514","DOI":"10.1007\/978-3-540-73595-3_38","volume-title":"Automated Deduction \u2013 CADE-21","author":"C. Weidenbach","year":"2007","unstructured":"Weidenbach, C., Schmidt, R., Hillenbrand, T., Rusev, R., Topic, D.: SPASS Version 3.0. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol.\u00a04603, pp. 514\u2013520. Springer, Heidelberg (2007)"}],"container-title":["Lecture Notes in Computer Science","Intelligent Computer Mathematics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-14128-7_12.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T02:47:50Z","timestamp":1606186070000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-14128-7_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642141270","9783642141287"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-14128-7_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}