On the formalization of the heat conduction problem in HOL

DOI10.1007/978-3-031-16681-5_2arXiv2208.06642OpenAlexW4296050254MaRDI QIDQ6159364FDOQ6159364

Elif Deniz, Sofiène Tahar, Osman Hasan, Adnan Rashid

Publication date: 2 June 2023

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Abstract: Partial Differential Equations (PDEs) are widely used for modeling the physical phenomena and analyzing the dynamical behavior of many engineering and physical systems. The heat equation is one of the most well-known PDEs that captures the temperature distribution and diffusion of heat within a body. Due to the wider utility of these equations in various safety-critical applications, such as thermal protection systems, a formal analysis of the heat transfer is of utmost importance. In this paper, we propose to use higher-order-logic (HOL) theorem proving for formally analyzing the heat conduction problem in rectangular coordinates. In particular, we formally model the heat transfer as a one-dimensional heat equation for a rectangular slab using the multivariable calculus theories of the HOL Light theorem prover. This requires the formalization of the heat operator and formal verification of its various properties, such as linearity and scaling. Moreover, we use the separation of variables method for formally verifying the solution of the PDEs, which allows modeling the heat transfer in the slab under various initial and boundary conditions using HOL Light.

Full work available at URL: https://arxiv.org/abs/2208.06642

zbMATH Keywords

heat equationpartial differential equationsseparation of variablestheorem provinghigher-order logicHOL Light

Mathematics Subject Classification ID

Computer science support for mathematical research and practice (68Vxx)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Transient heat conduction in one-dimensional composite slab. A ``natural analytic approach
• Differential equations and their applications. An introduction to applied mathematics. 3rd ed
• Formal Proof of a Wave Equation Resolution Scheme: The Method Error
• Heat Conduction
• Numerical Analysis of Ordinary Differential Equations in Isabelle/HOL
• The flow of ODEs: formalization of variational equation and Poincaré map
• Formalization of transform methods using HOL Light
• On the Formalization of Fourier Transform in Higher-order Logic
• Formalization of Euler-Lagrange equation set based on variational calculus in HOL light
• Trusting computations: a mechanized proof from partial differential equations to actual program
• A simple example for linear partial differential equations and its solution using the method of separation of variables

This page was built for publication: On the formalization of the heat conduction problem in HOL

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