一类积分不等式的机器判定

将一类积分不等式转化为Tarski模型外的齐次对称多项式不等式,该类齐次对称多项式的次数是给定的,变元个数可以是任意多个,并且多项式的系数是与变元个数相关的变系数.这些特点与杨路等人最近提出的几个公开问题密切相关,是比较有代表性的一类齐次对称多项式.然后利用Timofte关于对称多项式不等式判定的降维方法,结合不等式证明软件BOTTEMA及差分代换方法,给出对应的一类Tarski模型外的齐次对称多项式不等式的机器判定算法,从而实现原积分不等式的机器判定.当给定的积分不等式及齐次对称多项式不等式不成立时,可给出具体不成立的数值反例.应用例子表明问题的广泛性及算法的有效性.     

离散时间系统的鲁棒稳定性分析--积分二次约束方法

利用新近发展起来的积分二次约束（ＩＱＣ）方法,对离散时间系统,给出了其鲁棒稳定性分析准则,使一大类古典稳定性结果可以统一和概括在积分二次约束的框架之下。并且,利用积分二次约束方法,讨论了一类混合摄动系统的鲁棒稳定性。     

利用决策支持系统分析可重构制造系统中的问题

可重构制造系统是面向新世纪的先进制造模式 .本文提出利用决策支持系统解决可重构制造系统所面临的重构决策问题 ,在系统决策、加工单元布局、以及可重构产品的生产计划问题上采用智能化算法 ,可以得到满意的结果     

基于AADL的无线传感器网络的建模与分析

利用结构分析与设计语言AADL(Architecture Analysis and Design Language)对无线传感器网络进行建模,并对其中一个节点进行了详细的分析.介绍AADL语言以及它在嵌入式系统中建模的优势,展示了无线传感器网络的特征和关键技术.结合AADL,针对温度传感器案例,对温度传感器的结构及功能进行了详细描述,充分体现了此传感器节点的工作原理与内部结构,有助于提高其结构上的可改进性和扩展性,以进一步应用到传感器网络中.     

常用基本不等式的机器证明

不等式机器证明问题是智能系统领域的难点和热点问题.借助不等式证明软件BOTTEMA,对若干常用的基本不等式成功地实现了机器证明,包括算术、几何与调和平均不等式、排序不等式、Chebyshev不等式、Bernoulli不等式、三角形不等式及Jensen不等式等.所论不等式含有的变元个数是一个不确定的变量,属于Tarski模型外的不等式类型.机器证明得出的结论有时可能是已知结果的推广,其方法本身对同类不等式有示范性,更多的例子表明了该算法和软件的有效性.     

选择公理与Tukey引理等价性的机器证明

基于计算机证明辅助工具Coq,提出一种选择公理与Tukey引理等价性的形式化证明.在公理化集合论形式化系统基础上,给出选择公理与Tukey引理的形式化描述,这是Tukey引理的首次形式化.完成了选择公理与Tukey引理等价性的证明代码,并在Coq中通过验证.体现了基于Coq的数学定理机器证明具有可读性和交互性的特点,其证明过程规范、严谨、可靠,在集合论、拓扑学和代数学的形式化构建中具有重要应用.     

特定消谐脉宽调制开关角度的实解个数

为了解决特定消谐脉宽调制技术中开关角度非线性超越方程组的实解个数问题,利用三角函数倍角公式将非线性超越方程组转化为带不等式约束的多项式方程组,提出了一种基于半代数系统机器证明算法的实解分类方法.给出了N=3时的单相和三相逆变器以及N=4时的单相逆变器开关角度实解个数的完全分类,同时首次得到了分类边界点的解析解.理论推导和实验仿真结果表明:该方法能够从理论上给出调制比和实解个数之间的变化关系,对于开关角度的求解以及提高逆变器的消谐效果具有重要的指导意义.     

求解特定消谐变换器开关角度的并行完备算法

结式消元法在求解特定谐波消除脉宽调制变换器的开关角度时会遇到中间表达式膨胀耗尽内存的问题,为此文中提出基于多项式插值的方法,将结式行列式的展开转化为插值点计算和线性方程组求解2个步骤,并给出了该方法并行实现的主要流程。计算结果显示此方法能够有效避免中间表达式膨胀的问题,所能求解的开关点数大幅提升。针对开关点数为6的变换器,给出了全调制比范围内的开关角度,实验结果验证了所求开关角度的正确性。     

基于微分动态逻辑的铁路道口控制分析

利用微分动态逻辑对铁路道口控制进行形式化分析与建模.在火车从发送接近信号到进入道口的运动过程中,根据火车到达道口时间上的要求,将火车速度控制问题抽象成一个混成系统的安全性性质,用微分动态逻辑来描述,并使用混成系统证明工具KeYmaera对系统的安全性进行验证,以实现对火车进入道口前速度的正确控制.     

基于Coq的杨忠道定理形式化证明

实现拓扑学定理的机器证明,是吴文俊院士生前的宿愿.杨忠道定理涉及一般拓扑学中的诸多基本概念,对深刻理解拓扑空间的本质有重要意义.该定理表明,拓扑空间中每一个子集的导集为闭集当且仅当此空间中的每一个单点集的导集为闭集,是一般拓扑学中的一个重要定理.基于定理证明辅助工具Coq,从公理化集合论机器证明系统出发,对一般拓扑学中的开集、闭集、邻域、凝聚点和导集等拓扑基本概念进行形式化描述,给出这些概念基本性质的形式化验证,建立了拓扑空间的形式化框架.在此基础上,实现基于Coq的杨忠道定理形式化证明.全部引理、定理和推论均完整给出Coq的形式化描述和机器证明代码,并在计算机上运行通过,体现了基于Coq的数学定理机器证明具有可读性、交互性和智能性的特点,其证明过程规范、严谨、可靠.杨忠道定理的形式化证明是一般拓扑学形式化内容的一个深刻体现.