一阶逻辑中的扩展子句消去原则

对于一阶逻辑定理证明器，子句集化简一直是必不可少的步骤，这将有助于提高后续一阶逻辑定理证明器的证明效率. 针对子句冗余性的判断，提出了一种评估子句冗余性的原则:集合蕴涵模归结原则. 并且证明了该原则在不带等词一阶逻辑上的可靠性，根据该原则删除子句，不会影响原始子句集的不可满足性或者可满足性. 此外，依据该原则提出了两种新型的一阶逻辑预处理方法:集合归结包含消去（set resolution subsumption, SRSE）方法和集合归结不对称恒真消去（set resolution asymmetric tautology elimination, SRATE）方法，并证明了这两种子句消去方法在不带等词一阶逻辑子句集上的可靠性. 最后在理论上比较了SRSE方法和归结包含消去（sesolution subsumption elimination, RSE）方法以及SRATE方法和归结不对称恒真（sesolution asymmetric tautology elimination, RATE）方法之间的有效性，结果表明SRSE方法和SRATE方法分别比RSE方法和RATE方法更为有效.      

基于符号权重的一阶逻辑前提选择方法

为增强自动定理证明器从一阶逻辑问题的大规模前提中选择相关前提的能力，首先，提出符号权重计算公式，基于符号在问题中出现的频率获取不同符号对应的权重；其次，提出相关度计算公式，利用分配的符号权重计算问题中前提和结论间的相关度；同时，研究自适应相关度边界，用于判断前提与给定的结论是否相关；最后，在自动定理证明器中交互地结合前提选择和自动推理两个过程，可在充分选择相关前提的情况下及时停止前提选择过程.实验结果表明：在最优情况下，新提出的前提选择方法能够把参与证明的平均前提数量从1 876个降低到174个；与广泛使用的前提选择方法 E-SInE和Vampire-SInE相比，使用新方法能够帮助自动定理证明器E在MPTP2078基准测试集上分别提高19.49%和10.49%的证明率.     

基于路径搜索的格值命题逻辑自动推理方法

提出一种基于路径搜索的自动推理算法．除了采取预处理外，还采用了动态的删除策略，使对大部分路径的搜索变成对一条路径搜索．可快速地完成对一类格值命题逻辑中的任何一个子句集可满足性与不可满足性的判定．文中还讨论了该算法计算的复杂性．     

利用逻辑演绎求解SAT问题的启发式完全算法

为解决可满足性(satisfiability problem,SAT)问题求解过程中分支决策效率不高的问题,提出了一种基于逻辑演绎分组(logical deduction group,LDG)的启发式完全算法.该算法通过选择剩余未满足子句参与逻辑演绎,得到一组局部可满足赋值序列,并引导求解器优先搜索赋值序列所在解空间;对于可满足问题,可以通过迭代调用演绎过程,将局部可满足解成组地扩充为全局可满足解,对于不可满足问题,如果演绎结果出现空子句,则可以直接判定.采用SAT国际竞赛的实例,与具有代表性的指数级变元状态独立下降和(exponential variable state independent decaying sum,EVSIDS)变量决策算法进行了对比测试,结果表明:在求解总问题数方面,LDG比EVSIDS多出42个;在求解速度方面,LDG对可满足问题的求解时间相较EVSIDS平均减少了22.8%,对不可满足问题的求解时间平均减少了17.8%,总平均时间减少了20.1%.     

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

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

基于多元线性回归的线性系统状态空间辨识算法

提出了一种新的多变量线性系统状态空间辨识算法.该算法采用多元线性回归,而不是传统算法中的子空间投影.首先通过多元线性回归获得系统的预估器马尔可夫参数,然后基于一个关鍵等式获得系统的预估器可观性矩阵与状态序列的乘积矩阵,接着通过奇异值分解得到状态序列,最终再次运用多元线性回归求得系统状态空间模型的各个矩阵.由于本文的算法是预估器式的,因此适用于开环和闭环辨识.基于AIC准则,设计了算法的阶次选择策略,通过仿真例子,验证了该算法的有效性.     

