An Isabelle/HOL Formalisation of Green’s Theorem
View / Open Files
Authors
Abdulaziz, Mohammad
Paulson, LC
Publication Date
2019Journal Title
Interactive Theorem Proving
Publisher
Springer
Volume
9807
Number
3
Pages
763-786
Type
Book chapter
This Version
AM
Metadata
Show full item recordCitation
Abdulaziz, M., & Paulson, L. (2019). An Isabelle/HOL Formalisation of Green’s Theorem. Springer, Interactive Theorem Proving. [Book chapter]. https://doi.org/10.1007/978-3-319-43144-4_1
Abstract
We mechanise a proof of Green’s theorem in Isabelle/HOL. We use a novel proof that avoids the ubiquitous line integral cancellation argument. This eliminates the need to formalise orientations and region boundaries explicitly with respect to the outwards-pointing normal vector. Instead we appeal to a homological argument about equivalences between paths. Contributions include mechanised theories of line integrals and partial derivatives, as well as the first mechanisation of Green’s theorem.
Sponsorship
European Research Council (742178)
Identifiers
External DOI: https://doi.org/10.1007/978-3-319-43144-4_1
This record's DOI: https://doi.org/10.17863/CAM.35379
Rights
Licence:
http://www.rioxx.net/licenses/all-rights-reserved
Statistics
Total file downloads (since January 2020). For more information on metrics see the
IRUS guide.
Recommended or similar items
The current recommendation prototype on the Apollo Repository will be turned off on 03 February 2023. Although the pilot has been fruitful for both parties, the service provider IKVA is focusing on horizon scanning products and so the recommender service can no longer be supported. We recognise the importance of recommender services in supporting research discovery and are evaluating offerings from other service providers. If you would like to offer feedback on this decision please contact us on: support@repository.cam.ac.uk