计算机工程与科学2025，Vol.47Issue(6)：1050-1061,12.DOI:10.3969/j.issn.1007-130X.2025.06.011
斯托克斯定理的形式化及其初步应用
Formal verification of Stokes' theorem and its applications
摘要
Abstract
Stokes' theorem is one of the fundamental theorems in field theory,with extensive appli-cations in fluid mechanics,electromagnetics,and other domains.However,in practical applications,the satisfaction of its prerequisite conditions is often not rigorously verified,which introduces certain risks.Therefore,it is necessary to validate Stokes' theorem.This paper constructs a formal model of Stokes' theorem based on its mathematical definition.By analyzing the mathematical proof process of the theorem,this paper derives the derivation methodology for its formal verification.Following the analysis,construction,and verification objectives,this paper ccompletes the formal proof of the theo-rem.Finally,the proven Stokes' theorem is applied to the validation of the pipeline flow design models.关键词
形式化验证/定理证明/斯托克斯定理/HOL LightKey words
formal verification/theorem proving/Stokes' theorem/HOL light分类
计算机与自动化引用本文复制引用
刘永梅,王国辉,关永,张景芝,施智平,董璐..斯托克斯定理的形式化及其初步应用[J].计算机工程与科学,2025,47(6):1050-1061,12.基金项目
国家重点研发计划(2019YFB1309900) （2019YFB1309900）
国家自然科学基金(62002246,62272322,62272323) （62002246,62272322,62272323）
科技创新服务能力建设-基本科研业务费(科研费)项目(00621530290000) （科研费）
