图追踪的一阶理论
计算机科学中的逻辑
2023-11-29 v2
摘要
本文讨论了“图追踪”证明的形式化，这是一种在阿贝尔范畴中证明性质的常用技术。我们探讨了图追踪的本质如何由一个简单的多类一阶理论所刻画，并研究了该理论的模型与可判定性。这项工作的长期动机是基于交互式定理证明器，设计一种用于同调代数中书写可靠证明的计算机辅助工具。
引用
@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}
}