An Isabelle/HOL formalisation of Green's theorem

DOI10.1007/S10817-018-9495-ZMaRDI QIDQ2323451zbMATH OpenOpenAlexFDO

Authors Mohammad Abdulaziz, Lawrence C. 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

formalised mathematicsmathematical analysismathematical physicsmultivariate 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)

Recommendations

• An Isabelle/HOL formalisation of Green's theorem
• scientific article; zbMATH DE number 1670741
• Green's theorem from the viewpoint of applications.
• A formal proof of Cauchy's residue theorem
• On Green's theorem and Cauchy's theorem

Cites work

• A comprehensive introduction to differential geometry. Vol. 1-5
• An Approximation To a Rectifiable Plane Curve
• An Isabelle/HOL formalisation of Green's theorem
• Geometric measure theory.
• scientific article; zbMATH DE number 1232914 (Why is no real title available?)
• scientific article; zbMATH DE number 1462096 (Why is no real title available?)
• scientific article; zbMATH DE number 1477074 (Why is no real title available?)
• scientific article; zbMATH DE number 3294854 (Why is no real title available?)
• Isabelle/HOL. A proof assistant for higher-order logic
• Mathematical analysis II. Transl. from the 4th Russian edition by Roger Cooke
• The General Form of Green's Theorem
• The HOL Light theory of Euclidean space
• Three chapters of measure theory in Isabelle/HOL
• Type classes and filters for mathematical analysis in Isabelle/HOL

Cited in

(6)

• Reliable reconstruction of fine-grained proofs in a proof assistant
• Formalization of Dubé's degree bounds for Gröbner bases in Isabelle/HOL
• An Isabelle/HOL formalisation of Green's theorem
• A formal proof of Cauchy's residue theorem
• Formalising Knot Theory in Isabelle/HOL
• A formal correctness proof of Edmonds' blossom shrinking algorithm

Describes a project that uses

Uses Software

• Isabelle/HOL
• HOL
• Isabelle

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2323451)