Skip to main content

TS

An isabelle/HOL formalisation of green's theorem

Authors

Mohammad Abdulaziz and Lawrence Paulson

Data61
CSIRO

University of Cambridge

Abstract

We formalise a statement of Green’s theorem in Isabelle/HOL, which is its first formalisation to our knowledge. The theorem statement that we formalise is enough for most applications, specially in physics and engineering. An interesting aspect of our formalisation, is that we do not formalise orientations nor region boundaries explicitly, with respect to the outwards-pointing normal vector. Instead we refer to equivalences between paths.

BibTeX Entry

  @inproceedings{Abdulaziz_Paulson_16,
    author           = {Abdulaziz, Mohammad and Paulson, Lawrence},
    month            = aug,
    year             = {2016},
    keywords         = {formalised mathematics, mathematical analysis},
    title            = {An Isabelle/{HOL} Formalisation of Green's Theorem},
    booktitle        = {International Conference on Interactive Theorem Proving},
    address          = {Nancy, France}
  }

Download

Served by Apache on Linux on seL4.