{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,2,21]],"date-time":"2023-02-21T02:30:01Z","timestamp":1676946601764},"reference-count":8,"publisher":"Springer Science and Business Media LLC","issue":"2","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2013,2]]},"DOI":"10.1007\/s10817-012-9265-2","type":"journal-article","created":{"date-parts":[[2012,10,26]],"date-time":"2012-10-26T05:58:31Z","timestamp":1351231111000},"page":"161-172","source":"Crossref","is-referenced-by-count":2,"title":["Formalization of Definitions and Theorems Related to an Elliptic Curve Over a Finite Prime Field by Using Mizar"],"prefix":"10.1007","volume":"50","author":[{"given":"Yuichi","family":"Futa","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hiroyuki","family":"Okazaki","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yasunari","family":"Shidama","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2012,10,27]]},"reference":[{"key":"9265_CR1","unstructured":"Mizar proof checker: http:\/\/mizar.org\/ (1973). Accessed 7 May 2011"},{"key":"9265_CR2","unstructured":"Bonarska, E.: An introduction to PC mizar. Mizar Users Group, Fondation Philippe le Hodey, Brussels (1990)"},{"issue":"3","key":"9265_CR3","doi-asserted-by":"crossref","first-page":"131","DOI":"10.2478\/v10037-011-0021-6","volume":"19","author":"Y Futa","year":"2011","unstructured":"Futa, Y., Okazaki, H., Shidama, Y.: Set of points on elliptic curve in projective coordinates. Formal. Math. 19(3), 131\u2013139 (2011)","journal-title":"Formal. Math."},{"key":"9265_CR4","doi-asserted-by":"crossref","unstructured":"Blake, I., Seroussi, G., Smart, N.: Elliptic Curves in Cryptography. London Mathematical Society Lecture Note Series, No. 265. Cambridge University Press (1999)","DOI":"10.1017\/CBO9781107360211"},{"issue":"1","key":"9265_CR5","first-page":"175","volume":"1","author":"C Byli\u0144ski","year":"1990","unstructured":"Byli\u0144ski, C.: Binary operations. Formal. Math. 1(1), 175\u2013180 (1990)","journal-title":"Formal. Math."},{"issue":"3","key":"9265_CR6","first-page":"501","volume":"1","author":"J Trybulec","year":"1990","unstructured":"Trybulec, J.: Integers. Formal. Math. 1(3), 501\u2013505 (1990)","journal-title":"Formal. Math."},{"issue":"2","key":"9265_CR7","first-page":"377","volume":"1","author":"G Bancerek","year":"1990","unstructured":"Bancerek, G.: Cardinal numbers. Formal. Math. 1(2), 377\u2013382 (1990)","journal-title":"Formal. Math."},{"issue":"3","key":"9265_CR8","first-page":"441","volume":"1","author":"K Raczkowski","year":"1990","unstructured":"Raczkowski, K., Sadowski, P.: Equivalence relations and classes of abstraction. Formal. Math. 1(3), 441\u2013444 (1990)","journal-title":"Formal. Math."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/www.springerlink.com\/index\/pdf\/10.1007\/s10817-012-9265-2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,21]],"date-time":"2017-06-21T01:54:29Z","timestamp":1498010069000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-012-9265-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,10,27]]},"references-count":8,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2013,2]]}},"alternative-id":["9265"],"URL":"https:\/\/doi.org\/10.1007\/s10817-012-9265-2","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,10,27]]}}}