06119067

j

06119067 Lamb\'an, Laureano Mart{\'\i}n-Mateos, Francisco-Jes\'us Rubio, Julio Ruiz-Reina, Jos\'e-Luis Formalization of a normalization theorem in simplicial topology. Ann. Math. Artif. Intell. 64, No. 1, 1-37 (2012). 2012 Springer, Dordrecht EN automated reasoning formalization of mathematics ACL2 algebraic topology normalization theorem

doi:10.1007/s10472-011-9274-6

Summary: 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.