一种基于超连接的一阶逻辑反演推理算法

研究一种一阶谓词逻辑公式的反演求证算法,它是应用超连接过程来处理子句集的消解的,该算法具有比Ｒｏｂｉｎｓｏｎ的传统消解方法更高的效率．以一个实例讨论了该算法的应用,结果表明此算法可以保证在预定义的相关边界内,对任意一阶逻辑的推理具有终止性     

一种基于超连接的一阶逻辑反演推理算法

研究一种一阶谓词逻辑公式的反演求证算法,它是应用超连接过程来处理子句集的消解的,该算法具有比Ｒｏｂｉｎｓｏｎ的传统消解方法更高的效率,以一个实例讨论了该算法的应用,结果表明此算法可以保证在预定义的相关边界内,对任意一阶逻辑的推理具有终止性。     

自然推理系统中的假设前提引入与消去规则

形式化的自然推理系统最显著的特点就是引入假设前提.在自然推理中,可以根据需要随时引入假设前提,但是推理的结论不能依赖于假设前提,因此假设前提在其完成了使命后,必须被消去.运用假设前提消去规则进行推理就是按照“如果A1,A2,…,An├B,那么A1,A2,…,An-1├An→B”的规则进行语形变换的过程,但是理解假设前提消去规则何以能够消去假设前提这个问题,涉及到对前提与结论之间真假制约情况的讨论,属于语义解释的范围.     

一种基于事例推理的检索模型

以计算逻辑为理论基础设计了１种对象检索模型以解决定理机器证明中的“同理可证”问题,该模型采用基于事例的推理方法来进行推理,并将领域知识、控制性知识与事例知识分别统一到对象类层次结构上,因此结构清晰,可重用性高     

一种基于一阶谓词逻辑的模型表示方法

给出了一种应用于决策支持系统,基于一阶谓词逻辑的模型表示方法,并分析了此种表示方法的实用性和推理机制。     

两型自然推理系统的比较

1934年,S.Jaskowski与G.Gentzen几乎同时提出了所谓自然推理系统。两种系统都获得极大的发展,成为最受人们欢迎的系统。这两种系统各有优缺点,大体说来,前者最和人们日常的推理过程相近似,从而使用起来最为方便;后者则除可以不用割切(cut)规则外,各规则都是由简主繁,理论上最是简捷,没有兜圈子的毛病,最适宜于作理论上的探讨(尤其当讨论融贯性、可推导性等问题时)。因此长期以来,人们都认为使用时宜选择前者,作理论上探讨时,宜选择使用后者,并认为两者根本不同,无法变成一个。     

关于Cialdea一阶模态归结系统

指出了Ｃｉａｌｄｅａ一阶模态逻辑归结系统是不完备的．为了确保推理系统的完备性，给出了Ｃｉａｌｄｅａ系统的两种修正方法．     

基于本体的多Agent自动工艺系统

为把本体理念应用于多Agent的CAPP自动工艺系统，提出了基于本体的多Agent自动CAPP系统模型，并构造了单个Agent的基本架构；建立了该领域的零件本体库和特征本体库，采用基于RDF(S)的OIL语言对系统中的各Agent零件特征知识的语法和语义进行详细的描述与注释，并利用一阶谓词逻辑对各Agent之间本体转换规则的语法和语义加以描述；最后通过实例验证了本体的功能和转换规则的智能推理机制，从而很好地满足多Agent自动工艺系统之间零件特征知识共享、复用和互操作的需求，同时对其它领域知识信息的处理也有着很好的借鉴意义。     

带量词的合一算法

Ｒｏｂｉｎｓｏｎ于 １９６５年提出了归结原理，其主要工作是 Ｕｎｉｆｉｃａｔｉｏｎ算法。这个算法只能处理不带量词的子句公式，它不能用来发现定理的自然演绎证明。本文的算法能处理量词，它能用在基于自然演绎的定理证明系统上。文中给出合一定理的证明，基于此算法的自动自然演绎系统已实现，用它证明了Ａｎｄｒｅｗｓ；Ｂｌｅｄｓｏｅ和Ｐｅｌｌｏｔｉｅｒ挑战性问题。     

基于一阶模糊逻辑公式的有限解释真度的推理理论

通过给出公式的有限解释真度的平均值不变性定理,得到了一系列推理规则：平均值MP规则、平均值HS规则、平均值交推理规则．     

命题公式的一种演绎判定方法

命题公式的判定是人工智能领域中的一个核心问题。目前命题公式的判定方法大都是基于语义的,不能给出演绎过程,而这种演绎过程是许多推理性应用的重要依据,本文针对命题演算系统L,给出了一种可同时给出演绎过程的判定方法——演绎判定方法。首先提出了消解复杂性的两种范式：最简范式和文字范式,在此基础上给出了L的可判性定理的演绎证明及命题公式的演绎判定算法P(F),并基于ML语言设计了基于P(F)的演绎判定机DMBD。     

L^＊系统中的模糊演绎定理的改进形式

研究了模糊命题演算的形式演绎系统L^*，对其中的演绎定理进行了详细讨论，得到了在一定条件下的L^*系统中的演绎定理：设A，B∈F(S)，若|-(q→p∨p)∨q→A，Γ包含于F(S)，则|-A→B当且仅当rU{A}|-B，将L^*系统中的模糊演绎定理进行了改进，进一步说明了L^*系统所具有的良好性质．同时，在本文定理的证明中进一步体现了L^*系统中的公理L10在模糊命题演算形式演绎系统中的作用，为模糊命题演算的形式演绎系统的研究，特别是L10的应用研究提供了一种新的思路和方法。     

对扩展树证明的可靠性与完全性的简化证明(英文)

本文对扩展树给出一个不同的证明．它的长度比起Ｍｉｌｌｅｒ的证明要简短得多，而且改正了 Ｍｉｌｌｅｒ证明中的某些错误。     

扩展重言式

对于任何ｗｆｆ　Ａ，能够得到这样一个 ｗｆｆ，它和Ａ等价，且量词的辖域最小。如 果这后一个ｗｆｆ是重言式，则称Ａ是扩展重言式。还证明了，如Ａ是扩展重言式， 则Ａ。还定义了一个系统，对于这个系统的每一个定理，能够证明它是扩展重言式。     

基于改进的无穷值语义解释的中介谓词逻辑的λ-归结

中介谓词逻辑系统MF的无穷值语义解释,反映了反对对立概念之间的可变过程,并且该解释不同于MF的其他任何语义解释。但在该无穷值语义解释下,"当A fuz时～A真"这种情况并未得到反映。在此基础上,进一步研究得到了中介谓词逻辑系统MF一种真值域为[0,1-λ)∪(1-λ,λ)∪(λ,1](λ∈(0.5,1))的无穷值语义解释,重新定义了MF的文字,给出了MF中λ-互补文字及弱无中介集的定义,提出了一种新的MF的λ-归结原理,并证明了其可靠性和完备性。在改进的MF的无穷值语义解释下,不仅较好的表达了"当A fuz时～A真"的情形,而且其λ值的确定,可根据一定的实例知识计算出来,具有客观性。该解释进一步表明用中介逻辑作为模糊知识的表示与推理的工具是可行的。     

强模态归结

研究了命题模态逻辑Ｋ,Ｋ４,Ｄ,Ｄ４,Ｔ,Ｓ４的“”型模态逻辑结果的自动推理．提出了证明“”型模态逻辑结果的归结推理方法─—强模态归结．证明了强模态归结的可靠性与完备性．