���ڶ����οռ��������Ч·���������㷨

交通路网中有效路径的确定方法是进行各类随机交通流量分配的关键技术. 通过将启发式策略中的定向策略与层次空间推理策略相结合，模拟树的生长，提出了一种有效路径的定向层次空间推理搜索算法. 通过将该方法应用于随机用户均衡分配模型，说明了该方法的有效性. 该算法可以与各类随机交通分配模型结合，并为交通规划人员提供有力工具.     

业务模型驱动的应急物流本体知识表示及应用

为解决应急物流智能协作面临的异构信息融合与知识管理难题,以有效知识应用为目标,利用业务模型与本体模型对组成构件上的相关性进行映射,并根据系统控制与实体行为约束所需的业务推理规则,设计了3种模块之间的关系与四阶段转换步骤,形成了业务模型驱动的本体表示方法.以该方法为基础,结合应急物流领域需求,建立了由概念集合、概念属性、语义约束、推理规则等要素组成的应急物流本体模型.通过应急配送路径选择案例,自动推理得到可替代邻近点以完成配送路径求解.结果表明,应急物流本体模型及其应用实现了异构信息的本体融合,消除了以关键词匹配为基础的常规检索失效现象,满足了最小路径算法的执行条件,为应急物流决策模型及算法应用提供了知识层面的支持.      

基于Martins算法的联合运输最优路径规划

为了快速高效地找出最优的联运路径,在现有模型的基础上,考虑时间窗约束,建立了具有多目标、多运输方式、多货种的路径选择改进模型,并设计了2层搜索算法求解该模型.第1层在已知每条路径标签的基础上,根据时间窗删除规则并利用改进的Martins算法,计算出有效路径集;第2层将第1层的有效解作为其初始解,删除不满足货物运输总时间、中转次数和运输方式容量3个限制条件的路径,得到最优路径集合.根据货主的需求,采用序数偏好方法,组合不同的费用权重和时间权重得到综合权重值,找出对应最大综合权重值的最优路径.实例分析表明:相比已有的标签算法,改进算法增加了运算方式容量限制条件,缩小了解空间,避免了生成无效路径;相比拉格朗日松弛算法只能求得解的上下限,本文算法能够求得精确解,耗时在30 s以内,计算时间减少75%.      

接触网检修计划自动编制模型构建与应用

针对接触网检修计划人工编制效率低又难以实现优化的问题，将接触网检修计划编制转化为一个规划优化问题，利用整数规划方法，同时考虑接触网检修作业的连续性，将设备检修状态作为决策变量，以超周期惩罚费用与检修路径代价最小为优化目标，建立基于弹性周期区间的接触网检修计划自动编制模型，并基于多目标规划中分层序列法提出模型的启发式求解算法. 通过实际算例验证证明:该方法可实现接触网检修计划的自动编制与优化，编制时间相对于人工节省99.98%，巡检路径节省33.16%，提高了接触网检修计划的编制效率和效果.      

α-Automated Reasoning Method Based on Lattice-Valued Propositional Logic LP(X)

This paper is focused on automated reasoning based on classical propositional logic and lattice-valued propositional logic LP(X).A new method of automated resasoning is given ,and the soundness and completeness theorems of this method are proved.     

J-Resolution Fields of Generalized Literals of L14 P（X）

Introduction In order to study the lattice-valued logic system,Xu[1]proposed the concept of lattice implication alge-bra by combining the lattice with the implication alge-bra and discussed its properties systematically. InRefs.[2,3], a lattice-valued propositional logic sys-tem was established using the concepts of free alge-bra, which corresponds to the lattice implication alge-bra, and the semantic and syntactical problems of thissystem were discussed. Xu et al[4]extended the reso-lution p…     

基于改进蚁群算法的多AGV泊车路径规划

