{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T20:56:31Z","timestamp":1725656191708},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642275487"},{"type":"electronic","value":"9783642275494"}],"license":[{"start":{"date-parts":[[2012,1,1]],"date-time":"2012-01-01T00:00:00Z","timestamp":1325376000000},"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":[[2012]]},"DOI":"10.1007\/978-3-642-27549-4_15","type":"book-chapter","created":{"date-parts":[[2012,1,31]],"date-time":"2012-01-31T20:53:22Z","timestamp":1328043202000},"page":"113-120","source":"Crossref","is-referenced-by-count":3,"title":["A Certified Module to Study Digital Images with the Kenzo System"],"prefix":"10.1007","author":[{"given":"J\u00f3nathan","family":"Heras","sequence":"first","affiliation":[]},{"given":"Vico","family":"Pascual","sequence":"additional","affiliation":[]},{"given":"Julio","family":"Rubio","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"15_CR1","unstructured":"Andr\u00e9s, M., Lamb\u00e1n, L., Rubio, J., Ruiz-Reina, J.L.: Formalizing Simplicial Topology in ACL2. In: Proceedings of ACL2 Workshop 2007, pp. 34\u201339 (2007)"},{"issue":"4","key":"15_CR2","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/s10817-007-9094-x","volume":"40","author":"J. Aransay","year":"2008","unstructured":"Aransay, J., Ballarin, C., Rubio, J.: A mechanized proof of the Basic Perturbation Lemma. Journal of Automated Reasoning\u00a040(4), 271\u2013292 (2008)","journal-title":"Journal of Automated Reasoning"},{"key":"15_CR3","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/S0166-218X(02)00221-4","volume":"125","author":"R. Ayala","year":"2003","unstructured":"Ayala, R., Dom\u00ednguez, E., Franc\u00e9s, A.R., Quintero, A.: Homotopy in digital spaces. Discrete Applied Mathematics\u00a0125, 3\u201324 (2003)","journal-title":"Discrete Applied Mathematics"},{"key":"15_CR4","doi-asserted-by":"publisher","first-page":"962","DOI":"10.1016\/j.tcs.2010.11.016","volume":"412","author":"C. Dom\u00ednguez","year":"2011","unstructured":"Dom\u00ednguez, C., Rubio, J.: Effective Homology of Bicomplexes, formalized in Coq. Theoretical Computer Science\u00a0412, 962\u2013970 (2011)","journal-title":"Theoretical Computer Science"},{"key":"15_CR5","unstructured":"Dousson, X., Rubio, J., Sergeraert, F., Siret, Y.: The Kenzo program. Institut Fourier, Grenoble (1998), \n                    \n                      http:\/\/www-fourier.ujf-grenoble.fr\/~sergerar\/Kenzo\/"},{"issue":"2-3","key":"15_CR6","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1016\/j.dam.2004.09.014","volume":"147","author":"R. Gonz\u00e1lez-D\u00edaz","year":"2005","unstructured":"Gonz\u00e1lez-D\u00edaz, R., Real, P.: On the Cohomology of 3D Digital Images. Discrete Applied Math.\u00a0147(2-3), 245\u2013263 (2005)","journal-title":"Discrete Applied Math."},{"key":"15_CR7","unstructured":"Heras, J.: Digital Imaging programs for the Kenzo system. University of La Rioja (2010), \n                    \n                      http:\/\/www.unirioja.es\/cu\/joheras\/Digital-Images.rar"},{"key":"15_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/978-3-642-20551-4_3","volume-title":"Logic-Based Program Synthesis and Transformation","author":"J. Heras","year":"2011","unstructured":"Heras, J., Pascual, V., Rubio, J.: Proving with ACL2 the correctness of simplicial sets in the Kenzo system. In: Alpuente, M. (ed.) LOPSTR 2010. LNCS, vol.\u00a06564, pp. 37\u201351. Springer, Heidelberg (2011)"},{"key":"15_CR9","volume-title":"Computer-Aided Reasoning: An approach","author":"M. Kaufmann","year":"2000","unstructured":"Kaufmann, M., Manolios, P., Moore, J.S.: Computer-Aided Reasoning: An approach. Kluwer Academic Publishers, Dordrecht (2000)"},{"key":"15_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/978-3-642-22863-6_16","volume-title":"Interactive Theorem Proving","author":"L. Lamb\u00e1n","year":"2011","unstructured":"Lamb\u00e1n, L., Mart\u00edn-Mateos, F.J., Rubio, J., Ruiz-Reina, J.L.: Applying ACL2 to the Formalization of Algebraic Topology: Simplicial Polynomials. In: van Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) ITP 2011. LNCS, vol.\u00a06898, pp. 200\u2013215. Springer, Heidelberg (2011)"},{"key":"15_CR11","doi-asserted-by":"publisher","first-page":"756","DOI":"10.1126\/science.301.5634.756","volume":"8","author":"D. Mackenzie","year":"2003","unstructured":"Mackenzie, D.: Topologists and Roboticists Explore and Inchoate World. Science\u00a08, 756 (2003)","journal-title":"Science"},{"key":"15_CR12","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-62029-4","volume-title":"Homology","author":"S. MacLane","year":"1963","unstructured":"MacLane, S.: Homology. Springer, Heidelberg (1963)"},{"key":"15_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"106","DOI":"10.1007\/978-3-642-02614-0_13","volume-title":"Intelligent Computer Mathematics","author":"F.J. Mart\u00edn-Mateos","year":"2009","unstructured":"Mart\u00edn-Mateos, F.J., Rubio, J., Ruiz-Reina, J.L.: ACL2 verification of simplicial degeneracy programs in the Kenzo system. In: Carette, J., Dixon, L., Coen, C.S., Watt, S.M. (eds.) CALCULEMUS 2009. LNCS, vol.\u00a05625, pp. 106\u2013121. Springer, Heidelberg (2009)"},{"key":"15_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"695","DOI":"10.1007\/978-3-540-39903-2_85","volume-title":"Medical Image Computing and Computer-Assisted Intervention - MICCAI 2003","author":"F. S\u00e9gonne","year":"2003","unstructured":"S\u00e9gonne, F., Grimson, E., Fischl, B.: Topological Correction of Subcortical Segmentation. In: Ellis, R.E., Peters, T.M. (eds.) MICCAI 2003. LNCS, vol.\u00a02879, pp. 695\u2013702. Springer, Heidelberg (2003)"},{"key":"15_CR15","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1016\/0097-3165(89)90053-8","volume":"50","author":"J. Wood","year":"1989","unstructured":"Wood, J.: Spinor groups and algebraic coding theory. Journal of Combinatorial Theory\u00a050, 277\u2013313 (1989)","journal-title":"Journal of Combinatorial Theory"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Systems Theory \u2013 EUROCAST 2011"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-27549-4_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,26]],"date-time":"2019-04-26T00:47:31Z","timestamp":1556239651000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-27549-4_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642275487","9783642275494"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-27549-4_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}