id: 06119067
dt: j
an: 06119067
au: Lambán, Laureano; Martín-Mateos, Francisco-Jesús; Rubio, Julio;
    Ruiz-Reina, José-Luis
ti: Formalization of a normalization theorem in simplicial topology.
so: Ann. Math. Artif. Intell. 64, No. 1, 1-37 (2012).
py: 2012
pu: Springer, Dordrecht
la: EN
cc: 
ut: automated reasoning; formalization of mathematics; ACL2; algebraic
    topology; normalization theorem
ci: 
li: doi:10.1007/s10472-011-9274-6
ab: 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.
rv: