An Isabelle/HOL Formalisation of Green’s Theorem

DOI10.1007/978-3-319-43144-4_1zbMath1468.68312DBLPconf/itp/AbdulazizP16OpenAlexW2503421619WikidataQ57382542 ScholiaQ57382542MaRDI QIDQ2829238

Mohammad Abdulaziz, Lawrence Charles 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

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

Related Items (3)

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

Uses Software

• Isabelle
• Isabelle/HOL
• HOL

Cites Work

• Isabelle/HOL. A proof assistant for higher-order logic
• 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
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: An Isabelle/HOL Formalisation of Green’s Theorem