A method for mechanically diagram chasing

MaRDI QIDQ5017594zbMATH OpenFDO

Authors Zheng Xie, Zheng Ye, Lei Huang, Hongbo Li

Publication date 17 December 2021

zbMATH Keywords

automated theorem provingcommutative diagramdiagram chasingforward chaininghomological algebra

Mathematics Subject Classification ID

Software, source code, etc. for problems pertaining to commutative algebra (13-04) (Co)homology of commutative rings and algebras (e.g., Hochschild, André-Quillen, cyclic, dihedral, etc.) (13D03) Computational homological algebra (13P20)

Recommendations

• Diagram chasing in Mal'cev categories
• Duality for diagram chasing a la Mac Lane in non-abelian categories
• A mechanized proof of the basic perturbation lemma
• On free abelian categories for theorem proving
• A categorical reduction system for linear logic

Cited in

(1)

• On free abelian categories for theorem proving

This page was built for publication: A method for mechanically diagram chasing

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5017594)