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

• 作者: 关永 刘振科 叶世伟 张杰 施智平 李晓娟 金声震
• 来源期刊: 小型微型计算机系统
• 学科: 工学
• 关键词: 函数矩阵 形式化验证 矩阵微分法 定理证明 Higher-Order Logic 4
• 年，卷（期）: 2013,（3）
• 所属期刊栏目: 计算机体系结构
• 页码范围: 654-658
• 页数: 5页
• 分类号: TN319
• 字数: 3956字
• 语种: 中文

摘要

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