A mechanized proof of the basic perturbation lemma

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

zbMATH Keywords

IsabelleBasic perturbation lemmaHomological algebra

Mathematics Subject Classification ID

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

• Coq
• Isabelle
• Isabelle/Isar
• Isar
• Kenzo

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