多元协同演绎在一阶逻辑ATP中的应用

一阶逻辑是数理逻辑中重要的分支,对其逻辑公式的自动推理是人工智能领域重要的研究热点之一. 目前一阶逻辑自动定理证明大多采用二元归结方法，每次只有2个子句进行归结，只消去1组互补对，导致演绎归结式文字数较多，影响了演绎效率. 为此，基于矛盾体分离规则提出了一种多元协同演绎算法，该算法每次允许多个子句进行协同演绎，消去多组互补对，从而演绎分离式文字数较少且可控，能有效提高推理能力；并且，该算法通过有效演绎权重和无效演绎权重调整子句演绎顺序，利用回溯机制搜索较优路径，有效规划演绎路径. 将该算法应用于国际顶尖证明器Eprover 2.1，以CADE2017竞赛例（FOF组）为测试对象，对加入多元协同演绎算法的Eprover 2.1证明器进行试验. 试验结果表明其能力超过了Eprover 2.1:多证明定理8个；能证明Eprover 2.1未证明定理31个，占未证明总数的28.2%.      

基于边权重图神经网络的一阶逻辑前提选择

为提高自动定理证明器在大规模问题中证明问题的能力,前提选择任务应运而生.由于公式图的有向性,主流的图神经网络框架只能单向地对节点进行更新,且无法编码公式图中子节点间的顺序.针对以上问题,提出了带有边类型的双向公式图表示方法,并提出了一种基于边权重的图神经网络（edge-weight-based graph neural network,EW-GNN）模型用于编码一阶逻辑公式.该模型首先利用相连节点的信息来更新对应边类型的特征表示,随后利用更新后的边类型特征计算邻接节点对中心节点的权重,最后利用邻接节点的信息双向地对中心节点进行更新.实验比较分析表明：基于边权重的图神经网络模型在前提选择任务中表现得更加优越,其在相同的测试集上比当前最优模型的分类准确率高了约1%.     

Matheius定理的几点认识

Matheius定理是针对离散数学以及解决正整系数整数线性规划问题中多约束条件情况的应用性定理。通过介绍该定理及其证明,作者对定理的证明过程,及参数λ的存在性提出了一些看法,同时对定理的应用和图解方面进行了探讨,以期能够促进相关领域对该定理的重视和更广泛的应用。     

控制Lorenz混沌系统到平衡点

应用线性反馈法与延迟反馈法控制Lorens混沌系统．在线性反馈控制系统中，用Routh—Hurwitx定理，证明Lorens系统的三个平衡点在增益k大于某一阈值时，都是渐近稳定的；在延迟反馈控制系统中应用F1oquet理论和Hurwitz定理，证明在增益延迟积κι大于某一阈值时，两个非零平衡点是渐近稳定的，而零平衡点总是不稳定的．数值仿真结果验证了上述两种情况下各平衡点的可控性、稳定性．在实际问题中，常常要求系统能过一段时间后进入定常态，所以，线性反馈法与延迟反馈法控制混沌系统到平衡点的问题的研究具有实际应用的意义．     

基于形式化方法的平交道口控制系统安全设计

铁路平交道口控制系统是一种典型的安全苛求系统，为提高铁路平交道口的安全性，提出一个能适应双线双向接车的自动控制系统.首先，分析现有铁路平交道口的作业流程，利用新的控制系统解决现有系统中常见的三个问题，即出清检查、制动距离限制、连续接车中防护门短时间开放问题；其次，基于Event-B语言以及精化策略对设计的自动控制系统建立形式化模型；最后，检查证明义务以验证需求属性是否被满足，并应用动画器Animation展示系统功能的正确性.结果显示：相比传统的道口管理系统，本文提出的自动控制系统增加了双线连续接车功能，且使用形式化建模和验证，避免系统设计中存在的二义性，对平交道口安全管理有一定的参考意义.     

模糊商空间理论两个定理的补充

张铃等在“模糊粒度计算方法”中,核心定理证明中构造的等价关系是循环定义的,且没有证明它的截关系与商空间所对应的等价关系是相等的;模糊等价关系的粗细定义与模糊集理论的意义不一致,容易引起歧义．本文用通用的模糊数学符号和序代数理论的方法和观点对其进行修正和补充,给出两个定理的完整证明,使得相关结果的表达更简洁和规范,完善了模糊商空间理论．     

货运索道支架位置自动搜索方法

