A Topological Application of Labelled Natural Deduction

2019/06/19 by Veras, Tiago M. L., Ramos, Arthur F., de Queiroz, Ruy J. G. B. +1 · 2 citations
#Algebraic Topology (math.AT) #FOS: Computer and information sciences #FOS: Mathematics #Logic in Computer Science (cs.LO)

paper · doi:10.48550/arxiv.1906.09105

Abstract

We use a labelled deduction system based on the concept of computational paths (sequences of rewrites) as equalities between two terms of the same type. We also define a term rewriting system that is used to make computations between these computational paths, establishing equalities between equalities. We then proceed to show the main result here: using this system to obtain the calculation of the fundamental group of the circle, of the torus and the real projective plane.

Cited by

• The Seifert-van Kampen Theorem via Computational Paths: A Formalized Approach to Computing Fundamental Groups
• Formalizing Computational Paths and Fundamental Groups in Lean

Related

• An alternative approach to the calculation of fundamental groups based on labeled natural deduction
• Computational Paths -- An approach in the LND_EQ-TRS₂ system
• On the Calculation of Fundamental Groups in Homotopy Type Theory by\n Means of Computational Paths
• Formalizing Computational Paths and Fundamental Groups in Lean
• Deduction as Reduction