{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,11,11]],"date-time":"2026-11-11T07:07:38Z","timestamp":1794380858521,"version":"4.9.0"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642155819","type":"print"},{"value":"9783642155826","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-15582-6_30","type":"book-chapter","created":{"date-parts":[[2010,9,10]],"date-time":"2010-09-10T05:15:44Z","timestamp":1284095744000},"page":"155-166","source":"Crossref","is-referenced-by-count":18,"title":["Evaluation of Automated Theorem Proving on the Mizar Mathematical Library"],"prefix":"10.1007","author":[{"given":"Josef","family":"Urban","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Krystof","family":"Hoder","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Andrei","family":"Voronkov","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"30_CR1","first-page":"530","volume-title":"IJCAI","author":"M. Davis","year":"1981","unstructured":"Davis, M.: Obvious logical inferences. In: Hayes, P.J. (ed.) IJCAI, pp. 530\u2013531. William Kaufmann, San Francisco (1981)"},{"issue":"1","key":"30_CR2","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2478\/v10037-007-0001-z","volume":"15","author":"Y. Ding","year":"2007","unstructured":"Ding, Y.: Several classes of BCI-algebras and their properties. Formalized Mathematics\u00a015(1), 1\u20139 (2007)","journal-title":"Formalized Mathematics"},{"issue":"4","key":"30_CR3","first-page":"803","volume":"1","author":"J. Kotowicz","year":"1990","unstructured":"Kotowicz, J., Raczkowski, K., Sadowski, P.: Average value theorems for real functions of one variable. Formalized Mathematics\u00a01(4), 803\u2013805 (1990)","journal-title":"Formalized Mathematics"},{"key":"30_CR4","unstructured":"Matuszek, C., Cabral, J., Witbrock, M., DeOliveira, J.: An Introduction to the Syntax and Content of Cyc. In: Baral, C. (ed.) Proceedings of the 2006 AAAI Spring Symposium on Formalizing and Compiling Background Knowledge and Its Applications to Knowledge Representation and Question Answering, pp. 44\u201349 (2006)"},{"issue":"1","key":"30_CR5","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":"30_CR6","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 (2007)"},{"issue":"3","key":"30_CR7","doi-asserted-by":"publisher","first-page":"159","DOI":"10.2478\/v10037-007-0018-3","volume":"15","author":"M. Riccardi","year":"2007","unstructured":"Riccardi, M.: The Sylow theorems. Formalized Mathematics\u00a015(3), 159\u2013165 (2007)","journal-title":"Formalized Mathematics"},{"issue":"4","key":"30_CR8","doi-asserted-by":"publisher","first-page":"383","DOI":"10.1007\/BF00247436","volume":"3","author":"P. Rudnicki","year":"1987","unstructured":"Rudnicki, P.: Obvious inferences. J. Autom. Reasoning\u00a03(4), 383\u2013393 (1987)","journal-title":"J. Autom. Reasoning"},{"issue":"2-3","key":"30_CR9","first-page":"91","volume":"15","author":"A. Riazanov","year":"2002","unstructured":"Riazanov, A., Voronkov, A.: The design and implementation of VAMPIRE. Journal of AI Communications\u00a015(2-3), 91\u2013110 (2002)","journal-title":"Journal of AI Communications"},{"issue":"2-3","key":"30_CR10","first-page":"111","volume":"15","author":"S. Schulz","year":"2002","unstructured":"Schulz, S.: E \u2013 a brainiac theorem prover. Journal of AI Communications\u00a015(2-3), 111\u2013126 (2002)","journal-title":"Journal of AI Communications"},{"key":"30_CR11","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":"6","key":"30_CR12","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":"1-2","key":"30_CR13","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. J. Autom. Reasoning\u00a037(1-2), 21\u201343 (2006)","journal-title":"J. Autom. Reasoning"},{"issue":"2","key":"30_CR14","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1007\/s11786-008-0053-7","volume":"2","author":"J. Urban","year":"2008","unstructured":"Urban, J., Sutcliffe, G.: ATP-based cross-verification of Mizar proofs: Method, systems, and first experiments. Mathematics in Computer Science\u00a02(2), 231\u2013251 (2008)","journal-title":"Mathematics in Computer Science"},{"key":"30_CR15","series-title":"LNAI","first-page":"132","volume-title":"AISC 2010","author":"J. Urban","year":"2010","unstructured":"Urban, J., Sutcliffe, G.: Automated reasoning and presentation support for formalizing mathematics in Mizar. In: Autexier, S., Calmet, J., Delahaye, D., Ion, P.D.F., Rideau, L., Rioboo, R., Sexton, A.P. (eds.) AISC 2010. LNCS (LNAI), vol.\u00a06167, pp. 132\u2013146. Springer, Heidelberg (2010)"},{"key":"30_CR16","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: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol.\u00a05195, pp. 441\u2013456. Springer, Heidelberg (2008)"},{"key":"30_CR17","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"LPAR 2010","author":"J. Vyskocil","year":"2010","unstructured":"Vyskocil, J., Stanovsky, D., Urban, J.: Automated proof shortening by invention of new definitions. In: LPAR 2010. LNCS (LNAI). Springer, Heidelberg (to appear 2010)"},{"key":"30_CR18","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.) Automated Deduction \u2013 CADE-22. LNCS, vol.\u00a05663, pp. 140\u2013145. Springer, Heidelberg (2009)"},{"key":"30_CR19","unstructured":"Wiedijk, F.: CHECKER - notes on the basic inference step in Mizar (2000), \n                    \n                      http:\/\/www.cs.kun.nl\/~freek\/mizar\/by.dvi"},{"issue":"4","key":"30_CR20","doi-asserted-by":"publisher","first-page":"171","DOI":"10.2478\/v10037-007-0020-9","volume":"15","author":"F. Wiedijk","year":"2007","unstructured":"Wiedijk, F.: Arrow\u2019s impossibility theorem. Formalized Mathematics\u00a015(4), 171\u2013174 (2007)","journal-title":"Formalized Mathematics"}],"container-title":["Lecture Notes in Computer Science","Mathematical Software \u2013 ICMS 2010"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-15582-6_30.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,30]],"date-time":"2021-04-30T08:58:17Z","timestamp":1619773097000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-15582-6_30"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642155819","9783642155826"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-15582-6_30","relation":{"is-part-of":[{"id-type":"doi","id":"https:\/\/doi.org\/10.1007\/978-3-642-15582-6","asserted-by":"object"}]},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010]]}}}