TY - GEN
T1 - An Isabelle/HOL formalisation of Green’s theorem
AU - Abdulaziz, Mohammad
AU - Paulson, Lawrence C.
N1 - Publisher Copyright:
© Springer International Publishing Switzerland 2016.
PY - 2016
Y1 - 2016
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84984819459&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-43144-4_1
DO - 10.1007/978-3-319-43144-4_1
M3 - Conference contribution
SN - 9783319431437
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 3
EP - 19
BT - Interactive Theorem Proving - 7th International Conference, ITP 2016, Proceedings
A2 - Blanchette, Jasmin Christian
A2 - Merz, Stephan
PB - Springer Verlag
T2 - 7th International Conference on Interactive Theorem Proving, ITP 2016
Y2 - 22 August 2016 through 25 August 2016
ER -