摘要
定理证明是重要的形式化验证方法之一,其将系统建模为逻辑公式,依托定理证明器进行推理从而完成验证.定理证明器中包含的定理库越多,其建模和推理能力越强.控制理论中经常用函数向量描述状态空间,形式化函数矩阵理论对控制系统的形式化分析有重要意义.本文在高阶逻辑定理证明器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.
出处
《小型微型计算机系统》
CSCD
北大核心
2013年第3期654-658,共5页
Journal of Chinese Computer Systems
基金
国际科技合作计划项目(2010DFB10930
2011DFG13000)资助
国家自然科学基金项目(60873006
61070049
61170304
61104035)资助
北京市自然科学基金暨北京市教委重点项目(4122017
KZ201210028036)资助
北京市优秀人才培养资助项目
计算机体系结构国家重点实验室开放课题
