Formalization of a normalization theorem in simplicial topology
type: Item
instance of: scholarly article
title: Formalization of a normalization theorem in simplicial topology
zbMATH Open document ID: 1280.68232
author: Laureano Lambán
author: Francisco Jesús Martín-Mateos
author: Julio Rubio
author: José Luis Ruiz-Reina
published in: Annals of Mathematics and Artificial Intelligence
publication date: 2012-12-28T00:00:00Z
full work available at URL: https://idus.us.es/handle//11441/86280
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 68W30
Mathematics Subject Classification ID: 55U10
zbMATH DE Number: 6119067
zbMATH Keywords: automated reasoning
zbMATH Keywords: formalization of mathematics
zbMATH Keywords: ACL2
zbMATH Keywords: algebraic topology
zbMATH Keywords: normalization theorem
describes a project that uses: ACL2
describes a project that uses: EAT
describes a project that uses: Kenzo
MaRDI profile type: Publication
OpenAlex ID: W2034552599
cites work: A mechanized proof of the basic perturbation lemma
cites work: Generating certified code from formal proofs: a case study in homological algebra
cites work: Towards Constructive Homological Algebra in Type Theory
cites work: Triangulations. Structures for algorithms and applications
cites work: Object oriented institutions to specify symbolic computation systems
cites work: Computing in Coq with Infinite Algebraic Data Structures
cites work: Semisimplicial objects and the Eilenberg-Zilber Theorem
cites work: Proving with ACL2 the Correctness of Simplicial Sets in the Kenzo System
cites work: An object-oriented interpretation of the EAT system
cites work: Applying ACL2 to the Formalization of Algebraic Topology: Simplicial Polynomials
cites work: Q5639839
cites work: Sheaves in geometry and logic: a first introduction to topos theory
cites work: ACL2 Verification of Simplicial Degeneracy Programs in the Kenzo System
cites work: Q5550390
cites work: A verified common lisp implementation of Buchberger's algorithm in ACL2
cites work: Homological perturbation theory and associativity
cites work: Q3975344
cites work: Constructive algebraic topology
DOI: 10.1007/S10472-011-9274-6
Recommended article: Normalisation for the fundamental crossed complex of a simplicial set
Recommended article: Q5845950
Recommended article: Q5074875
Recommended article: Q5449997
Recommended article: A uniform approach to normality for topological spaces
Recommended article: A generalized approach towards normality for topological spaces
Recommended article: Q3062059
Recommended article: Formal aspects of topological complexity
Recommended article: Simplicial normalization in the entire cyclic cohomology of Banach algebras
Recommended article: Normal and conormal maps in homotopy theory
description: scientific article; zbMATH DE number 6119067