An Isabelle/HOL formalisation of Green's theorem

DOI10.1007/978-3-319-43144-4_1MaRDI QIDQ2829238zbMATHOpenAlexDBLPWikidataFDO

Authors Mohammad Abdulaziz, Lawrence C. Paulson

Publication date 27 October 2016

Published in Interactive Theorem Proving (Search for Journal in Brave)

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

Mathematics Subject Classification ID

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

Recommendations

• An Isabelle/HOL formalisation of Green's theorem
• Green's theorem from the viewpoint of applications.
• A formal proof of Cauchy's residue theorem
• On Green's theorem and Cauchy's theorem
• The General Form of Green's Theorem

Cites work

• scientific article; zbMATH DE number 1232914 (Why is no real title available?)
• scientific article; zbMATH DE number 3280855 (Why is no real title available?)
• scientific article; zbMATH DE number 3321872 (Why is no real title available?)
• An Approximation To a Rectifiable Plane Curve
• Isabelle/HOL. A proof assistant for higher-order logic
• The General Form of Green's Theorem
• Three chapters of measure theory in Isabelle/HOL
• Type classes and filters for mathematical analysis in Isabelle/HOL

Cited in

(5)

• A Coq formalization of Lebesgue integration of nonnegative functions
• Reliable reconstruction of fine-grained proofs in a proof assistant
• A formal proof of Cauchy's residue theorem
• Formalising Knot Theory in Isabelle/HOL
• An Isabelle/HOL formalisation of Green's theorem

Describes a project that uses

Uses Software

• Isabelle
• Isabelle/HOL
• HOL

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 Q2829238)