基于高阶逻辑的分数阶建模与验证理论研究

本项目首次将分数阶微积分与形式化验证结合起来，在高阶逻辑定理证明中建立分数阶微积分理论体系。针对实际复杂系统，提出分数阶建模方法，构建和完善分数阶系统HOL推理平台，包括在形式化验证的高阶逻辑定理证明器中引入分数阶微积分基本定义，验证分数阶微积分的基本运算、性质、定律等内容，建立分数阶微积分理论体系，并用其检验分数阶模型的精确性。分数阶模型由于引入分数阶次可以更加准确的描述实际复杂系统，分数阶验证能够提高定理证明的完备性和准确性。本课题的研究成果将完善分数阶理论体系和高阶逻辑验证理论体系，为定理验证的广泛应用提供基础，对人工智能等相关领域的发展起到积极的推动作用。

随着人们对自然认识的逐步深入，发现了自然界的本质是分数阶的。分数阶模型可以更加准确的描述实际复杂系统。复杂系统的安全性、精准性、完备性受到更大关注。本项目首次将分数阶微积分与形式化验证结合起来。分数阶建模与验证能够准确描述复杂系统，并在高阶逻辑中证明系统正确性。提出了分数阶的认知过程模型，课程评估、教育评估的分数阶建模方法，城市交通流的分数阶模型，以及环境污染的分数阶模型。针对分数阶系统高可靠性分析理论的发展需要，完成了实数二项式系数及性质的高阶逻辑形式化建模与验证、Gauge积分及性质的高阶逻辑形式化建模与验证、分数阶微积分定义及性质的高阶逻辑形式化建模与验证，包括建立了分数阶微积分两种定义的高阶逻辑模型，三种常用定义间的相互转化，对分数阶微积分的零阶性、线性性质、分数阶微积分与整数阶微积分的一致性和叠加性进行了形式化验证。提出了拉普拉斯变换的高阶逻辑形式化建模与验证，将拉氏变换的卷积定理进行高阶逻辑建模及形式化验证分析。在实际系统中应用本项目建立的定理，策略等验证了实际系统，完成了分数阶电容的形式化分析与验证、分数阶微分电路的形式化分析与验证、直流电机的形式化验证、反向积分电路的形式化建模与验证、SpaceWire 译码电路的高阶逻辑形式化建模与验证、FC元件的形式化分析与验证、分数阶PID控制器的形式化分析与验证。研究成果完善了分数阶理论体系和高阶逻辑验证理论体系，为定理验证的广泛应用提供基础，对人工智能等相关领域的发展起到积极的推动作用。发表学术论文16篇，申请发明专利2项，软件著作权3项；获省部级奖项3次，培养研究生5名，晋升高级职称1人，在十余家国内外学术刊物担任审稿人。