HOL中热传导问题的形式化
计算机科学中的逻辑
2022-08-16 v1
摘要
偏微分方程（PDEs）被广泛用于建模物理现象并分析许多工程与物理系统的动态行为。热方程是其中最著名的PDE之一，刻画了物体内部的温度分布与热扩散。由于这些方程在各种安全关键应用（如热防护系统）中的广泛用途，对热传递的形式化分析至关重要。在本文中，我们提出使用高阶逻辑（HOL）定理证明来形式化分析直角坐标系中的热传导问题。特别地，我们利用HOL Light定理证明器的多变量微积分理论，将热传递形式化为矩形板的一维热方程。这需要形式化热算子并形式化验证其线性与缩放等各种性质。此外，我们使用分离变量法形式化验证该PDE的解，从而能够在HOL Light中针对各种初始与边界条件对板内热传递进行建模。
引用
@article{arxiv.2208.06642,
title = {On the Formalization of the Heat Conduction Problem in HOL},
author = {Elif Deniz and Adnan Rashid and Osman Hasan and Sofiène Tahar},
journal= {arXiv preprint arXiv:2208.06642},
year = {2022}
}
备注
15th Conference on Intelligent Computer Mathematics