针对智能停车库中自动导引小车(Automated Guided Vehicle,AGV)存取车的路径规划问题,提出一种基于改进蚁群算法的多AGV泊车路径规划方法.单AGV路径规划方面,在基本蚁群算法基础上引入蚂蚁回退策略来增强适应性,同时改进启发式信息和信息素更新策略提高算法的收敛速度和寻优能力.多AGV路径规划方面,提出改进冲突解决策略来解决多AGV之间的冲突,其中采用临时规避-重新寻路策略来解决相向冲突.针对某典型停车场抽象模型的仿真结果表明,改进蚁群算法寻路成功率更高,并具有较强的全局搜索能力和较快的收敛速度,改进冲突解决策略能合理避免冲突,可以满足多AGV存取车路径规划的要求.     

基于Ant-agent 的自动化码头AGV 控制算法

为解决自动化码头水平运输区存在的自动导引车(AGV)路径冲突和道路死锁问题,提高运输效率,将AGV视为蚂蚁智能体(Ant-agent),设定其携带负反馈机制的信息素进入运输路网. 引入拥挤度及拥挤度阈值q ,建立新的状态转移规则;针对节点冲突和路径拥堵,构建解决机制;提出基于Ant-agent 的AGV控制算法,采用两阶段均匀设计试验法确定算法最优参数组合. 仿真结果表明,与传统动态路径规划算法对比,所提算法在各运输任务量下的避碰性能、解锁性能和运输效率均有较大提高,可有效地解决AGV路径冲突和道路死锁,提高运输效率.     

用于最短路算法的公交网络模型构建

公共交通线路网络的复杂化使乘客难于选择最优的出行线路。用于最短路算法的公交网络模型,解决了有向图难以承载票价和换乘这两个出行要素的问题,有效地把公交出行要素包含在弧中,使得最短路算法可以直接根据这些要素搜索最优出行方案。     

Power-Aware Anycast Routing in Wireless Sensor Network Exploiting Small World Effect

By considering energy-efficient anycast routing in wireless sensor network (WSN), and combining small world characteristics of WSN with the properties of the ant algorithm, a power-aware anycast routing algorithm (SWPAR) with multi-sink nodes is proposed and evaluated. By SWPAR, the optimal sink node is found and the problem of routing path is effectively solved. Simulation results show that compared with the sink-based anycast routing protocol (SARP) and the hierarchy-based anycast routing protocol (HARP), the proposed algorithm improves network lifetime and reduces power consumption.     

Ideal resolution principle for lattice-valued first-order logic based on lattice implication algebra

As a continuate work,ideal-based resolution principle for lattice-valued first-order logic system LF(X) is proposed,which is an extension of α-resolution principle in lattice-valued logic system based on lattice implication algebra.In this principle,the resolution level is an ideal of lattice implication algebra,instead of an element in truth-value field.Moreover,the soundness theorem is given.In the light of lifting lemma,the completeness theorem is established.This can provide a new tool for automated reasoning.     

基于层次分析法的应急救援最优路径选择分析

运用图论中的最短路径相关知识,综合道路交通的各种相关因素,给出道路应急救援系统中最优路径选择的解决方法.首先应用层次分析法分析影响路径的权重系数,然后用Dijkstra算法求出最短路径,并通过MATLAB进行计算仿真,结果表明此方法能够有效地解决应急救援系统中的最优路径问题.     

自动化码头多AGV路径冲突的优化控制研究

针对自动引导车(AGV)在自动化码头水平运输过程中可能发生的路径冲突问题,提出一种将AGV路径容量、安全距离、行驶时间及行驶速度相结合的多参数优化控制模型.Dijkstra算法规划多条AGV路径,位向量交集运算法检测路径冲突,改进的速度控制策略通过控制AGV在冲突节点处的行驶速度,解决冲突问题.对某自动化码头的AGV路网进行仿真实验和分析.比较停车策略、速度控制策略和改进的速度控制策略的结果,验证了改进速度控制策略在AGV路径冲突问题中的可行性及有效性.