{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,26]],"date-time":"2025-10-26T20:36:08Z","timestamp":1761510968137},"reference-count":25,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2012,11,6]],"date-time":"2012-11-06T00:00:00Z","timestamp":1352160000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2013,2]]},"DOI":"10.1007\/s10817-012-9269-y","type":"journal-article","created":{"date-parts":[[2012,11,5]],"date-time":"2012-11-05T10:45:06Z","timestamp":1352112306000},"page":"229-241","source":"Crossref","is-referenced-by-count":44,"title":["ATP and Presentation Service for Mizar Formalizations"],"prefix":"10.1007","volume":"50","author":[{"given":"Josef","family":"Urban","sequence":"first","affiliation":[]},{"given":"Piotr","family":"Rudnicki","sequence":"additional","affiliation":[]},{"given":"Geoff","family":"Sutcliffe","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2012,11,6]]},"reference":[{"key":"9269_CR1","unstructured":"Alama, J., K\u00fchlwein, D., Tsivtsivadze, E., Urban, J., Heskes, T.: Premise selection for mathematics by corpus analysis and kernel methods. ArXiv e-prints (2011)"},{"issue":"1","key":"9269_CR2","first-page":"91","volume":"1","author":"G Bancerek","year":"1990","unstructured":"Bancerek, G.: The ordinal numbers. J. Formaliz. Reason. 1(1), 91\u201396 (1990)","journal-title":"J. Formaliz. Reason."},{"key":"9269_CR3","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\u201997), pp. 58\u201362 (1997)"},{"issue":"2","key":"9269_CR4","first-page":"153","volume":"3","author":"A Grabowski","year":"2010","unstructured":"Grabowski, A., Kornilowicz, A., Naumowicz, A.: Mizar in a Nutshell. J. Formaliz. Reason. 3(2), 153\u2013245 (2010)","journal-title":"J. Formaliz. Reason."},{"issue":"3","key":"9269_CR5","doi-asserted-by":"crossref","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. Ann. Math. 162(3), 1065\u20131185 (2005)","journal-title":"Ann. Math."},{"key":"9269_CR6","unstructured":"Hales, T. (ed.): A Special Issue on Formal Proof of Notices of the AMS, vol. 55(11). American Mathematical Society (2008)"},{"key":"9269_CR7","doi-asserted-by":"crossref","unstructured":"Harrison, J.: Optimizing proof search in model elimination. In: McRobbie, M., Slaney, J.K. (eds.) Proceedings of the 13th International Conference on Automated Deduction. Lecture Notes in Artificial Intelligence, number 1104, pp. 313\u2013327. Springer (1996)","DOI":"10.1007\/3-540-61511-3_97"},{"key":"9269_CR8","doi-asserted-by":"crossref","unstructured":"Hoder, K., Voronkov, A.: Sine Qua Non for large theory reasoning. In: Sofronie-Stokkermans, V., Bj\u0153rner, N. (eds.) Proceedings of the 23rd International Conference on Automated Deduction. Lecture Notes in Artificial Intelligence, number 6803, pp. 299\u2013314. Springer (2011)","DOI":"10.1007\/978-3-642-22438-6_23"},{"key":"9269_CR9","unstructured":"Hurd, J.: First-order proof tactics in higher-order logic theorem provers. In: Archer, M., Di Vito, B., Mu\u00f1oz, C. (eds.) Design and Application of Strategies\/Tactics in Higher Order Logics (STRATA 2003), pp. 56\u201368. NASA Technical Reports, number NASA\/CP-2003-212448 (2003)"},{"key":"9269_CR10","doi-asserted-by":"crossref","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 (2009)","DOI":"10.1145\/1629575.1629596"},{"issue":"1","key":"9269_CR11","doi-asserted-by":"crossref","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. Appl. Log. 7(1), 41\u201357 (2009)","journal-title":"J. Appl. Log."},{"key":"9269_CR12","doi-asserted-by":"crossref","first-page":"161","DOI":"10.4064\/cm-3-2-161-162","volume":"3","author":"J Mycielski","year":"1955","unstructured":"Mycielski, J.: Sur le coloriage des graphes. Colloq. Math. 3, 161\u2013162 (1955)","journal-title":"Colloq. Math."},{"key":"9269_CR13","unstructured":"Paulson, L.C., Blanchette, J.C.: Three years of experience with Sledgehammer, a practical link between automated and interactive theorem provers. In: 8th IWIL. Invited talk (2010)"},{"key":"9269_CR14","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, number 257, pp. 59\u201369 (2007)"},{"issue":"2","key":"9269_CR15","doi-asserted-by":"crossref","first-page":"169","DOI":"10.2478\/v10037-012-0019-8","volume":"20","author":"P Rudnicki","year":"2012","unstructured":"Rudnicki, P., Stewart, L.: Simple graphs as simplicial complexes: the Mycielskian of a graph. Formalized Mathematics 20(2), 169\u2013183 (2012)","journal-title":"Formalized Mathematics"},{"key":"9269_CR16","doi-asserted-by":"crossref","unstructured":"Sutcliffe, G.: SystemOnTPTP. In: McAllester, D. (ed.) Proceedings of the 17th International Conference on Automated Deduction. Lecture Notes in Artificial Intelligence, number 1831, pp. 406\u2013410. Springer (2000)","DOI":"10.1007\/10721959_31"},{"key":"9269_CR17","doi-asserted-by":"crossref","unstructured":"Urban, J.: XML-izing Mizar: making semantic processing and presentaion of MML easy. In: Kohlhase, M. (ed.) Proceedings of the 4th International Conference on Mathematical Knowledge Management. Lecture Notes in Computer Science, number 3863, pp. 346\u2013360 (2005)","DOI":"10.1007\/11618027_23"},{"issue":"4","key":"9269_CR18","doi-asserted-by":"crossref","first-page":"414","DOI":"10.1016\/j.jal.2005.10.004","volume":"4","author":"J Urban","year":"2006","unstructured":"Urban, J.: MizarMode\u2014an integrated proof assistance tool for the mizar way of formalizing mathematics. J. Appl. Log. 4(4), 414\u2013427 (2006)","journal-title":"J. Appl. Log."},{"issue":"1\u20132","key":"9269_CR19","first-page":"21","volume":"37","author":"J Urban","year":"2006","unstructured":"Urban, J.: MPTP 0.2: design, implementation, and initial experiments. J. Autom. Reasoning 37(1\u20132), 21\u201343 (2006)","journal-title":"J. Autom. Reasoning"},{"key":"9269_CR20","unstructured":"Urban, J.: Parallelizing Mizar. CoRR. abs\/1206.0141 (2012)"},{"key":"9269_CR21","doi-asserted-by":"crossref","unstructured":"Urban, J., Alama, J., Rudnicki, P., Geuvers, H.: A Wiki for Mizar: motivation, considerations, and initial prototype. In: AISC\/MKM\/Calculemus. LNCS, vol. 6167, pp. 455\u2013469 (2010)","DOI":"10.1007\/978-3-642-14128-7_38"},{"key":"9269_CR22","doi-asserted-by":"crossref","unstructured":"Urban, J., Hoder, K., Voronkov, A.: Evaluation of automated theorem proving on the Mizar mathematical library. In: ICMS. LNCS, vol. 6327, pp. 155\u2013166 (2010)","DOI":"10.1007\/978-3-642-15582-6_30"},{"issue":"2","key":"9269_CR23","doi-asserted-by":"crossref","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. Math. Comput. Sci. 2(2), 231\u2013251 (2008)","journal-title":"Math. Comput. Sci."},{"key":"9269_CR24","doi-asserted-by":"crossref","unstructured":"Urban, J., Sutcliffe, G., Pudl\u00e1k, P., Vyskocil, J.: MaLARea SG1\u2014machine learner for automated reasoning with semantic guidance. In: IJCAR. LNCS, vol. 5195, pp. 441\u2013456 (2008)","DOI":"10.1007\/978-3-540-71070-7_37"},{"key":"9269_CR25","doi-asserted-by":"crossref","unstructured":"Vyskocil, J., Stanovsk\u00fd, D., Urban, J.: Automated proof compression by invention of new definitions. In: Clarke, E.M., Voronkov, A. (eds.) LPAR (Dakar). Lecture Notes in Computer Science, vol. 6355, pp. 447\u2013462. Springer (2010)","DOI":"10.1007\/978-3-642-17511-4_25"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-012-9269-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-012-9269-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-012-9269-y","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,7,5]],"date-time":"2019-07-05T03:45:55Z","timestamp":1562298355000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-012-9269-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,11,6]]},"references-count":25,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2013,2]]}},"alternative-id":["9269"],"URL":"https:\/\/doi.org\/10.1007\/s10817-012-9269-y","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,11,6]]}}}