Ponente: Mohammad Abdulaziz (Technische Universität München)
Lugar: Seminario Mirian Andrés (Edificio CCT)
Hora: viernes 17 de noviembre, 11:00
Resumen: We describe a formalisation of Green’s theorem, a fundamental result of multivariate calculus, in Isabelle/HOL. The theorem statement that we formalise is enough for most applications, especially in physics and engineering. An interesting aspect of our proof is that we neither formalise orientations nor region boundaries explicitly, with respect to the outwards-pointing normal vector. Instead we refer to homological equivalences between paths.
The slides of the talk can be found in the following link.