A First Order Theory of Diagram Chasing - INRIA - Institut National de Recherche en Informatique et en Automatique Access content directly
Conference Papers Year : 2024

A First Order Theory of Diagram Chasing

Une théorie du premier ordre pour la chasse au diagramme


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.
Fichier principal
Vignette du fichier
main.pdf (710.89 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

hal-04266479 , version 1 (02-11-2023)
hal-04266479 , version 2 (04-12-2023)





Assia Mahboubi, Matthieu Piquerez. A First Order Theory of Diagram Chasing. CSL 2024 - 32nd EACSL Annual Conference on Computer Science Logic, Feb 2024, Naples, Italy. pp.1-19. ⟨hal-04266479v2⟩
197 View
55 Download



Gmail Facebook X LinkedIn More