格林定理的形式化及其初步应用

来源：计算机工程与科学杂志2023年第7期北京时间：

作者：刘永梅, 王国辉, 关永, 张景芝, 施智平, 董璐

单位：（1.首都师范大学信息工程学院，北京 100048；2.电子系统可靠性与数理交叉学科国际科技合作基地，北京 100048）

摘要：格林定理广泛应用于物理学、流体力学和化学等领域。通常使用传统的计算机仿真和数值计算方法构建基于格林定理的系统模型。然而，由于工具软件可能存在的系统缺陷导致模型出现偏差，从而使任务失败。为解决上述问题,采用基于高阶逻辑的形式化方法，在定理证明器HOL Light中实现了格林定理相关内容的高阶逻辑建模与验证。首先，对梯度、散度等基本概念和性质进行了形式化描述；其次，对格林定理及其性质进行了形式化建模与验证；最后，基于格林定理的形式化模型完成了地下水控制模型的高阶逻辑推导，进而确保系统模型的安全性。

关键词：形式化验证,定理证明,格林定理,HOL Light,

基金资助：国家重点研发计划（2019YFB1309900）;国家自然科学基金（62002246,62272322,62272323）;科技创新服务能力建设-基本科研业务费（科研费）项目（00621530290000）