An Isabelle/HOL formalisation of Green's theorem

DOI10.1007/978-3-319-43144-4_1zbMATH Open1468.68312DBLPconf/itp/AbdulazizP16OpenAlexW2503421619WikidataQ57382542 ScholiaQ57382542MaRDI QIDQ2829238FDOQ2829238

Lawrence C. Paulson, Mohammad Abdulaziz

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

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

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)

Cites Work

• Title not available (Why is that?)
• Isabelle/HOL. A proof assistant for higher-order logic
• Type Classes and Filters for Mathematical Analysis in Isabelle/HOL
• Three Chapters of Measure Theory in Isabelle/HOL
• Title not available (Why is that?)
• The General Form of Green's Theorem
• Title not available (Why is that?)
• An Approximation To a Rectifiable Plane Curve

Cited In (4)

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

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)