针对货运索道支架位置自动搜索方法缺失的问题，提出了凸包点遍历法、地形自适应法和干涉点搜索法等3种索道支架位置自动搜索方法，均能够实现二维地形剖面上的索道支架位置自动搜索. 其中:凸包点遍历法在地形凸包点建立支架，通过冗余支架筛除获得支架位置；地形自适应法通过判断索道承载索曲线在下降过程中与地形的干涉条件确定支架位置；干涉点搜索法采用在承载索曲线与地形的最大干涉位置添加中间支架的方法实现支架位置搜索. 3种方法的支架位置搜索成功率差别不大，分别为9.12%、8.38%和8.26%，但干涉点搜索法的计算速度分别是凸包点遍历法和地形自适应法的5.8倍和3.5倍. 因此，在实际工程应用中，建议使用速度最快的干涉点搜索法进行输电线路货运索道支架位置自动搜索.      

面向海图信息发布的点符号模型设计与实现

海图符号在GIS上的显示与在纸质载体信息发布所呈现的方式不同,导致符号在信息发布时不能及时准确地转换。针对此问题,提出一种符号信息发布的通用样式规范,采用中间件的方式,使用XML对需要转换的符号进行规范化描述,并对描述进行解析,使其能够通过PDF发布或出版,实现数据模型的解析输出,使海图符号信息能够自动准确并及时地更新发布。此转换模型有助于海图符号的传递和共享,保证数据的及时性和一致性。     

基于生成对抗网络的交通流参数实时估计模型

为有效调控道路网时空资源，需实时估计交通流参数。若要准确估计交通流参数，应详细考虑道路网交通流时空特征。本文基于生成对抗网络，提出一种能捕捉交通流时空特征的实时估计模型，即TSTGAN模型。该模型包括生成器和判别器两部分，生成器利用门控卷积神经网络 捕捉交通流的动态空间特征，使用基于注意力机制的长短期记忆神经网络分析交通流的动态时间特征；采用门控卷积神经网络与长短期记忆神经网络构建判别器；通过对抗方式训练生成对抗网络的生成器与判别器，实时获得交通流参数估计值。使用中国山东省淄博市12个卡口设备和美国加州洛杉矶市23个线圈检测器获得的交通流量数据，验证TSTGAN模型的可靠性。结果表 明，TSTGAN模型引入的时空模块能有效提取交通流的时空特征，所得均方根误差和平均绝对误差比现有模型分别降低2.12%~42.41%和1.66%~40.49%，证明所提TSTGAN模型可以提高交通 流参数的估计精度。     

并联离线再生式颗粒捕捉器的试验研究

介绍一种并联式颗粒捕捉器及其试验情况.这种颗粒捕捉器采用2个壁流式金属烧结毡过滤器芯,2个滤芯并联安装,交替工作和再生.再生策略采用工况背压作为再生开始的条件,电加热引燃,采用控制再生空气流量的办法控制再生速度和再生温度.试验和实车运行证明该颗粒捕捉器新鲜状态时过滤效率63%,使用后期过滤效率81%,对实际运行油耗的影响在3%以内,可进行自动再生,满足车载使用要求.该过滤器可用于车辆的黑烟治理和采用EGR技术的欧IV发动机.     

粗集决策与聚类分析的改进模型

通过分析粗集理论与聚类分析的内在联系，从理论上探讨了两者的融合机理，并给出了相关的数学证明．考虑到粗集决策难以构造决策表的缺陷，采用聚类分析构造等价关系扩展信息表，提出了等价聚类的概念。建立了基于聚类分析的粗集模型；考虑到聚类分析权重确定存在的问题，采用粗集理论的属性约简思想，解决聚类分析中的权重和冗余性问题，建立了基于粗集理论的聚类分析模型，从而解决了原有模型的不足．     

考虑排放控制区的绿色多式联运路径和速度优化

针对考虑排放控制区的绿色公海多式联运路径和速度优化问题，本文首先构建不同碳排放政策下多目标混合整数非线性规划模型，并根据问题特性将其转化为等价的线性模型；其次，为有效求解模型，提出融合问题特性的改进自适应遗传算法，根据问题特点设计多层编解码机制和自适应遗传进化策略；最后，以我国某公海多式联运系统为例，验证所提模型和算法的有效性，并针对不同时间窗和低硫燃油价格进行敏感性分析。实验结果表明：与传统遗传算法和商业求解器Lingo相比，改进自适应遗传算法能获得更满意的方案，分别减少了5.2%和3.7%的多式联运总成本；强制碳排放政策下，排放限额的变化一般不会改变经营人的路线选择，只会影响经营人是否进行运输活动；碳税政策下，碳税价格上涨对多式联运总成本影响很小；碳交易政策下，不同排放限额的多式联运方案可能一致；货物准备时间延后和截止时间提前会增加运输成本，船舶在排放控制区内外使用不同航速能够带来明显的经济效益。     

多人共站第一类混流装配线平衡问题的优化

