本书系统深入地阐述了矩阵结构和矩阵函数的公理化体系，并给出基于此公理体系进行形式化分析与验证的应用。主要内容包括：矩阵结构的形式化；矩阵序列与矩阵级数理论的形式化；矩阵函数微分的形式化；矩阵理论的自动化定理证明；矩阵理论公理化系统在信息或物理系统形式化建模验证中的应用。
本书可作为机器定理证明、形式化方法、理论计算机科学及软件工程等领域的科研人员及工程技术人员的参考书，也可供高等院校相关专业高年级本科生和研究生阅读。

符号说明
序
前言
第1章 绪论
1.1 背景及意义
1.2 研究现状
1.2.1 矩阵分析
1.2.2 数学形式化的发展现状
1.3 定理证明系统HOL Light
1.3.1 HOL Light简介
1.3.2 系统相关符号的约定
1.4 主要内容
1.5 本书结构
参考文献
第2章 矩阵结构的形式化
2.1 抽象空间
2.1.1 线性空间
2.1.2 拓扑空间
2.1.3 距离空间与赋范空间
2.1.4 内积空间与希尔伯特空间
2.2 矩阵结构
2.3 矩阵结构的基本数据类型
2.4 矩阵结构基本性质的形式化
2.4.1 线性性质
2.4.2 拓扑性质
2.4.3 范数性质
2.4.4 内积性质
2.5 矩阵结构的完备性
2.5.1 空间完备性的形式化
2.5.2 巴拿赫空间与希尔伯特空间
2.6 本章小结
参考文献
第3章 矩阵序列与矩阵级数理论的形式化
3.1 矩阵序列与矩阵级数的形式化
3.1.1 矩阵序列
3.1.2 矩阵级数
3.1.3 矩阵幂级数
3.2 柯西审敛准则在矩阵序列的推广
3.2.1 柯西审敛准则
3.2.2 比较审敛法和比值审敛法
3.3 矩阵函数的形式化
3.3.1 一般矩阵函数的形式化定义
3.3.2 常用的由矩阵幂级数表示的矩阵函数
3.4 矩阵结构紧致性的形式化分析
3.4.1 紧致性相关概念的形式化
3.4.2 紧致性的等价性证明
3.5 本章小结
参考文献
第4章 矩阵函数微分的形式化
4.1 矩阵函数连续性
4.1.1 矩阵函数连续性的形式化定义
4.1.2 矩阵函数连续性的形式化
4.2 矩阵函数的Fréchet微分
4.2.1 Fréchet微分定义的形式化
4.2.2 矩阵函数微分基本性质的形式化
4.3 矩阵函数微分与有界线性算子
4.4 本章小结
参考文献
第5章 矩阵理论的自动定理证明
5.1 引言
5.2 判定程序基本理论及矩阵结构理论判定性研究
5.2.1 判定程序基本理论
5.2.2 矩阵结构理论判定性的初步研究
5.3 自动证明算法的设计与实现
5.3.1 算法的基本流程
5.3.2 算法的程序实现
5.3.3 判定程序的有效性测试
5.4 本章小结
参考文献
第6章 应用示例
6.1 一种面向Massive MIMO的矩阵求逆算法形式化分析
6.1.1 引言
6.1.2 系统模型的形式化
6.1.3 算法模型的形式化
6.1.4 级数收敛性的形式化分析
6.2 机器人机构运动学中的李群李代数模型的形式化验证
6.2.1 引言
6.2.2 机构运动学中常用李群李代数的形式化
6.2.3 机构运动学中常用李群李代数及其指数映射的形式化验证
6.3 本章小结
参考文献