函数矩阵理论在HOL4中的形式化

Formalization of Function Matrix Theory in HOL4

定理证明是重要的形式化验证方法之一,其将系统建模为逻辑公式,依托定理证明器进行推理从而完成验证.定理证明器中包含的定理库越多,其建模和推理能力越强.控制理论中经常用函数向量描述状态空间,形式化函数矩阵理论对控制系统的形式化分析有重要意义.本文在高阶逻辑定理证明器Higher-Order Logic 4中形式化函数向量和函数矩阵,包括形式化定义数据类型、运算及形式化验证运算性.本文同时给出了函数矩阵求导的形式化定义,证明了矩阵微分法中函数矩阵(或函数向量)相对于数量变量的微分法的常用定理,并给出了对二次型函数求导的形式化证明.本文工作已整理成定理库.

Theorem proving is one of the most important methods of formal verification,it model the system for logic formula,reasoning and complete verification relying on theorem prover.The more the theorem prover contains theorem library,the stronger its reasoning ability.Function matrices are widely used in the control theory to describe state space.Formalizing the function matrix theory is significant for the formal analysis of control systems.Based on the higher order logical theorem prover Higher-Order Logic 4,this paper formalizes the function vector and function matrix theory,including data types,operations and their properties.The paper also presents the formal definition of the function matrix derivative,proves the commonly used theorems of the function matrix(or function vector) differential on quantity variables and presents the formal proof of quadratic function derivative.The formalization is implemented as a library in the Higher-Order Logic 4 system.