针对使用传统模型和算法求解第一类多人共站混流装配线的平衡问题，兼顾工作站数、工人数和工作站负荷均衡，引入了新变量和不对称约束来构建新的数学模型. 提出了一种改进的鸡群算法，使用基于优先权值的编码方式在解码过程中优先选择能最早开始作业的工人来减少序列相关空闲时间，设定工位分配接受准则来分配工人数量以减少工位平均空闲时间；根据适应值大小将种群分为3个不同的群体来实现系统的有效搜索，其中，公鸡群个体基于其适应值差异在不同大小的邻域范围内搜索，母鸡群个体基于适应值相关的参数分别向所归属的公鸡或者其他公鸡/母鸡方向搜索，小鸡群个体则向其归属的母鸡方向搜索；最后将新模型和改进的鸡群算法用于求解标杆算例. 研究结果表明:在算例验证中，对比传统的模型，新模型多找出8个算例的最优解，且寻优速度更快；在算法平均收敛运算时间相似的情况下，本文所提算法求得的平均工人数、工位数以及平滑指标系数等评价指标分别提高了10.74%、16.05%和44.89%，验证了所提模型和算法的有效性和优越性.      

舰船保障装备效能评估方法研究

结合实例阐述了层次分析法和专家评分法的一般原理，并将这两种方法结合起来进行实例评估．在评估过程中，运用层次分析法来求取各评价指标的权重系数；运用专家评分法来对评价指标进行量化评分；最后将两者结果结合起来进行效能的计算及评估．实例证明将这种方法运用到舰船保障装备效能评估之中，能够进一步减少人为主观因素引起的误差，评估结果实用、有效。     

铁路网上带权重的车流径路优化方法

主要研究了铁路网上车流径路的选择优化问题，在充分考虑到起初路网中的车流具有不同同权重的情况下，建立了该问题的０－１规划模型，并讨论了带权重与不带权重两种车流径路优化模型之间的关系。     

Rolle定理的两个特殊证法

Ｒｏｌｌｅ定理是微分学中最基本，最重要的定理之一，在数学分析教程中，对于Ｒｏｌｌｅ定理的证明大多是千篇一律的，本文给出Ｒｏｌｌｅ定理的两个特殊证法。     

基于改进ACGAN的齿轮箱多模式数据增强与故障诊断

针对现有生成对抗网络(GAN)难以高效率生成多模式的故障样本和训练不稳定问题，提出了一种改进辅助分类生成对抗网络(ACGAN),并将其用于齿轮箱多模式数据增强和智能故障诊断，以确保运载工具的安全运行；引入独立的分类器构建新型ACGAN框架，改善了经典ACGAN的分类精度与判别精度之间的兼容性；使用Wasserstein距离定义具有平滑特性的新型对抗损失函数，以此克服GAN易出现模式崩塌和梯度消失的缺点；引入谱归一化方法替代权重裁剪，限制判别器的权重参数，提高对抗训练过程的稳定性；为验证改进ACGAN的有效性和优越性，对齿轮箱的6类健康状态样本进行试验分析。分析结果表明：改进ACGAN生成的故障样本在数据层面和特征层面取得了更好的质量评估结果，其中基于结构相似度的评估指标平均优于对比方法0.249 3,基于最大平均差异的评估指标平均优于对比方法0.696 6;改进ACGAN的训练过程更加稳定，其损失函数具有更优的收敛性，同时在多模式故障诊断情景下具有更高的效率，其训练时间缩减为对比方法的20%;针对故障样本缺失的情况，改进ACGAN的生成样本能有效辅助深度学习智能故障诊断模型的训练，可将...     

Cauchy微分中值定理的多种探究式证明法

以Cauchy中值定理为例,给出了7种Cauchy中值定理的探究式证明方法,探讨了探究式教学法在定理证明过程中的应用,为大学数学教学提出了更高的要求。     

铁路车辆自动防溜器装车试验研究

为了克服长期困扰铁路行业的车辆防溜作业强度大、效率低、安全可靠性差等问题,研制了铁路车辆自动防溜器。介绍了防溜器的工作原理,计算表明C70、C80型货车在空载和重载状况下铁路车辆自动防溜器的制动力能够得到保证。样品安装在58组116辆C70A型货车上,开展了试验列车的性能测试、空重车坡道防溜和运行考核试验,证明研制的铁路车辆自动防溜器单车防溜制动力强,能保证车辆在坡度不大于12‰任何线路上实现自动防溜、安全停放。较之传统的人工作业防溜措施在经济、社会效益方面具有明显的优势。     

表面粗糙度符号与参数的智能化标注

讨论了利用VBA在AutoCAD中快速准确标注表面粗糙度的实现技术和方法,阐述了各种情况下准确标注表面粗糙度所需的插入点和角度的动态确定方法,通过运行工程中的宏,能够在所选实体的指定位置自动生成符合国家标准规定的表面粗糙度符号。