A mechanized proof of the basic perturbation lemma
From MaRDI portal
Publication:928666
DOI10.1007/s10817-007-9094-xzbMath1140.68059OpenAlexW2027737519WikidataQ57721926 ScholiaQ57721926MaRDI QIDQ928666
Clemens Ballarin, Jesús Aransay, Julio Jesús Rubio García
Publication date: 11 June 2008
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-007-9094-x
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (14)
Homotopy groups of suspended classifying spaces: An experimental approach ⋮ Formalization of a normalization theorem in simplicial topology ⋮ A Certified Reduction Strategy for Homological Image Processing ⋮ Effective homology of bicomplexes, formalized in Coq ⋮ Exploring the structure of an algebra text with locales ⋮ From types to sets by local type definition in higher-order logic ⋮ Proving with ACL2 the Correctness of Simplicial Sets in the Kenzo System ⋮ Generating certified code from formal proofs: a case study in homological algebra ⋮ A case-study in algebraic manipulation using mechanized reasoning tools ⋮ Incidence Simplicial Matrices Formalized in Coq/SSReflect ⋮ ACL2 Verification of Simplicial Degeneracy Programs in the Kenzo System ⋮ From Types to Sets by Local Type Definitions in Higher-Order Logic ⋮ Formalizing in Coq Hidden Algebras to Specify Symbolic Computation Systems ⋮ Modelling algebraic structures and morphisms in ACL2
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Constructivism in mathematics. An introduction. Volume I
- Isabelle/HOL. A proof assistant for higher-order logic
- Constructive algebraic topology
- The foundation of a generic theorem prover
- A formal proof of Sylow's theorem. An experiment in abstract algebra with Isabelle H0L
- On the chain-complex of a fibration
- A logical approach to abstract algebra
- A Fixed Point Approach to Homological Perturbation Theory
- A formally verified proof of the prime number theorem
- Towards Constructive Homological Algebra in Type Theory
- On constructive mathematics
- Interpretation of Locales in Isabelle: Theories and Proof Contexts
This page was built for publication: A mechanized proof of the basic perturbation lemma