Document Open Access Logo

A First Order Theory of Diagram Chasing

Authors Assia Mahboubi , Matthieu Piquerez

PDF
Thumbnail PDF

File

LIPIcs.CSL.2024.38.pdf
  • Filesize: 0.77 MB
  • 19 pages

Document Identifiers

Author Details

Assia Mahboubi
  • Nantes Université, École Centrale Nantes, CNRS, INRIA, LS2N, UMR 6004, France
  • Vrije Universiteit Amsterdam, The Netherlands
Matthieu Piquerez
  • Nantes Université, École Centrale Nantes, CNRS, INRIA, LS2N, UMR 6004, France

Funding

This work has received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (grant agreement No. 101001995).

Acknowledgements

The authors would like to thank Kenji Maillard, Loïc Pujet and the anonymous reviewers for their useful comments and suggestions on this work.

Cite As Get BibTex

Assia Mahboubi and Matthieu Piquerez. A First Order Theory of Diagram Chasing. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 38:1-38:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024) https://doi.org/10.4230/LIPIcs.CSL.2024.38

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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • Diagram chasing
  • formal proofs
  • abelian categories
  • decidability

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

Supplementary Materials

References

  1. URL: http://matthieu.piquerez.fr/partage/FANL_duality.v.
  2. Sergei Ivanovich Adyan. Algorithmic undecidability of problems of recognition of certain properties of groups. Dokl. Akad. Nauk SSSR, 103:533-535, 1955. Google Scholar
  3. Krzysztof Bar, Aleks Kissinger, and Jamie Vicary. Globular: an online proof assistant for higher-dimensional rewriting. Log. Methods Comput. Sci., 14(1), 2018. URL: https://doi.org/10.23638/LMCS-14(1:8)2018.
  4. Luc Chabassier and Bruno Barras. A graphical interface for diagrammatic proofs in proof assistants. Contributed talks in the 29th International Conference on Types for Proofs and Programs (TYPES 2023), 2023. URL: https://types2023.webs.upv.es/TYPES2023.pdf.
  5. Leonardo Mendonça de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. The lean theorem prover (system description). In Amy P. Felty and Aart Middeldorp, editors, Automated Deduction - CADE-25 - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings, volume 9195 of Lecture Notes in Computer Science, pages 378-388. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-21401-6_26.
  6. Eric Finster and Samuel Mimram. A type-theoretical definition of weak ω-categories. In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017, pages 1-12. IEEE Computer Society, 2017. URL: https://doi.org/10.1109/LICS.2017.8005124.
  7. Peter Freyd. Abelian categories. An introduction to the theory of functors. Harper’s Series in Modern Mathematics. Harper & Row Publishers, New York, 1964. Google Scholar
  8. Markus Himmel. Diagram chasing in interactive theorem proving. Bachelorarbeit. Karlsruher Institut für Technologie, 2020. URL: https://pp.ipd.kit.edu/uploads/publikationen/himmel20bachelorarbeit.pdf.
  9. Wilfrid Hodges. A shorter model theory. Cambridge: Cambridge University Press, 1997. Google Scholar
  10. Ambroise Lafont. A categorical diagram editor to help formalising commutation proofs. URL: https://amblafont.github.io/graph-editor/index.html.
  11. F. William Lawvere and Stephen H. Schanuel. Conceptual mathematics. A first introduction to categories. Cambridge: Cambridge University Press, 2nd ed. edition, 2009. Google Scholar
  12. Saunders Mac Lane. Homology. Class. Math. Berlin: Springer-Verlag, reprint of the 3rd corr. print. 1975 edition, 1995. Google Scholar
  13. Saunders Mac Lane. Categories for the working mathematician, volume 5 of Grad. Texts Math. New York, NY: Springer, 2nd ed edition, 1998. Google Scholar
  14. J. Peter May. A concise course in algebraic topology. Chicago, IL: University of Chicago Press, 1999. Google Scholar
  15. Yannis Monbru. Towards automatic diagram chasing. M1 report. École Normale Supérieure Paris-Saclay, 2022. URL: https://github.com/ymonbru/Diagram-chasing/blob/main/MONBRU_Yannis_Rapport.pdf.
  16. Matthieu Piquerez. Tropical Hodge theory and applications. PhD thesis, Institut Polytechnique de Paris, November 2021. URL: https://theses.hal.science/tel-03499730#.
  17. Michael O. Rabin. Recursive unsolvability of group theoretic problems. Ann. Math. (2), 67:172-194, 1958. URL: https://doi.org/10.2307/1969933.
  18. Emily Riehl. Category Theory in Context. Dover Publications, 2017. URL: https://math.jhu.edu/~eriehl/context.pdf.
  19. Peter Selinger. A survey of graphical languages for monoidal categories. In Bob Coecke, editor, New Structures for Physics, volume 813 of Lecture Notes in Physics, pages 289-355. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-12821-9_4.
  20. Alfred Tarski. The semantic conception of truth and the foundations of semantics. Philos. Phenomenol. Res. 4, 341-376 (1944)., 1944. Google Scholar
  21. The Coq Development Team. The coq proof assistant, June 2023. URL: https://doi.org/10.5281/zenodo.8161141.
  22. Cédric Ho Thanh, Pierre-Louis Curien, and Samuel Mimram. A sequent calculus for opetopes. In 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019, Vancouver, BC, Canada, June 24-27, 2019, pages 1-12. IEEE, 2019. URL: https://doi.org/10.1109/LICS.2019.8785667.
  23. Vladimir Voevodsky. Univalent semantics of constructive type theories. In Jean-Pierre Jouannaud and Zhong Shao, editors, Certified Programs and Proofs - First International Conference, CPP 2011, Kenting, Taiwan, December 7-9, 2011. Proceedings, volume 7086 of Lecture Notes in Computer Science, page 70. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-25379-9_7.
  24. Douglas B. West. Introduction to graph theory. New Delhi: Prentice-Hall of India, 2nd ed. edition, 2005. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact