Tableau算法的优化及模型规约技术
摘要：为了近一步提高模态逻辑推理机的效率,提出了两种Tableau算法优化技术——冲突技术和矛盾学习技术,并结合这两种技术实现了针对模态逻辑S4的推理机S4P.在此基础上,为了从Tableau算法生成的模型图中构造一个规模较小的模型,又提出通用模型的概念,然后给出通用模型的规约技术并证明该技术对于任意依赖于公理D、T、B、4和5中部分或全部公理的正规模态逻辑的正确性.最后,使用逻辑工作台测试用例对S4P的效率进行测试,实验结果表明S4P的效率优于RACER和FaCT＋＋;同时,对S4P生成的测试用例中非有效公式的否定对应的通用模型进行规约,实验结果表明通过模型规约能明显地缩减模型的规模.直接优化性能指标的多排序模型融合方法
摘要：现有排序学习算法忽视了查询之间的差异,在建立排序模型的过程中等同对待训练样本集中的所有查询及其相关文档,影响了排序模型的性能.文中描述了查询之间的差异,并在训练过程中考虑查询之间的差异,提出了一种基于有监督学习的多排序模型融合方法.这种方法首先使用每一个查询及其相关文档训练出子排序模型,并将每一个子排序模型的输出转化为体现查询差异的特征数据,使用监督学习方法,实现了多排序模型的融合.更进一步,针对排序问题的特性,文中提出了一种直接优化排序性能的融合函数融合子排序模型,使用梯度上升方法优化其下界函数.文中证明了直接优化排序性能的融合函数融合子排序模型的性能优于子排序模型线性合并的性能.基于较大规模真实数据应用的实验结果表明,直接优化性能指标的多排序模型融合方法可以比传统排序学习模型具有更好的排序性能.模糊语义下知识系统的结构及信息传播的研究
摘要：文中提出模糊概念空间及规则空间,作为对知识系统进行形式化表示的统一框架.首先,基于形式概念分析理论以及L模糊集构造了概念粒,通过对概念粒之间关联关系的研究定义了概念射,进而构造了高层次知识单元“概念粒簇”.概念粒簇由不同概念粒聚合而成,作为模糊概念空间中的结构层次.其次,通过定义概念粒之间语义整合的先验规则以及积运算构造了规则空间,阐明了概念粒在规则空间的作用下相互之间进行信息传播的机制.文中的结论为进一步研究模糊语义下知识系统的动态构成及演化机制奠定了理论基础.粒子滤波算法
摘要：粒子滤波算法逐渐成为科学领域的研究热点.文章首先阐述了粒子滤波算法的提出背景,根据m阶马尔科夫假设,分析算法基本原理并推导后验概率密度及权值更新公式.分析了基本粒子滤波算法中存在的问题以及解决方法.针对粒子滤波算法重要性采样密度的选择问题,综述了重要性采样密度选择方法.对重采样技术及样本匮乏问题进行了深入的分析,讨论了算法收敛性分析的最新进展.对自适应粒子滤波算法以及粒子滤波算法在各主要应用领域的进展进行了论述.最后对粒子滤波算法的研究前景提出了展望.一种基于冲突的增量诊断方法
摘要：增量诊断是一种在离散事件系统中进行诊断的重要方法,因其能够根据新观测和原有诊断的结果进行进一步诊断,在长时间复杂行为的系统上有着良好的运行效率和诊断特性.文章提出了一种带有回溯的增量诊断方法.在离线定义的自动机链模型上根据在线观测进行局部诊断,用轨迹概率选出最可能诊断的同时,保存可行的候选诊断作为回溯点.若增量过程产生冲突,则回溯并根据新观测动态重新对候选诊断选择排序.既避免了不完全可诊断性条件下,增量诊断所面临的多候选选择,亦避免了由于仅保留最优结果导致的重复诊断.基于特征子集区分度与支持向量机的特征选择算法
摘要：考虑特征之间的相关性对于其类间区分能力的影响,提出了一种新的特征子集区分度衡量准则——DFS（Discernibility of Feature Subsets）准则.该准则考虑特征之间的相关性,通过计算特征子集中全部特征对于分类的联合贡献来判断特征子集的类间辨别能力大小,不再只考虑单个特征对于分类的贡献.结合顺序前向、顺序后向、顺序前向浮动和顺序后向浮动4种特征搜索策略,以支持向量机（Support Vector Machines,SVM）为分类工具,引导特征选择过程,得到4种基于DFS与SVM的特征选择算法.其中在顺序前/后向浮动搜索策略中,首先根据DFS准则加入/去掉特征到特征子集中,然后在浮动阶段根据所得临时SVM分类器的分类性能决定刚加入/去掉特征的去留.UCI机器学习数据库数据集的对比实验测试表明,提出的DFS准则是一种很好的特征子集类间区分能力度量准则;基于DFS与SVM的特征选择算法实现了有效的特征选择;与其他同类算法相比,基于DFS准则与SVM的特征选择算法具有非常好的泛化性能,但其所选特征子集的规模不一定是最好的.三分之二模拟拓扑
摘要：三分之二模拟为验证系统的实现满足其规范提供了抽象描述.为了刻画系统的实现逐渐接近于规范,该文利用网极限的观点,以三分之二模拟为基础,建立系统实现的收敛机制,说明系统规范是其实现的极限形式.首先提出三分之二极限模拟和三分之二模拟极限的定义,建立三分之二模拟的极限理论.其次,建立三分之二极限模拟的拓扑结构,包括子网闭包、尾闭包、自然延拓和复合,证明三分之二模拟极限构成一个收敛类,并诱导一个拓扑,给出三分之二模拟极限的拓扑理论.最后,证明三分之二模拟极限在各种复合算子下的拟同余性（pre-congruence）,进而说明各种复合算子关于三分之二模拟极限的连续性.L（k）-index：一种支持标签路径的高效k双拟结构索引
摘要：针对基于k双拟的结构索引创建和更新低效问题、查询结果重复验证问题以及标签路径不可获得性问题,提出了一种新的结构索引L（k）-index.L（k）-index通过引入标签路径,在创建时无须k次遍历原数据,并采取批量更新策略,大大提高索引创建和更新的效率,而在空间上仅有很小增加.对于长度大于k＋1的路径查询,L（k）-index无须访问原数据进行验证,并支持批量节点的标签路径获得.通过大量实验表明,同∧（k）-index相比,L（k）-index创建时间平均提高66.7％,查询处理时间效率平均提高68.9％,批量更新效率平均每节点提高58.8％,而空间仅增加22.5％.Vague时间段关系与Vague区域关系的表示和复合推理
摘要：Vague时间段关系和Vague区域关系的表示和复合推理问题在时空数据库和人工智能等领域具有重要的研究意义.为了处理复杂的Vague时间段关系,基于Vague集形式化给出了Vague时间段、Vague时间段划分等重要概念;给出了基于Vague集的线性Vague时间段关系模型和周期性双向叠合Vague时间段关系模型;进一步提出了Vague时间段关系和Vague区域关系的复合推理策略和推理算法;给出了实验分析和实例模型,对实例模型进行了详细的讨论.研究成果可处理Vague时间段和Vague区域内其时刻点和区域点的不确定的隶属信息,可较好地表示和分析Vague时间段关系和Vague区域关系及其复合推理问题.基于完备抽象解释的性质强保留抽象研究
摘要：在模型检验中,抽象是解决状态空间爆炸问题的重要方法.通常的抽象是非强保留的,即可能存在时序性质在抽象模型不满足而在具体模型满足的情况.文中首先系统地构造μ演算Lμ语义模型的安全抽象,在此基础上,转换为通用Kripke结构下的安全抽象.然后基于抽象解释框架及完备抽象解释和性质强保留之间的关系,构造使得Lμ性质强保留的最小抽象模型精化,并转换为抽象解释中抽象域的最小完备精化.依据此完备抽象域求得性质强保留的最优抽象状态划分,从而构造出性质强保留且最优的抽象状态转换系统.形式背景与协调决策形式背景属性约简与概念格生成
摘要：通过引入交式可约元概念,文中提出了一种形式背景属性约简的新方法.基于此方法,获得了形式背景属性约简个数计算的精确公式,改进了原有的约简个数估计.在此基础上,给出了概念格的生成算法及其图示.最后,针对协调决策形式背景,通过实例给出了新的属性约简方法.经典命题逻辑的概率语义及其应用
摘要：文中将经典命题逻辑的赋值域由二值（（0,1}）推广到概率空间,引进了命题公式的概率赋值并建立命题逻辑的概率语义,证明了一个命题公式为重言式当且仅当其在每个概率赋值下的值都等于1.引入了命题公式的概率真度、不确定度、∧-概率真度、∧-不确定度等概念,并说明了∧-概率真度是已有的二值命题逻辑各种真度概念的推广,通过讨论∧-概率真度的性质,表明∧-概率真度在全体公式集F（S）上满足Kolnogorov公理.证明在形式推演的一个有效推理中,结论的∧-不确定度不超过各前提的∧-不确定度与其必要度的乘积之和.利用公式的∧-不确定度引进公式间的∧-相似度和∧-伪距离,证明了在一定条件下所建立的∧-伪距离空间没有孤立点且通常的逻辑运算关于∧-伪距离是连续的.在∧-伪距离空间中,提出了F（S）上的两种不同近似推理模式,并通过实际应用例子说明所提出的近似推理模式是有效的.基于动作空间的三维装箱问题的确定性高效率求解算法
摘要：三维装箱问题要求将有限个三维矩形物体尽可能多地装入到一个三维矩形箱子中,使得箱子的填充率即体积利用率最大.在求解三维装箱问题的穴度算法的基础之上,进一步做了以下改进：（1）将当前剩余空间中可能放入的每个体积最大的三维矩形虚拟物体所对应的空间定义为动作空间,在动作空间内放入物体并使穴度的定义体现放入物体与动作空间的吻合程度;（2）在物体放入位置的选择上直接体现“金角银边草肚皮”的思想,每一步只选择最靠近箱子边缘的一个动作空间来装载物体;（3）结合捆绑策略,将形状大小相同的物体捆绑为一个较大的矩形块进行放入,对捆绑块形状大小的选择为在不超出动作空间的前提下尽量用物体填满该空间的两至三个维度.实验结果表明,改进后的穴度算法在付出很少的开销代价的情况下显著地提高了箱子的填充率.仿生蚊子追踪算法
摘要：旅行商问题（Traveling Salesman Problem,TSP）是NP完全问题中最为著名的问题,它易于陈述而难于求解,至今尚未找到准确有效的求解大规模TSP问题的方法.文中提出了能求出TSP有效近似最优解的新的蚊子追踪（Mosquito Host Seeking,MHS）算法,证明了蚊子的目标追踪行为和MHS数学模型的一致性、蚊子追踪算法的收敛性,并通过理论证明确定了MHS算法中各参数的选择范围.蚊子追踪算法是一个全新的仿生算法.文中以TSP问题为载体,详细提出了蚊子追踪算法的动机、生物学模型、数学模型、算法、理论基础（数学证明）及大量实验结果.从理论和实验两方面证明了蚊子追踪算法能够求出TSP问题理论上的优化解.基于向量的几何可读自动证明
摘要：几何定理机器证明已经成功发展了多种新方法,但其中对中学几何中向量的机器证明研究没有抓住其回路的基本特征.文中以向量的回路为出发点,提出了基于回路的向量可读证明新方法,开发了机器证明新程序.该程序对常见的构造类型欧氏几何题目能快速作图,并依据题目类型的不同,分别用不同的向量方法对其进行自动推理,证明结果简短可读.经过大量实例测试,证明将向量用于几何自动推理是可行和高效的.与《超级画板》等中的证明器相比,文中算法在自动推理能力和证明过程可读性方面有较大提高.文中给出的基于向量的几何可读证明算法丰富了几何定理自动推理方法,并且具有应用于几何教学实践的价值.自动获取派生谓词规划领域的通用规划
摘要：通用规划（解）是针对某个领域的像算法一样的规划解,通过对其的解释可以直接得出具体问题的规划解,而不需要调用任何规划系统.但是目前通用规划的提取只能在一些简单或者特殊的领域中进行,没有推广到复杂或者一般的规划领域.该文提出在包含派生谓词的规划领域自动获取通用规划的方法.与已有获取方法不同的是：首先,基于派生谓词规则,文中方法明确指出派生谓词目标与动作效果之间的依赖关系,用以完善通用规划中动作应用的目的;其次,在提取过程中借助角色来帮助识别规划解中的循环结构.实验结果表明,文中方法不仅容易在派生谓词规划领域中获取通用规划,而且还能够以较好的性能求解一类以派生谓词为主要目标的规划“难”题.该文是在派生谓词规划领域中提取通用规划的首创性工作.基于汉明距离递减变换的可逆逻辑综合算法
摘要：可逆逻辑综合是指对给定的可逆函数自动构造对应的可逆逻辑电路.现有的可逆逻辑综合算法虽然通过后期优化能够得到近似最优解,但是都存在生成的原始电路门数较多的问题,增加了后期优化工作的难度.文中提出一种基于真值表异位数计算的综合方法,根据异位数判定是否需增加逻辑非门达到减少输入和输出向量的汉明距离,从而实现边计算边简化函数,最后采用汉明距离递减变换的方法生成最终的电路.通过实验表明,相比于其他的综合算法,该算法得到的原始电路更接近于最优解或近似最优解,很大程度上减少了算法后续的优化工作量.贝叶斯预测型进化算法
摘要：提出了一种新型进化算法即贝叶斯预测型进化算法,该算法是有效解决遗传算法中的连锁和欺骗问题的一种新方法,其主要特点是：（1）该算法基于最优解的概率分布和贝叶斯定理预测最优解所在的子空间;（2）该算法能高效利用所有先前代蕴含的信息,可以方便地引入专家知识;（3）该算法模型比较简单并且能以很快的速率收敛到最优解子空间.从理论上分析了贝叶斯预测型进化算法的收敛性、收敛速率和逆收敛算子.理论分析与在14个标准的测试函数上的仿真实验显示了该算法求解较为精确、稳定和快速.