论文部分内容阅读
定理证明是重要的形式化验证方法之一,其将系统建模为逻辑公式,依托定理证明器进行推理从而完成验证.定理证明器中包含的定理库越多,其建模和推理能力越强.控制理论中经常用函数向量描述状态空间,形式化函数矩阵理论对控制系统的形式化分析有重要意义.本文在高阶逻辑定理证明器Higher-Order Logic 4中形式化函数向量和函数矩阵,包括形式化定义数据类型、运算及形式化验证运算性.本文同时给出了函数矩阵求导的形式化定义,证明了矩阵微分法中函数矩阵(或函数向量)相对于数量变量的微分法的常用定理,并给出了对二次型函数求导的形式化证明.本文工作已整理成定理库.
Theorem proving is one of the important formalized verification methods, which models the system as a logical formula and relies on the theorem prover to complete the verification. The more theorem libraries are contained in the theorem prover, the stronger its modeling and reasoning ability In the control theory, the state space is usually described by the function vector, and the formalized function matrix theory is of great significance to the formal analysis of the control system.In this paper, the formalized function vectors and function matrices in Higher Order Logic Proof Proof 4, Including the formal definition of data types, operations and formal verification of computability.In this paper, we also give the formal definition of function matrix derivation, and prove that the differential matrix of function matrix (or function vector) relative to the number of variables in matrix differential method Commonly used theorems and formal proofs of the derivation of quadratic functions are given.