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.

翻译：本文讨论“图表追逐”证明的形式化——这是在阿贝尔范畴中证明性质的标准技巧。我们探讨如何通过一个简单的多类一阶理论捕捉图表追逐的本质，并研究该理论的模型与可判定性。本工作的长期动机在于，为同调代数中基于交互式定理证明器编写可靠证明的计算机辅助工具设计奠定基础。