Lambán Pardo, LaureanoMartín Mateos, Francisco JesúsRubio, JulioRuiz Reina, José Luis2019-05-132019-05-132012Lambán Pardo, L., Martín Mateos, F.J., Rubio, J. y Ruiz Reina, J.L. (2012). Formalization of a normalization theorem in simplicial topology. Annals of Mathematics and Artificial Intelligence, 64 (1), 1-37.1012-2443https://hdl.handle.net/11441/86280In this paper we present a complete formalization of the Normalization Theorem, a result in Algebraic Simplicial Topology stating that there exists a homotopy equivalence between the chain complex of a simplicial set, and a smaller chain complex for the same simplicial set, called the normalized chain complex. Even if the Normalization Theorem is usually stated as a higher-order result (with a Category Theory flavor) we manage to give a first-order proof of it. To this aim it is instrumental the introduction of an algebraic data structure called simplicial polynomial. As a demonstration of the validity of our techniques we developed a formal proof in the ACL2 theorem prover.application/pdfengAttribution-NonCommercial-NoDerivatives 4.0 Internacionalhttp://creativecommons.org/licenses/by-nc-nd/4.0/Automated reasoningFormalization of mathematicsACL2Algebraic topologyNormalization theoreminfo:eu-repo/semantics/articleinfo:eu-repo/semantics/openAccesshttps://doi.org/10.1007/s10472-011-9274-6