Applying ACL2 to the Formalization of Algebraic Topology: Simplicial Polynomials

DOI10.1007/978-3-642-22863-6_16zbMath1342.68292OpenAlexW55003788MaRDI QIDQ3088007

Francisco Jesús Martín-Mateos, Laureano Lambán, José Luis Ruiz-Reina, Julio Jesús Rubio García

Publication date: 17 August 2011

Published in: Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-22863-6_16

Mathematics Subject Classification ID

Simplicial sets and complexes in algebraic topology (55U10) Chain complexes in algebraic topology (55U15)

Related Items (1)

Formalization of a normalization theorem in simplicial topology

Uses Software

• ACL2
• Kenzo

Cites Work

• Unnamed Item
• Unnamed Item
• Triangulations. Structures for algorithms and applications
• A verified common lisp implementation of Buchberger's algorithm in ACL2
• Constructive algebraic topology
• Proving with ACL2 the Correctness of Simplicial Sets in the Kenzo System
• ACL2 Verification of Simplicial Degeneracy Programs in the Kenzo System

This page was built for publication: Applying ACL2 to the Formalization of Algebraic Topology: Simplicial Polynomials