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

Abstract: 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.

Key words: formal verification, theorem proving, Greens theorem, HOL Light