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

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

基于有限格蕴涵代数的格值命题逻辑语义系统

以有限格蕴涵代数作为逻辑系统的真值域，在其上建立了基于有限格蕴涵代数的格值命题逻辑语义系统，研究了在A水平上系统的赋值和公式的可满足性等基本定义，证明了系统“有效性”的可判定性并给出了判定算法。     

一种新的模糊逻辑代数系统

基于对模糊逻辑和模糊推理的系统研究,一种新的模糊逻辑代数－Ｒ０代数已于近期被建立,这为模糊逻辑提供了一种新的代数框架。文中对Ｒ０代数作进一步研究,给出Ｒ０代数的一系列代数性质,并澄清Ｒ０代数与其它模糊逻辑代数系统之间的关系。