{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,1,10]],"date-time":"2023-01-10T20:15:18Z","timestamp":1673381718302},"reference-count":24,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2012,1,1]],"date-time":"2012-01-01T00:00:00Z","timestamp":1325376000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Ann Math Artif Intell"],"published-print":{"date-parts":[[2012,1]]},"DOI":"10.1007\/s10472-011-9274-6","type":"journal-article","created":{"date-parts":[[2012,1,7]],"date-time":"2012-01-07T06:52:18Z","timestamp":1325919138000},"page":"1-37","source":"Crossref","is-referenced-by-count":6,"title":["Formalization of a normalization theorem in simplicial topology"],"prefix":"10.1007","volume":"64","author":[{"given":"Laureano","family":"Lamb\u00e1n","sequence":"first","affiliation":[]},{"given":"Francisco-Jes\u00fas","family":"Mart\u00edn\u2013Mateos","sequence":"additional","affiliation":[]},{"given":"Julio","family":"Rubio","sequence":"additional","affiliation":[]},{"given":"Jos\u00e9-Luis","family":"Ruiz\u2013Reina","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2012,1,8]]},"reference":[{"key":"9274_CR1","unstructured":"Andr\u00e9s,\u00a0M., Lamb\u00e1n,\u00a0L., Rubio,\u00a0J., Ruiz-Reina,\u00a0J.L.: Formalizing simplicial topology in ACL2. In: Proceedings ACL2 Workshop 2007, pp.\u00a034\u201339. University of Austin (2007)"},{"issue":"4","key":"9274_CR2","doi-asserted-by":"crossref","first-page":"271","DOI":"10.1007\/s10817-007-9094-x","volume":"40","author":"C Aransay","year":"2008","unstructured":"Aransay,\u00a0C., Ballarin,\u00a0C., Rubio,\u00a0J.: A mechanized proof of the basic perturbation lemma. J. Autom. Reason. 40(4), 271\u2013292 (2008)","journal-title":"J. Autom. Reason."},{"issue":"2","key":"9274_CR3","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1007\/s00165-009-0120-0","volume":"22","author":"C Aransay","year":"2010","unstructured":"Aransay,\u00a0C., Ballarin,\u00a0C., Rubio,\u00a0J.: Generating certified code from formal proofs: a case study in homological algebra. Form. Asp. Comput. 22(2), 193\u2013213 (2010)","journal-title":"Form. Asp. Comput."},{"key":"9274_CR4","doi-asserted-by":"crossref","unstructured":"Coquand,\u00a0T., Spiwack,\u00a0A.: Towards constructive homological algebra in type theory. In: Calculemus 2007, Lecture Notes in Artificial Intelligence, vol.\u00a04573, pp.\u00a040\u201354. Springer (2007)","DOI":"10.1007\/978-3-540-73086-6_4"},{"key":"9274_CR5","doi-asserted-by":"crossref","unstructured":"De Loera,\u00a0J.A., Rambau,\u00a0J., Santos,\u00a0F.: Triangulations. Structures for Algorithms and Applications. Springer (2010)","DOI":"10.1007\/978-3-642-12971-1"},{"key":"9274_CR6","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1051\/ita:2007015","volume":"41","author":"C Dom\u00ednguez","year":"2007","unstructured":"Dom\u00ednguez,\u00a0C., Lamb\u00e1n,\u00a0L., Rubio,\u00a0J.: Object-oriented institutions to specify symbolic computation systems. Rairo-Theor. Inform. Appl. 41, 191\u2013214 (2007)","journal-title":"Rairo-Theor. Inform. Appl."},{"key":"9274_CR7","doi-asserted-by":"crossref","unstructured":"Dom\u00ednguez,\u00a0C., Rubio,\u00a0J.: Computing in coq with infinite algebraic data structures. In: Calculemus 2010, Lecture Notes in Artificial Intelligence, vol. 6167, pp. 204\u2013218. Springer (2010)","DOI":"10.1007\/978-3-642-14128-7_18"},{"key":"9274_CR8","unstructured":"Dousson,\u00a0X., Sergeraert,\u00a0F., Siret,\u00a0Y.: The Kenzo Program. Institut Fourier, Grenoble (1999) http:\/\/www-fourier.ujf-grenoble.fr\/~sergerar\/Kenzo\/"},{"key":"9274_CR9","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1007\/BF01452241","volume":"1","author":"DBA Epstein","year":"1966","unstructured":"Epstein,\u00a0D.B.A.: Semisimplicial objects and the Eilenberg\u2013Zilber theorem. Invent. Math. 1, 209\u2013220 (1966)","journal-title":"Invent. Math."},{"key":"9274_CR10","doi-asserted-by":"crossref","unstructured":"Heras,\u00a0J., Pascual,\u00a0V., Rubio,\u00a0J.: Proving with ACL2 the correctness of simplicial sets in the Kenzo system. In: LOPSTR 2010, Lecture Notes in Computer Science, vol.\u00a06564, pp.\u00a0 37\u201351. Springer (2010)","DOI":"10.1007\/978-3-642-20551-4_3"},{"key":"9274_CR11","doi-asserted-by":"crossref","unstructured":"Kaufmann, M., Manolios, P., Moore, J S.: Computer-Aided Reasoning: An Approach. Kluwer (2000)","DOI":"10.1007\/978-1-4615-4449-4"},{"issue":"3","key":"9274_CR12","doi-asserted-by":"crossref","first-page":"187","DOI":"10.1007\/s00200-003-0129-1","volume":"14","author":"L Lamb\u00e1n","year":"2003","unstructured":"Lamb\u00e1n,\u00a0L., Pascual,\u00a0V., Rubio,\u00a0J.: An object-oriented interpretation of the EAT System. Appl. Algebra Eng. Commun. Comput. 14(3), 187\u2013215 (2003)","journal-title":"Appl. Algebra Eng. Commun. Comput."},{"key":"9274_CR13","doi-asserted-by":"crossref","unstructured":"Lamb\u00e1n,\u00a0L., Mart\u00edn\u2013Mateos,\u00a0F.J., Rubio,\u00a0J., Ruiz\u2013Reina,\u00a0J.L.: Applying ACL2 to the formalization of algebraic topology: simplicial polynomials. In: Interactive Theorem Proving 2011, Lecture Notes in Computer Science, vol.\u00a06898, pp.\u00a0200\u2013215. Springer (2011)","DOI":"10.1007\/978-3-642-22863-6_16"},{"key":"9274_CR14","doi-asserted-by":"crossref","unstructured":"Mac Lane,\u00a0S.: Homology. Springer (1963)","DOI":"10.1007\/978-3-642-62029-4"},{"key":"9274_CR15","doi-asserted-by":"crossref","unstructured":"Mac Lane,\u00a0S.: Categories for the Working Mathematician. Springer (1971)","DOI":"10.1007\/978-1-4612-9839-7"},{"key":"9274_CR16","doi-asserted-by":"crossref","unstructured":"Mac Lane,\u00a0S., Moerdijk,\u00a0I.: Sheaves in Geometry and Logic. Springer (1992)","DOI":"10.1007\/978-1-4612-0927-0"},{"key":"9274_CR17","unstructured":"Mart\u00edn\u2013Mateos,\u00a0F.J., Alonso,\u00a0J.A., Hidalgo,\u00a0M.J., Ruiz\u2013Reina,\u00a0J.L.: A generic instantiation tool and a case study: a generic multiset theory. In: Proceedings of the Third International ACL2 Workshop and its Applications, pp.\u00a0188\u2013201 (2002)"},{"key":"9274_CR18","doi-asserted-by":"crossref","unstructured":"Mart\u00edn\u2013Mateos,\u00a0F.J., Rubio,\u00a0J., Ruiz\u2013Reina,\u00a0J.L.: ACL2 verification of simplicial degeneracy programs in the Kenzo system. In: Calculemus 2009, Lecture Notes in Artificial Intelligence, vol.\u00a05625, pp. 106\u2013121. Springer (2009)","DOI":"10.1007\/978-3-642-02614-0_13"},{"key":"9274_CR19","unstructured":"May,\u00a0J.P.: Simplicial Objects in Algebraic Topology. Van Nostrand (1967)"},{"issue":"1","key":"9274_CR20","doi-asserted-by":"crossref","first-page":"96","DOI":"10.1016\/j.jsc.2009.07.002","volume":"45","author":"I Medina\u2013Bulo","year":"2010","unstructured":"Medina\u2013Bulo,\u00a0I., Palomo\u2013Lozano,\u00a0F., Ruiz\u2013Reina,\u00a0J.L.: A verified common lisp implementation of Buchberger\u2019s algorithm in ACL2. J. Symb. Comput. 45(1), 96\u2013123 (2010)","journal-title":"J. Symb. Comput."},{"issue":"5","key":"9274_CR21","doi-asserted-by":"crossref","first-page":"51","DOI":"10.4310\/HHA.2000.v2.n1.a5","volume":"2","author":"P Real","year":"2000","unstructured":"Real,\u00a0P.: Homological perturbation theory and associativity. Homol. Homotopy Appl. 2(5), 51\u201388 (2000)","journal-title":"Homol. Homotopy Appl."},{"key":"9274_CR22","unstructured":"Romero,\u00a0A.: Effective homology and spectral sequences. PhD Thesis. Universidad de La Rioja (2007). Available at: http:\/\/www.unirioja.es\/cu\/anromero\/tesis.pdf"},{"key":"9274_CR23","first-page":"35","volume":"192","author":"J Rubio","year":"1990","unstructured":"Rubio,\u00a0J., Sergeraert,\u00a0F.: Supports acycliques and algorithmique. Ast\u00e9risque 192, 35\u201355 (1990)","journal-title":"Ast\u00e9risque"},{"key":"9274_CR24","doi-asserted-by":"crossref","first-page":"389","DOI":"10.1016\/S0007-4497(02)01119-3","volume":"126","author":"J Rubio","year":"2002","unstructured":"Rubio,\u00a0J., Sergeraert,\u00a0F.: Constructive algebraic topology. Bull. Sci. Math. 126, 389\u2013412 (2002)","journal-title":"Bull. Sci. Math."}],"container-title":["Annals of Mathematics and Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-011-9274-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10472-011-9274-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-011-9274-6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,22]],"date-time":"2019-06-22T02:07:41Z","timestamp":1561169261000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10472-011-9274-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,1]]},"references-count":24,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2012,1]]}},"alternative-id":["9274"],"URL":"https:\/\/doi.org\/10.1007\/s10472-011-9274-6","relation":{},"ISSN":["1012-2443","1573-7470"],"issn-type":[{"value":"1012-2443","type":"print"},{"value":"1573-7470","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,1]]}}}