基于可计算性逻辑的知识表示与推理

以可计算性逻辑的完备子集CL4为基础进行知识表示,将知识分为简单知识与一般知识.通过分析知识库系统的特点和需求,给出了采用正反向混合推理方法的推理机设计,并举例说明以CL4为基础的知识库系统,具有能够表达和查询更细致的知识、便于用户和系统交互的优点.

可计算性逻辑中CL4系统定理证明

可计算性逻辑的形式系统CL4具有强大的表达能力和很好的应用前景,为了进一步完善其理论基础,采用严格的逻辑方法,对该系统中的相关重要定理进行证明。证明过程及其结果显示,该系统中的一般原子表示一般的可计算性问题,在意义上有别于经典逻辑中的原子。

可计算性逻辑中CoL2系统的可判定性分析

可计算性(Computability)即算法有解性,是数学和计算机科学领域中重要的概念之一。可计算性逻辑(Computability Logic,CoL)是关于可计算性的形式理论,是一种交互的资源逻辑。其中,CoL2系统采用博弈的语义,是对经典命题逻辑的扩展,在经典命题逻辑的基础上添加了选择运算和一般原子,比经典命题逻辑更富有表达力,具有更广阔的应用前景,并且有较高的证明效率。分析了CoL2系统的可判定性,即通过提出一个算法来判断任意一个CoL2公式是否是可证明的,并且证明了该算法是多项式空间内运行的。

可计算性逻辑研究进展

可计算性逻辑(Computability Logic,简称CoL)在交互计算算法理论、运算集合和基于Cirquent的推理系统等方面得到持续研究。在可计算性逻辑中,经典逻辑的公式表示成了交互计算的问题;求解可计算性问题的过程可以看成是机器(计算部件)和环境(输入输出部件)之间的博弈;经典逻辑的公式“真”值表示在可计算性逻辑中存在着一个有效解;推理系统的建立采用自然演绎推理方法,图形化表示的cirquent允许不同的父结点可以有相同的子结点,保证资源可以共享,资源共享还可以有选择进行区分,而且,这种基于电路式的推理已经证明比传统的Gentzen相继式推理证明效率有指数级的提高。Cirquent演算的灵活性、高效性、表达性强等特点,使它正成为CoL的一种公理化工具。

知识库系统的逻辑基础

针对知识库系统的研究现状和存在的问题,分析了用经典一阶谓词逻辑作为知识库系统逻辑基础的不充分性,根据知识库系统的特点和需求,指出可计算性逻辑既能为知识库系统提供合理的逻辑基础,又能弥补经典逻辑作为知识库系统逻辑基础的不足.并在此基础上用证明论方法,建立了一个基于可计算性逻辑的完备子集CL4的知识库系统的公理系统,显示出易于表达、操作简单的特点.

Extended IF逻辑的命题演算系统

Extended IF逻辑是一阶逻辑的扩张,其主要特点是可表达量词间的相互依赖和独立关系,但其命题部分至今没有得到公理化.基于Cirquent演算方法,给出了一个关于Cirquent语义(命题水平)可靠完备的形式系统.该系统能够很好地解释和表达命题联结词间的相互依赖和独立关系,从而使Extended IF逻辑在命题水平得到了真正意义上的公理化.