形式背景的几种分离性

利用拓扑方法定义了形式背景的T0,T1,T2分离性,探讨几种分离性之间的关系,并研究诸分离性的性质.证明了诸分离性对兼容子背景是遗传的且被满足一定条件的背景映射所保持.另外,还得到拓扑空间(X,τ)的上述几种分离性与形式背景(X,τ,∈)的相应分离性在一定条件下是一致的.     

基于关联格的概念格约简理论

研究概念格与其关联格之间的关系并给出了两者之间的同构定理,进而研究了由概念格的关联格来进行属性约简的理论与方法。     

一种验证数控系统软件安全可靠性的建模方法

作为一个典型的离散计算机控制系统,CNC(数字控制)系统在运行中需要满足可靠性和安全性。因此如何设计出安全可靠的系统软件以及如何有效地对CNC系统的安全性和可靠性进行验证成为一个非常重要的问题。基于此给出一个新的建模方法TTM/ATRTTL(时间转化模型/全时轴实时时态逻辑)来描述和验证CNC系统。TTM/ATRTTL提供了一整套方法用于描述CNC系统建模的硬实时特性和反馈特性,也提供了一个包括一整套验证规则和定理的验证模型并且应用工具STeP和SF2STeP来实现之。这个验证模型可以用于对TTM/ATRTTL表达的系统的可靠性,安全性进行验证。使用该建模和验证方法可以对OAC(开放式体系结构CNC)系统进行分析和验证,并设计出OAC的逻辑控制器,该控制器是OAC系统的核心部分。验证结果表明,该形式化建模与验证方法可以有效地对CNC系统进行分析和建模。在此基础上,可以开发出能够保证系统可靠性和安全性的CNC系统软件。     

形式三角矩阵环上导子的几个结果

设A,B是有单位元的结合环,M是一个非零(A,B)-双模,D为形式三角矩阵环 Tri(A,M,B)={(^a₀ ^m_b)|a∈A, m∈M, b∈B} 上的导子。如果对于任意X,Y∈Tri(A,M,B), D(X^m)=(D(X))ⁿ或D((XY)ⁿ)=D(Xⁿ)D(Yⁿ) 成立,其中m,n≥1为固定的整数,那么D=0。     

卫星定位系统的验证原型

用模型检查的方法对卫星定位系统进行了验证,对把模型检查应用于实际系统进行了初步的探索。     

普遍声逆散射微扰论与形式参数展开法

使用第一作者提出的形式参数展开法给出了在Ｂｏｒｎ 和Ｒｙｔｏｖ 变换下的有限形式声衍射层析成像理论算法．所给出的Ｂｏｒｎ 变换下的有限形式重建公式对散射体的要求比较松,适用于一类中强散射情况,而且计算量也不大．Ｒｙｔｏｖ 变换下的有限形式重建公式,因涉及广义散射,所以Ｓｏｍ ｍ ｅｒｆｅｌｄ 辐射条件不再成立,用它进行重建仍有很大困难．本文还给出了单频任意波阵面入射波情况下更普遍逆散射微扰论,包括Ｒｙｔｏｖ 变换下积分形式声逆散微扰理论．     

一类三角函数方幂之和

用发生函数的方法得到三角函数方幂与等比序列乘积之和以及含有两个不同三角函数乘积方幂和的计算公式．     

mKdV方程的新椭圆函数解

提出一种求解非线性微分方程椭圆函数解的方法,并通过此方法,求出了mKdV(modified Korteweg-de Vries)方程的多个椭圆函数解,涵盖了一些已知解,也包括新的无理式解及一些新的椭圆函数解,这些解在某些情况下可退化为孤子解和三角函数解。此方法还可用于求解其它非线性微分方程。     

汉语动宾谓语句的形式刻画

运用认知范畴论的观点对动宾谓语句作类典型和非类典型的划分,着力分析这两类语句的不同特征;在此基础上,作者借助一阶谓词逻辑、类型论、λ演算等工具,对汉语类典型动宾谓语句与两种非类典型动宾语句作初步的形式刻画。     

基2的流水式快速傅里叶变换处理机的形式化模型

快速傅里叶变换(FFT)的应用领域非常广泛,其硬件实现方法多种多样。传统的电路正确性验证的方法是模拟,这种方法的主要缺点是不能穷尽模拟全部输入情况,而形式化方法使用纯数学手段证明电路具有某些属性,从而证明其正确性。所以用形式化方法验证FFT电路的正确性具有极强的实用价值。形式化验证的第一步工作是对要验证的电路进行建模,因此本文首先介绍了国内外FFT形式化建模的主要方法和优缺点,然后用重写系统给出了任意N=2M点的基2的流水式快速傅里叶变换处理机的形式化模型,显示了重写系统用于复杂硬件电路建模的优越性,为进一步的电路正确性验证奠定基础。