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

Formal verification of Green's theorem and its applications

作　　者：刘永梅[1,2] 王国辉 关永[2] 张景芝 施智平 董璐[1] LIU Yong-mei;WANG Guo-hui;GUAN Yong;ZHANG Jing-zhi;SHI Zhi-ping;DONG Lu(Information Engineering College,Capital Normal University,Beijing 100048;International Science and Technology Cooperation Base of Electronic System Reliability and Mathematical Interdisciplinary,Capital Normal University,Beijing 100048,China)

机构地区：[1]首都师范大学信息工程学院,北京100048 [2]电子系统可靠性与数理交叉学科国际科技合作基地,北京100048

出　　处：《计算机工程与科学》2023年第7期1178-1187,共10页Computer Engineering & Science

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

摘　　要：格林定理广泛应用于物理学、流体力学和化学等领域。通常使用传统的计算机仿真和数值计算方法构建基于格林定理的系统模型。然而,由于工具软件可能存在的系统缺陷导致模型出现偏差,从而使任务失败。为解决上述问题,采用基于高阶逻辑的形式化方法,在定理证明器HOL Light中实现了格林定理相关内容的高阶逻辑建模与验证。首先,对梯度、散度等基本概念和性质进行了形式化描述;其次,对格林定理及其性质进行了形式化建模与验证;最后,基于格林定理的形式化模型完成了地下水控制模型的高阶逻辑推导,进而确保系统模型的安全性。Green's theorem is widely used in physics,hydrodynamics,chemistry and other fields.Traditional computer simulation and numerical calculation methods are usually used to build the system model based on Green's theorem.However,the possible system defects in the tool software lead to the deviation of the model,which makes the task fail.In order to solve the above problems,this paper adopts the formalization method based on higher-order logic to realize the higher-order logic modeling and verification of Green's theorem related content in the theorem prover HOL Light.Firstly,the basic concepts and properties of gradient and divergence are formally described.Secondly,formal modeling and verification of Green's theorem and its properties are carried out.Finally,the high-level logical derivation of groundwater control model is completed based on the formal model of Green's theorem,so as to ensure the safety of the system model.

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

分 类 号：TP393[自动化与计算机技术—计算机应用技术]