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.

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