A First Order Theory of Diagram Chasing
Logic in Computer Science
2023-11-29 v2
Abstract
This paper discusses the formalization of proofs "by diagram chasing", a standard technique for proving properties in abelian categories. We discuss how the essence of diagram chases can be captured by a simple many-sorted first-order theory, and we study the models and decidability of this theory. The longer-term motivation of this work is the design of a computer-aided instrument for writing reliable proofs in homological algebra, based on interactive theorem provers.
Keywords
Cite
@article{arxiv.2311.01790,
title = {A First Order Theory of Diagram Chasing},
author = {Assia Mahboubi and Matthieu Piquerez},
journal= {arXiv preprint arXiv:2311.01790},
year = {2023}
}