本书是分数阶系统与高阶逻辑形式化验证的基础理论研究著作。分数阶系统是建立在分数阶微积分方程理论上实际系统的数学模型。分数阶微积分方程是扩展传统微积分学的一种直接方式，即允许微积分方程中对函数的阶次选择分数，而不仅是现有的整数。分数阶微积分不仅为系统科学提供了一个新的数学工具，它的广泛应用也表明了实际系统动态过程本质上是分数阶的。高阶逻辑形式化验证是形式化验证方法的一种，它是一种人机交互的定理证明方法。本书以分数阶微积分和高阶逻辑形式化验证为切入点，系统性研究了分数阶系统的求解、近似化、控制器设计与高阶逻辑形式化分析验证等内容。
本书填补了分数阶系统的高阶逻辑形式化验证研究著作方面的空白，可供数学、控制科学、形式化验证等相关学科的学生、科技工作者和教师参考。

第1章 分数阶系统概述
1.1 分数阶系统简介
1.2 分数阶系统求解
1.3 分数阶系统近似化
1.4 成比例分数阶系统
1.5 分数阶PID控制器
参考文献
第2章 相关理论基础
2.1 基本函数
2.2 分数阶微积分定义
2.2.1 Grunwald-Letnikov分数阶微积分定义
2.2.2 Riemann-Liouville分数阶微积分定义
2.2.3 Caputo分数阶微积分定义
2.2.4 分数阶微积分定义间的关系
2.2.5 分数阶微积分的性质
2.3 分数阶微积分的基本变换
2.3.1 Laplace变换
2.3.2 Fourier变换
2.4 分数阶微积分方程的解
2.4.1 分数阶微积分方程
2.4.2 解的存在与唯一性
第3章 分数阶系统求解
3.1 分数阶线性微积分方程求解
3.1.1 求解算法
3.1.2 步长的影响
3.2 分数阶微积分框图求解法
3.2.1 分数阶微积分模块
3.2.2 框图法求解分数阶线性微积分方程
3.2.3 框图法求解分数阶非线性微积分方程
参考文献
第4章 分数阶微积分算子近似
4.1 直接近似化方法
4.2 间接近似化方法
4.3 改进近似法
4.3.1 系数的选取
4.3.2 Taylor级数的剪切
4.4 分数阶系统最优降阶
4.5 仿真实例
参考文献
第5章 成比例分数阶系统
5.1 成比例分数阶系统表示方法
5.2 状态空间与传递函数的关系
5.3 成比例分数阶系统的稳定性
5.4 成比例分数阶系统的能控性与能观性
5.4.1 能控性
5.4.2 能观性
5.5 成比例分数阶系统的响应分析
5.6 理想传递函数
5.7 成比例分数阶系统实例分析
5.8 成比例分数阶系统的H2范数
5.9 控制器设计与仿真
参考文献
第6章 分数阶PID控制器设计
6.1 分数阶PID控制器
6.2 简单分数阶系统的分数阶PID控制器设计与仿真
6.2.1 控制器设计
6.2.2 仿真实例
6.3 分数阶系统的分数阶PID控制器设计与仿真
6.3.1 控制器设计
6.3.2 仿真实例
参考文献
第7章 分数阶PID控制器对比研究
7.1 位置伺服系统
7.2 分数阶PID控制器与模型预测控制的比较
7.3 分数阶PID控制器与整数阶PID控制器的对比研究
7.3.1 控制器设计
7.3.2 分数阶PID控制器对于负载变化的鲁棒性
7.3.3 近似中N的选取
7.4 分数阶PI控制器与整数阶PI控制器的对比研究
7.4.1 控制器设计
7.4.2 分数阶PI控制器对于负载变化的鲁棒性
7.5 分数阶控制器对于弹性参数的鲁棒性
7.5.1 分数阶PID控制器的鲁棒性
7.5.2 分数阶PI控制器的鲁棒性
7.6 分数阶控制器对于机械非线性的鲁棒性
参考文献
第8章 智能PID温度控制算法研究
8.1 PID参数模糊自整定温度测控仪
8.1.1 模糊PID控制器的设计
8.1.2 硬件部分
8.1.3 软件部分
8.2 基于遗传算法的连续重整装置智能PID温度控制系统
8.2.1 系统组成
8.2.2 遗传算法的基本操作
8.2.3 基于遗传算法的PID参数寻优的过程
8.2.4 连续重整装置反应器温度控制系统PID参数的寻优设计
8.2.5 控制效果分析
8.3 连续重整装置模糊自适应PID温度控制系统
8.3.1 PID型模糊控制器结构
8.3.2 参数自适应方法
8.3.3 隶属度函数的调整和可调因子的自整定
8.3.4 控制效果分析
参考文献
第9章 风暴灾害中的分数阶模型
9.1 人员伤亡损失评估
9.2 直接经济损失评估
9.3 间接经济损失评估
9.4 举例分析
参考文献
第10章 教育评估的分数阶模型
10.1 教育评估简介
10.2 分数阶评估方法
10.2.1 课程评估指标体系
10.2.2 确定指标权重
10.2.3 基于关联距离度的评估模型
10.3 实例分析
参考文献
第11章 分数阶序列最小优化方法
11.1 支持向量机
11.1.1 线性可分支持向量机
11.1.2 线性不可分支持向量机
11.1.3 非线性支持向量机与核函数
11.2 序列最小优化算法
11.3 序列最小优化算法的分数阶拓展
11.4 实例验证
第12章 LIBSVM工具箱中分数阶C-支持向量分类方法
12.1 泰勒展开式推导
12.1.1 一元泰勒展开式
12.1.2 多元泰勒展开式
12.1.3 分数阶泰勒展开式
12.2 目标函数的分数阶改进
12.3 拉格朗日乘子的更新
12.3.1 选取拉格朗日乘子α的下标i
12.3.2 选取拉格朗日乘子α的下标j
12.3.3 对拉格朗日乘子的更新
12.4 分数阶导数集合的更新
12.5 法向量w和偏移量b的计算
12.6 确定分类结果
12.7 实例验证
第13章 高阶逻辑定理证明器
13.1 形式化验证
13.1.1 等价性验证
13.1.2 模型检验
13.1.3 定理证明
13.2 HOL系统概述
13.2.1 HOL系统的发展
13.2.2 ML语言
13.2.3 HOL类型
13.2.4 定理库
13.2.5 对策和策略