实数二项式系数在HOL4中的形式化

定理证明是一种形式化方法,在高可靠性系统验证中起着越来越重要的作用。分数阶微积分是高可靠性系统分析的基础,实数二项式系数是分数阶微积分定义的重要组成部分。在高阶逻辑定理库中还没有实数二项式系数的形式化。提出实数二项式系数高阶逻辑形式化方法。首先研究阶乘幂在HOL4中的形式化,然后利用阶乘幂的高阶逻辑形式分析实数二项式系数,最后将实数二项式系数应用于分数阶微积分的形式化。分数阶微积分的形式化分析表明了实数二项式系数及其运算性质形式化的正确性和有效性。     

分数阶非因果BP神经网络模型

由一阶因果、反因果微分的定义推导出Caputo分数阶因果、反因果微积分,并在此基础上定义Caputo分数阶非因果微积分。将它们分别应用于BP神经网络的反向传播过程中对权值进行处理,产生了Caputo分数阶因果、反因果和非因果BP神经网络模型。为了方便对比,将这些模型分别对波士顿房屋数据集和MNIST数据集进行处理。模拟结果表明：在整数阶因果、反因果和非因果的模型之间,整数阶非因果模型的结果最好;分数阶因果、反因果和非因果模型分别与其相应的整数阶模型进行比较,得出分数阶模型得到的准确率比整数阶的高;在分数阶因果、反因果和非因果的模型之间,非因果的准确性最高。总的来说,Caputo分数阶因果、反因果和非因果微积分都对传统BP神经网络有优化作用,尤其是分数阶非因果微积分的优化效果最好。     

连续傅里叶变换基础理论的高阶逻辑形式化

连续傅里叶变换(CFT)在数学和工程技术领域都有着广泛应用.利用高阶逻辑定理证明器HOL4,实现了对连续傅里叶变换定义及其常用运算性质的形式化,包括线性、频移、反转性、积分、时域一阶微分及高阶微分运算性质,为采用形式化方法分析相关系统奠定了基础.最后利用定理证明的方法对电阻电感电容(RLC)串联谐振电路的频率响应特性进行了验证,说明了CFT形式化的初步应用.     

分数阶Birkhoff系统基于Caputo导数的Noether对称性与守恒量

在Caputo分数阶导数下研究分数阶Birkhoff系统的Noether对称性与守恒量.首先,定义Caputo分数阶导数下的分数阶Pfaff作用量,建立分数阶Birkhoff方程及其相应的横截性条件;其次,基于Pfaff作用量在无限小变换下的不变性,分别在时间不变和时间变化的无限小变换下,给出了不变性条件.基于Frederico和Torres的分数阶守恒量概念,建立了分数阶Birkhoff系统的Noether定理,揭示了分数阶Noether对称性与分数阶守恒量之间的内在联系.     

分数阶系统状态空间描述的数值算法

利用Grünwald-Letnicov分数微积分定义计算分数微积分的数值解,计算精度仅为1阶,不能满足快速收敛性要求.给出并证明了分数阶微积分的高阶近似所应满足的条件,并在此基础上推导出分数阶线性定常系统状态空间描述的数值计算公式.本法不但公式简单易编程,而且具有计算精度高、运算速度快等优点.给出一个粘弹性动态系统的仿真实例,验证了其有效性.     

基于HOL4的形式化方法

针对计算机系统设计的正确性问题,研究了一种在测试空间上完备的形式化方法,探讨了硬件系统在定理证明器HOL4中进行形式化验证的一般方法,其中包括如何采用高阶逻辑形式化描述系统的实现与规范,以及在HOL4中证明目标的一般过程.同时,以乘法器为实例,提出一种功能分解法对需要分析的电路进行形式化建模,并对模型的性质在HOL4中进行推理与验证,从而证明了乘法器电路设计的模型满足所提取的性质.     

Riemann-Liouville型分数阶导数的非线性估计（英文）

本文主要研究任意有界连续信号的Riemann-Liouville分数阶导数估计问题.当分数阶α属于0到1时,首先利用滑模技术提出一种有界连续信号分数阶导数的非线性估计方法;然后将其结果推广至分数阶α∈R⁺的情况,并给出相应的非线性估计方案.借助Riemann-Liouville分数阶微积分频率分布模型,本文详细分析讨论了所给分数阶导数非线性估计的收敛性问题,并得到相应闭环系统是渐近稳定的结论.文中所提方法的主要优点是在事先未知给定信号分数阶导数上界的情况下,不仅能自适应地估计其Riemann-Liouville分数阶导数,而且当信号中含有随机噪声和不确定扰动时依然能正常工作.数值仿真实例验证了本文所给估计方法的可行性和有效性.     

函数矩阵及其微积分的高阶逻辑形式化

函数矩阵广泛应用于动态系统的建模与分析。传统的函数矩阵分析主要采用纸笔演算、数值计算和符号推导的方法,这些方法不能保证提供精确或正确的结果。高阶逻辑定理证明作为一种高可靠的形式化验证方法,可以克服以上不足。在高阶逻辑定理证明器HOL4中对函数向量和函数矩阵相关理论进行形式化,内容包括函数向量和函数矩阵及其连续性、微分、积分的形式化定义和相关性质的逻辑推理证明。为示范函数矩阵形式化的应用,最后给出机器人运动学中旋转矩阵微分公式的形式化验证。     

变阶分数阶微分方程的数值解法综述

