{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,15]],"date-time":"2025-11-15T17:00:44Z","timestamp":1763226044166},"publisher-location":"Berlin, Heidelberg","reference-count":51,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642366741"},{"type":"electronic","value":"9783642366758"}],"license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-36675-8_13","type":"book-chapter","created":{"date-parts":[[2013,2,28]],"date-time":"2013-02-28T19:04:22Z","timestamp":1362078262000},"page":"240-257","source":"Crossref","is-referenced-by-count":19,"title":["Theorem Proving in Large Formal Mathematics as an Emerging AI Field"],"prefix":"10.1007","author":[{"given":"Josef","family":"Urban","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ji\u0159\u00ed","family":"Vysko\u010dil","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"13_CR1","unstructured":"The QED Manifesto. In: Bundy, A. (ed.) CADE 1994. LNCS, vol.\u00a0814, pp. 238\u2013251. Springer, Heidelberg (1994)"},{"key":"13_CR2","unstructured":"Alama, J., K\u00fchlwein, D., Tsivtsivadze, E., Urban, J., Heskes, T.: Premise selection for mathematics by corpus analysis and kernel methods. CoRR, abs\/1108.3446 (2011)"},{"key":"13_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/978-3-642-28717-6_6","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"J. Alama","year":"2012","unstructured":"Alama, J., K\u00fchlwein, D., Urban, J.: Automated and Human Proofs in General Mathematics: An Initial Comparison. In: Bj\u00f8rner, N., Voronkov, A. (eds.) LPAR-18. LNCS, vol.\u00a07180, pp. 37\u201345. Springer, Heidelberg (2012)"},{"key":"13_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1007\/978-3-642-04222-5_5","volume-title":"Frontiers of Combining Systems","author":"E. Althaus","year":"2009","unstructured":"Althaus, E., Kruglov, E., Weidenbach, C.: Superposition Modulo Linear Arithmetic SUP(LA). In: Ghilardi, S., Sebastiani, R. (eds.) FroCoS 2009. LNCS, vol.\u00a05749, pp. 84\u201399. Springer, Heidelberg (2009)"},{"issue":"4","key":"13_CR5","first-page":"733","volume":"9","author":"G. Bancerek","year":"2001","unstructured":"Bancerek, G., Endou, N., Sakai, Y.: On the characterizations of compactness. Formalized Mathematics\u00a09(4), 733\u2013738 (2001)","journal-title":"Formalized Mathematics"},{"key":"13_CR6","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/978-3-540-71070-7_14","volume-title":"Automated Reasoning","author":"C.E. Benzm\u00fcller","year":"2008","unstructured":"Benzm\u00fcller, C.E., Paulson, L.C., Theiss, F., Fietzke, A.: LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol.\u00a05195, pp. 162\u2013170. Springer, Heidelberg (2008)"},{"key":"13_CR7","doi-asserted-by":"crossref","unstructured":"Bertot, Y., Casteran, P.: Interactive Theorem Proving and Program Development - Coq\u2019Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. Springer (2004)","DOI":"10.1007\/978-3-662-07964-5"},{"issue":"2","key":"13_CR8","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/s10817-010-9213-y","volume":"47","author":"M.P. Bonacina","year":"2011","unstructured":"Bonacina, M.P., Lynch, C., de Moura, L.M.: On deciding satisfiability by theorem proving with speculative inferences. J. Autom. Reasoning\u00a047(2), 161\u2013189 (2011)","journal-title":"J. Autom. Reasoning"},{"key":"13_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/978-3-642-31365-3_11","volume-title":"Automated Reasoning","author":"C.E. Brown","year":"2012","unstructured":"Brown, C.E.: Satallax: An Automatic Higher-Order Prover. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol.\u00a07364, pp. 111\u2013117. Springer, Heidelberg (2012)"},{"key":"13_CR10","unstructured":"Carlson, A., Cumby, C., Rosen, J., Roth, D.: SNoW User\u2019s Guide. Technical Report UIUC-DCS-R-99-210, University of Illinois at Urbana-Champaign (1999)"},{"key":"13_CR11","unstructured":"Claessen, K., Sorensson, N.: New Techniques that Improve MACE-style Finite Model Finding. In: Baumgartner, P., Fermueller, C. (eds.) Proceedings of the CADE-19 Workshop: Model Computation - Principles, Algorithms, Applications (2003)"},{"key":"13_CR12","series-title":"RISC-Linz Report Series No. 97-50","first-page":"58","volume-title":"Int. Workshop on First-Order Theorem Proving (FTP 1997)","author":"I. Dahn","year":"1997","unstructured":"Dahn, I., Wernhard, C.: First order proof problems extracted from an article in the MIZAR Mathematical Library. In: Bonacina, M.P., Furbach, U. (eds.) Int. Workshop on First-Order Theorem Proving (FTP 1997). RISC-Linz Report Series No. 97-50, vol.\u00a0(97-50), pp. 58\u201362. Johannes Kepler Universit\u00e4t, Linz, Austria (1997)"},{"issue":"2","key":"13_CR13","first-page":"153","volume":"3","author":"A. Grabowski","year":"2010","unstructured":"Grabowski, A., Korni\u0142owicz, A., Naumowicz, A.: Mizar in a nutshell. Journal of Formalized Reasoning\u00a03(2), 153\u2013245 (2010)","journal-title":"Journal of Formalized Reasoning"},{"key":"13_CR14","unstructured":"H\u00e4hnle, R., Kerber, M., Weidenbach, C.: Common Syntax of the DFG-Schwerpunktprogramm Deduction. Technical Report TR 10\/96, Fakult\u00e4t f\u00fcr Informatik, Univers\u00e4t Karlsruhe, Karlsruhe, Germany (1996)"},{"key":"13_CR15","series-title":"Dagstuhl Seminar Proceedings","volume-title":"Mathematics, Algorithms, Proofs","author":"T.C. Hales","year":"2005","unstructured":"Hales, T.C.: Introduction to the Flyspeck project. In: Coquand, T., Lombardi, H., Roy, M.-F. (eds.) Mathematics, Algorithms, Proofs. Dagstuhl Seminar Proceedings, vol.\u00a005021, Internationales Begegnungs- und Forschungszentrum f\u00fcr Informatik (IBFI), Schloss Dagstuhl, Germany (2005)"},{"key":"13_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/BFb0031814","volume-title":"Formal Methods in Computer-Aided Design","author":"J. Harrison","year":"1996","unstructured":"Harrison, J.: HOL Light: A Tutorial Introduction. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol.\u00a01166, pp. 265\u2013269. Springer, Heidelberg (1996)"},{"key":"13_CR17","unstructured":"Jaskowski, S.: On the rules of suppositions. Studia Logica, 1 (1934)"},{"key":"13_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/978-3-540-74915-8_19","volume-title":"Computer Science Logic","author":"K. Korovin","year":"2007","unstructured":"Korovin, K., Voronkov, A.: Integrating Linear Arithmetic into Superposition Calculus. In: Duparc, J., Henzinger, T.A. (eds.) CSL 2007. LNCS, vol.\u00a04646, pp. 223\u2013237. Springer, Heidelberg (2007)"},{"key":"13_CR19","first-page":"3","volume":"4","author":"R. Matuszewski","year":"2005","unstructured":"Matuszewski, R., Rudnicki, P.: Mizar: the first 30 years. Mechanized Mathematics and Its Applications\u00a04, 3\u201324 (2005)","journal-title":"Mechanized Mathematics and Its Applications"},{"key":"13_CR20","unstructured":"McCune, W.W.: LADR: Library of Automated Deduction Routines, http:\/\/www.mcs.anl.gov\/AR\/ladr"},{"key":"13_CR21","doi-asserted-by":"crossref","unstructured":"McCune, W.W.: Mace4 Reference Manual and Guide. Technical Report ANL\/MCS-TM-264, Argonne National Laboratory, Argonne, USA (2003)","DOI":"10.2172\/822574"},{"key":"13_CR22","unstructured":"McCune, W.W.: Otter 3.3 Reference Manual. Technical Report ANL\/MSC-TM-263, Argonne National Laboratory, Argonne, USA (2003)"},{"issue":"1","key":"13_CR23","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1016\/j.jal.2007.07.004","volume":"7","author":"J. Meng","year":"2009","unstructured":"Meng, J., Paulson, L.C.: Lightweight relevance filtering for machine-generated resolution problems. J. Applied Logic\u00a07(1), 41\u201357 (2009)","journal-title":"J. Applied Logic"},{"key":"13_CR24","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1145\/505168.505170","volume-title":"FOIS 2001: Proceedings of the International Conference on Formal Ontology in Information Systems","author":"I. Niles","year":"2001","unstructured":"Niles, I., Pease, A.: Towards a standard upper ontology. In: FOIS 2001: Proceedings of the International Conference on Formal Ontology in Information Systems, pp. 2\u20139. ACM Press, New York (2001)"},{"key":"13_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.T.: Isabelle\/HOL - A Proof Assistant for Higher-Order Logic. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"13_CR26","doi-asserted-by":"crossref","unstructured":"Nonnengart, A., Weidenbach, C.: Computing small clause normal forms. In: Handbook of Automated Reasoning, vol.\u00a0I, pp. 335\u2013367. Elsevier and MIT Press (2001)","DOI":"10.1016\/B978-044450813-3\/50008-4"},{"issue":"1-2","key":"13_CR27","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1016\/S0747-7171(03)00037-3","volume":"36","author":"J. Otten","year":"2003","unstructured":"Otten, J., Bibel, W.: leanCoP: Lean Connection-Based Theorem Proving. Journal of Symbolic Computation\u00a036(1-2), 139\u2013161 (2003)","journal-title":"Journal of Symbolic Computation"},{"key":"13_CR28","unstructured":"Prevosto, V., Waldmann, U.: SPASS+T. In: Sutcliffe, G., Schmidt, R., Schulz, S. (eds.) ESCoR 2006. CEUR, vol.\u00a0192, pp. 18\u201333 (2006)"},{"issue":"1","key":"13_CR29","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1007\/BF00263451","volume":"8","author":"A. Quaife","year":"1992","unstructured":"Quaife, A.: Automated Deduction in von Neumann-Bernays-Godel Set Theory. Journal of Automated Reasoning\u00a08(1), 91\u2013147 (1992)","journal-title":"Journal of Automated Reasoning"},{"key":"13_CR30","unstructured":"Quaife, A.: Automated Development of Fundamental Mathematical Theories. Kluwer Academic Publishers (1992)"},{"key":"13_CR31","unstructured":"Ramachandran, D., Reagan, P., Goolsbey, K.: First-orderized ResearchCyc: Expressiveness and Efficiency in a Common Sense Knowledge Base. In: Shvaiko, P. (ed.) Proceedings of the Workshop on Contexts and Ontologies: Theory, Practice and Applications (2005)"},{"issue":"2-3","key":"13_CR32","first-page":"91","volume":"15","author":"A. Riazanov","year":"2002","unstructured":"Riazanov, A., Voronkov, A.: The Design and Implementation of Vampire. AI Communications\u00a015(2-3), 91\u2013110 (2002)","journal-title":"AI Communications"},{"issue":"2-3","key":"13_CR33","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"},{"issue":"6","key":"13_CR34","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"},{"key":"13_CR35","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1007\/978-3-540-73595-3_20","volume-title":"Automated Deduction \u2013 CADE-21","author":"G. Sutcliffe","year":"2007","unstructured":"Sutcliffe, G., Puzis, Y.: SRASS - A Semantic Relevance Axiom Selection System. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol.\u00a04603, pp. 295\u2013310. Springer, Heidelberg (2007)"},{"issue":"1","key":"13_CR36","doi-asserted-by":"crossref","first-page":"59","DOI":"10.3233\/AIC-2009-0441","volume":"22","author":"G. Sutcliffe","year":"2009","unstructured":"Sutcliffe, G.: The 4th IJCAR automated theorem proving system competition - CASC-J4. AI Commun.\u00a022(1), 59\u201372 (2009)","journal-title":"AI Commun."},{"key":"13_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-17511-4_1","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"G. Sutcliffe","year":"2010","unstructured":"Sutcliffe, G.: The TPTP World \u2013 Infrastructure for Automated Reasoning. In: Clarke, E.M., Voronkov, A. (eds.) LPAR-16 2010. LNCS, vol.\u00a06355, pp. 1\u201312. Springer, Heidelberg (2010)"},{"key":"13_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1007\/3-540-36469-2_16","volume-title":"Mathematical Knowledge Management","author":"J. Urban","year":"2003","unstructured":"Urban, J.: Translating Mizar for First Order Theorem Provers. In: Asperti, A., Buchberger, B., Davenport, J.H. (eds.) MKM 2003. LNCS, vol.\u00a02594, pp. 203\u2013215. Springer, Heidelberg (2003)"},{"issue":"3-4","key":"13_CR39","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/s10817-004-6245-1","volume":"33","author":"J. Urban","year":"2004","unstructured":"Urban, J.: MPTP - Motivation, Implementation, First Experiments. Journal of Automated Reasoning\u00a033(3-4), 319\u2013339 (2004)","journal-title":"Journal of Automated Reasoning"},{"key":"13_CR40","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 Presentation of MML Easy. In: Kohlhase, M. (ed.) MKM 2005. LNCS (LNAI), vol.\u00a03863, pp. 346\u2013360. Springer, Heidelberg (2006)"},{"key":"13_CR41","unstructured":"Urban, J.: MaLARea: a Metasystem for Automated Reasoning in Large Theories. In: Urban, J., Sutcliffe, G., Schulz, S. (eds.) Proceedings of the CADE-21 Workshop on Empirically Successful Automated Reasoning in Large Theories, pp. 45\u201358 (2007)"},{"issue":"1-2","key":"13_CR42","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/s10817-006-9032-3","volume":"37","author":"J. Urban","year":"2007","unstructured":"Urban, J.: MPTP 0.2: Design, Implementation, and Initial Experiments. Journal of Automated Reasoning\u00a037(1-2), 21\u201343 (2007)","journal-title":"Journal of Automated Reasoning"},{"key":"13_CR43","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"546","DOI":"10.1007\/978-3-540-75560-9_39","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"J. Urban","year":"2007","unstructured":"Urban, J., Sutcliffe, G.: ATP Cross-Verification of the Mizar MPTP Challenge Problems. In: Dershowitz, N., Voronkov, A. (eds.) LPAR 2007. LNCS (LNAI), vol.\u00a04790, pp. 546\u2013560. Springer, Heidelberg (2007)"},{"key":"13_CR44","unstructured":"Urban, J., Trac, S., Sutcliffe, G., Puzis, Y.: Combining Mizar and TPTP Semantic Presentation Tools. In: Proceedings of the Mathematical User-Interfaces Workshop 2007 (2007)"},{"key":"13_CR45","unstructured":"Urban, J.: An overview of methods for large-theory automated theorem proving (invited paper). In: H\u00f6fner, A., McIver, G. (eds.) ATE Workshop. CEUR Workshop Proceedings, vol.\u00a0760, pp. 3\u20138. CEUR-WS.org (2011)"},{"key":"13_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"455","DOI":"10.1007\/978-3-642-14128-7_38","volume-title":"Intelligent Computer Mathematics","author":"J. Urban","year":"2010","unstructured":"Urban, J., Alama, J., Rudnicki, P., Geuvers, H.: A Wiki for Mizar: Motivation, Considerations, and Initial Prototype. In: Autexier, S., Calmet, J., Delahaye, D., Ion, P.D.F., Rideau, L., Rioboo, R., Sexton, A.P. (eds.) AISC 2010. LNCS, vol.\u00a06167, pp. 455\u2013469. Springer, Heidelberg (2010)"},{"issue":"2","key":"13_CR47","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/s10817-012-9269-y","volume":"50","author":"J. Urban","year":"2013","unstructured":"Urban, J., Rudnicki, P., Sutcliffe, G.: ATP and Presentation Service for Mizar Formalizations. J. Autom. Reasoning\u00a050(2), 229\u2013241 (2013)","journal-title":"J. Autom. Reasoning"},{"key":"13_CR48","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., Pudl\u00e1k, P., Vysko\u010dil, J.: MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol.\u00a05195, pp. 441\u2013456. Springer, Heidelberg (2008)"},{"key":"13_CR49","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/978-3-642-22119-4_21","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"J. Urban","year":"2011","unstructured":"Urban, J., Vysko\u010dil, J., \u0160t\u011bp\u00e1nek, P.: MaLeCoP Machine Learning Connection Prover. In: Br\u00fcnnler, K., Metcalfe, G. (eds.) TABLEAUX 2011. LNCS, vol.\u00a06793, pp. 263\u2013277. Springer, Heidelberg (2011)"},{"key":"13_CR50","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1007\/978-3-642-02959-2_10","volume-title":"Automated Deduction \u2013 CADE-22","author":"C. Weidenbach","year":"2009","unstructured":"Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Suda, M., Wischnewski, P.: SPASS Version 3.5. In: Schmidt, R.A. (ed.) CADE 2009. LNCS, vol.\u00a05663, pp. 140\u2013145. Springer, Heidelberg (2009)"},{"key":"13_CR51","unstructured":"Wiedijk, F.: CHECKER - notes on the basic inference step in Mizar (2000), http:\/\/www.cs.kun.nl\/~freek\/mizar\/by.dvi"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning and Mathematics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-36675-8_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,7,23]],"date-time":"2020-07-23T00:11:30Z","timestamp":1595463090000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-36675-8_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642366741","9783642366758"],"references-count":51,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-36675-8_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}