An Isabelle/HOL formalisation of Green's theorem

DOI10.1007/s10817-018-9495-zzbMath1468.68313OpenAlexW2900255997MaRDI QIDQ2323451

Mohammad Abdulaziz, Lawrence Charles Paulson

Publication date: 2 September 2019

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://www.repository.cam.ac.uk/handle/1810/262376

zbMATH Keywords

mathematical physicsmathematical analysisformalised mathematicsmultivariate calculus

Mathematics Subject Classification ID

Integral formulas of real functions of several variables (Stokes, Gauss, Green, etc.) (26B20) Formalization of mathematics in connection with theorem provers (68V20)

Related Items (1)

Reliable reconstruction of fine-grained proofs in a proof assistant

Uses Software

• Isabelle
• Isabelle/HOL
• HOL

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Isabelle/HOL. A proof assistant for higher-order logic
• Geometric measure theory.
• The HOL Light theory of Euclidean space
• An Isabelle/HOL Formalisation of Green’s Theorem
• Three Chapters of Measure Theory in Isabelle/HOL
• The General Form of Green's Theorem
• Type Classes and Filters for Mathematical Analysis in Isabelle/HOL
• An Approximation To a Rectifiable Plane Curve
• Mathematical analysis II. Transl. from the 4th Russian edition by Roger Cooke

This page was built for publication: An Isabelle/HOL formalisation of Green's theorem