近年来,分数阶微积分作为一种工具已经被广泛应用于工程中的各个领域.较常阶分数阶微积分算子而言,变阶分数阶微积分算子能够更加准确地描述复杂系统的物理特性,变阶分数阶微积分建模作为一个强大的数学工具,为工程建模提供了便利.在前人优秀研究成果的基础上,结合近几年的国内外相关学者的研究成果对变分数阶微积分方程的研究作全面的综述.以变阶分数阶微分方程、变阶时间分数阶对流-扩散方程、变阶分数阶反应-扩散方程、变阶分数阶积分-微分方程和时滞变阶分数阶微分方程为主要研究对象,从变分数阶微积分算子的相关定义、模型、数值解及在工程中的相关应用等几个方面进行介绍.研究发现,近年来的算法多集中在多项式算法的基础上,通过构建不同的运算矩阵来实现变阶微分方程到代数方程组的转换.该综述可为相关领域的研究学者提供参考.     

SpaceWire译码电路在HOL4中的形式化验证

SpaceWire是在苛刻环境下的高速通信总线协议,译码电路是其接收端的关键电路,对该电路进行形式化验证具有重要的现实意义.形式化验证方法中的定理证明将需要分析的电路进行形式化建模,结合定理证明器,对模型的性质进行严格推理从而完成验证.本文运用定理证明的方法,在高阶逻辑证明工具HOL4中对SpaceWire总线的译码电路进行形式化验证.首先根据SpaceWire标准规范抽取相关性质,用高阶逻辑语言形式化描述;然后分析电路设计中的VHDL代码,依据代码实现的功能用相应的逻辑谓词建模;最后在HOL4中证明了译码电路设计的模型能满足所提取的性质.本文同时给出了形式化建模的方法和验证过程.     

A note on fractional-order derivatives of periodic functions

In this paper, it is shown that the fractional-order derivatives of a periodic function with a specific period cannot be a periodic function with the same period. The fractional-order derivative considered here can be obtained based on each of the well-known definitions Grunwald-Letnikov definition, Riemann-Liouville definition and Caputo definition. This concluded point confirms the result of a recently published work proving the non-existence of periodic solutions in a class of fractional-order models. Also, based on this point it can be easily proved the absence of periodic responses in a wider class of fractional-order models. Finally, some examples are presented to show the applicability of the paper achievements in the solution analysis of fractional-order systems.     

On the Formalization of Gamma Function in HOL

The Gamma function is a special transcendental function that is widely used in probability theory, fractional calculus and analytical number theory. This paper presents a higher-order logic formalization of the Gamma function using the HOL4 theorem prover. The contribution of this paper can be mainly divided into two parts. Firstly, we extend the existing integration theory of HOL4 by formalizing a variant of improper integrals using sequential limits. Secondly, we build upon these results to formalize the Gamma function and verify some of its main properties, such as pseudo-recurrence relation, functional equation and factorial generalization. In order to illustrate the practical effectiveness and utilization of our work, we formally verify some properties of Euler’s generalized power rule of differentiation, Mittag-Leffler functions and the relationship between the Exponential and Gamma random variables.     

The HOL logic extended with quantification over type variables

The HOL system is an LCF-style mechanized proof assistant for conducting proofs in higher-order logic. This paper discusses a proposal to extend the primitive basis of the logic underlying the HOL system with a very simple form of quantification over types. It is shown how certain practical problems with using the definitional mechanisms of HOL would be solved by the additional expressive power gained by making this extension.     

Partial and Nested Recursive Function Definitions in Higher-order Logic

Based on inductive definitions, we develop a tool that automates the definition of partial recursive functions in higher-order logic (HOL) and provides appropriate proof rules for reasoning about them. Termination is modeled by an inductive domain predicate which follows the structure of the recursion. Since a partial induction rule is available immediately, partial correctness properties can be proved before termination is established. It turns out that this modularity also facilitates termination arguments for total functions, in particular for nested recursions. Our tool is implemented as a definitional package extending Isabelle/HOL. Various extensions provide convenience to the user: pattern matching, default values, tail recursion, mutual recursion and currying.     

Self-Formalisation of Higher-Order Logic

We present a mechanised semantics for higher-order logic (HOL), and a proof of soundness for the inference system, including the rules for making definitions, implemented by the kernel of the HOL Light theorem prover. Our work extends Harrison’s verification of the inference system without definitions. Soundness of the logic extends to soundness of a theorem prover, because we also show that a synthesised implementation of the kernel in CakeML refines the inference system. Apart from adding support for definitions and synthesising an implementation, we improve on Harrison’s work by making our model of HOL parametric on the universe of sets, and we prove soundness for an improved principle of constant specification in the hope of encouraging its adoption. Our semantics supports defined constants directly via a context, and we find this approach cleaner than our previous work formalising Wiedijk’s Stateless HOL.     

The Right Tools for the Job: Correctness of Cone of Influence Reduction Proved Using ACL2 and HOL4

We present a case study illustrating how to exploit the expressive power of higher-order logic to complete a proof whose main lemma is already proved in a first-order theorem prover. Our proof exploits a link between the HOL4 and ACL2 proof systems to show correctness of a cone of influence reduction algorithm, implemented in ACL2, with respect to the classical semantics of linear temporal logic, formalized in HOL4.     

Mechanizing some advanced refinement concepts

We describe how the HOL theorem prover can be used to check and apply rules of program refinement. The rules are formulated in the refinement calculus, which is a theory of correctness preserving program transformations. We embed a general command notation with a predicate transformer semantics in the logic of the HOL system. Using this embedding, we express and prove rules for data refinement and superposition refinement of initialized loops. Applications of these proof rules to actual program refinements are checked using the HOL system, with the HOL system generating these conditions. We also indicate how the HOL system is used to prove the verification conditions. Thus, the HOL system can provide a complete mechanized environment for proving program refinements.