{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,10]],"date-time":"2026-01-10T01:15:49Z","timestamp":1768007749862,"version":"3.49.0"},"reference-count":11,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2012,11,1]],"date-time":"2012-11-01T00:00:00Z","timestamp":1351728000000},"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-9266-1","type":"journal-article","created":{"date-parts":[[2012,10,31]],"date-time":"2012-10-31T15:18:21Z","timestamp":1351696701000},"page":"147-160","source":"Crossref","is-referenced-by-count":5,"title":["Custom Automations in Mizar"],"prefix":"10.1007","volume":"50","author":[{"given":"Marco Bright","family":"Caminati","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Giuseppe","family":"Rosolini","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2012,11,1]]},"reference":[{"key":"9266_CR1","doi-asserted-by":"crossref","unstructured":"Bancerek, G., Urban, J.: Integrated semantic browsing of the Mizar mathematical library for authoring Mizar articles. In: Mathematical Knowledge Management, pp. 44\u201357. Springer (2004)","DOI":"10.1007\/978-3-540-27818-4_4"},{"issue":"2","key":"9266_CR2","doi-asserted-by":"crossref","first-page":"141","DOI":"10.1007\/s10817-007-9073-2","volume":"39","author":"P Cairns","year":"2007","unstructured":"Cairns, P., Gow, J.: Integrating searching and authoring in Mizar. J. Autom. Reason. 39(2), 141\u2013160 (2007)","journal-title":"J. Autom. Reason."},{"issue":"3","key":"9266_CR3","doi-asserted-by":"crossref","first-page":"155","DOI":"10.2478\/v10037-011-0025-2","volume":"19","author":"M Caminati","year":"2011","unstructured":"Caminati, M.: Preliminaries to classical first-order model theory. Form. Math. 19(3), 155\u2013167 (2011)","journal-title":"Form. Math."},{"issue":"2","key":"9266_CR4","first-page":"153","volume":"3","author":"A Grabowski","year":"2010","unstructured":"Grabowski, A., Korni\u0142owicz, A., Naumowicz, A.: Mizar in a nutshell. J. Form. Reason. 3(2), 153\u2013245 (2010)","journal-title":"J. Form. Reason."},{"issue":"23","key":"9266_CR5","first-page":"191","volume":"10","author":"A Naumowicz","year":"2007","unstructured":"Naumowicz, A.: Evaluating prospective built-in elements of computer algebra in Mizar. Stud. Log. Gramm. Rhetor. 10(23), 191\u2013200 (2007)","journal-title":"Stud. Log. Gramm. Rhetor."},{"key":"9266_CR6","doi-asserted-by":"crossref","unstructured":"Naumowicz, A., Byli\u0144ski, C.: Improving Mizar texts with properties and requirements. In: Mathematical Knowledge Management, pp. 290\u2013301. Springer (2004)","DOI":"10.1007\/978-3-540-27818-4_21"},{"issue":"3","key":"9266_CR7","doi-asserted-by":"crossref","first-page":"197","DOI":"10.1023\/A:1006218513245","volume":"23","author":"P Rudnicki","year":"1999","unstructured":"Rudnicki, P., Trybulec, A.: On equivalents of well-foundedness. J. Autom. Reason. 23(3), 197\u2013234 (1999)","journal-title":"J. Autom. Reason."},{"key":"9266_CR8","unstructured":"Rudnicki, P., Urban, J.: Escape to ATP for Mizar. In: First Workshop on Proof eXchange for Theorem Proving. http:\/\/pxtp2011.loria.fr\/ (2011). Accessed 23 Oct 2012"},{"issue":"4","key":"9266_CR9","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\u2013an 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","key":"9266_CR10","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1142\/S0218213006002588","volume":"15","author":"J Urban","year":"2006","unstructured":"Urban, J.: MoMM-fast interreduction and retrieval in large libraries of formalized mathematics. Int. J. Artif. Intell. Tools 15(1), 109 (2006)","journal-title":"Int. J. Artif. Intell. Tools"},{"key":"9266_CR11","doi-asserted-by":"crossref","unstructured":"Wiedijk, F.: Mizar\u2019s soft type system. In: Proceedings of the 20th International Conference on Theorem Proving in Higher Order Logics, pp. 383\u2013399. Springer (2007)","DOI":"10.1007\/978-3-540-74591-4_28"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-012-9266-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-012-9266-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-012-9266-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T21:21:52Z","timestamp":1559251312000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-012-9266-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,11,1]]},"references-count":11,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2013,2]]}},"alternative-id":["9266"],"URL":"https:\/\/doi.org\/10.1007\/s10817-012-9266-1","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,11,1]]}}}