An Isabelle/HOL formalisation of Green’s theorem
Accepted version
Peer-reviewed
Repository URI
Repository DOI
Change log
Authors
Abdulaziz, M
Paulson, LC
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, especially in physics and engineering. An interesting aspect of our formalisation is that we neither formalise orientations nor region boundaries explicitly, with respect to the outwards-pointing normal vector. Instead we refer to equivalences between paths.
Description
Keywords
46 Information and Computing Sciences
Journal Title
Lecture Notes in Computer Science
Conference Name
Journal ISSN
0302-9743
1611-3349
1611-3349
Volume Title
9807
Publisher
Springer