知识库系统的逻辑基础

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

函数/逻辑归约演算系统ELNF

ELNF 演算是我们在 LNF 演算的基础之上自然扩展逻辑处理设施而成的函数/逻辑演算系统。本文简要介绍了 ELNF 的概念,较详细地描述了扩展的内容与方法.     

状态逻辑语言迭代程序的可计算性

状态逻辑型程序设计语言是一种有坚实理论基础，既可描述递归又可描述迭代的高效，实用、新型的纯逻辑式程序设计语言，递归无疑地确保了其计算能力，本文证明了仅用状态逻辑的迭工程序冰可计算部分递旭函数，这就等于证明了，任何图灵可计算的对象都可用纯逻辑代地定义和高效地计算。     

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

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

区间逻辑的一个辅助证明工具

DC/P(duration calculus prover)是一族实时区间逻辑的辅助定理证明工具.它采用Gentzen风格相继式演算作为基本证明系统,并结合项重写、自动判定算法等技术以提高证明的自动化程序.该文介绍了DC/P的语义编码方法、采用的相继式证明系统及实现技术,并给出了应用实例.     

IF函数的使用

本文分析IF函数在EXCEL中的各种应用。通过公式、IF函数等的使用EXCEL中的表格数据将更加精炼、规范。     

悖论逻辑及其表演算

悖论逻辑LP是一个超协调逻辑,极小悖论逻辑LPm是一个LP的非单调逻辑扩展.本文给出了一阶LP和LPm的表演算.为此,本文在论证了(极小)悖论逻辑语义性质基础上,首先给出一个LP的(记号)表演算,然后给出一个LPm的极小表演算,并证明了两个表演算分别对于LP和LPm语义的可靠与完全性定理.     

状态逻辑语言迭代程序的可计算性*

状态逻辑型程序设计语言是一种有坚实理论基础，既可描述递归又可描述迭代的高效、实用、新型的纯逻辑式程序设计语言．递归无疑地确保了其计算能力本文证明了仅用状态逻辑的迭代程序就可计算部分递归函数．这就等于证明了，任何图灵可计算的对象都可用纯逻辑迭代地定义和高效地计算．     

悖论逻辑的表演算

悖论逻辑ＬＰ是一个超协调逻辑，发展超协调逻辑（ＬＰ）的目的是使得不会从矛盾推出任一命题，但它有一个主要缺点：就是一些在经典逻辑中有效的推理在ＬＰ中不再有效；极小悖论逻辑ＬＰｍ能克服这个缺点，使得在没有矛盾的直接影响下超协调逻辑等价于经典逻辑．ＬＰ和ＬＰｍ原来都只给出语义定义，虽然已有ＬＰ的证明论，但如何得到一个ＬＰｍ的证明论仍是一个未解问题．本文提出了一种可靠与完全的表演算作为ＬＰ与ＬＰｍ的证明论．     

基于模糊命题模态逻辑的形式推理系统

探讨基于可信度的模糊命题模态逻辑的形式推理,给出相关的模糊Kripke语义描述.其研究目的旨在解决基于模态命题逻辑的模糊推理的能行问题.在研究过程与方法上,以完全形式化的方法将模糊模态逻辑语法和语义统一在一个形式系统中,以模糊约束作为基本表达式,给出推理规则,建立了相应的模糊推理形式系统,并以形式系统中模糊约束集的可满足性来表示模糊推理的有效性,使模糊推理过程变得容易,为最终在计算机上实现基于模态逻辑的模糊推理打下了一定的基础.主要结论是证明了基于可满足性的模糊推理形式系统的可靠性与完备性.     

命题逻辑中形式推演证明题的自动评阅系统

自动阅卷评分是大规模计算机考试的必然选择,而数学类主观题涉及运算符号、运算步骤、解题方法多样等问题,其自动评分一直制约着考试系统的发展。数理逻辑是数学的一个分支,命题逻辑是数理逻辑的一部分。命题逻辑的同一个形式可推演性模式可以有不同的形式证明,即存在一题多解的情况,但其证明有严格的程式,针对其特点用C#开发一个适用于其自身的自动评分系统。应用表明,系统操作界面友好,可大大提高教师阅卷的工作效率。     

概率命题逻辑是经典命题演算形式系统的随机事件语义

经典命题演算形式系统(CPC)中的公式只是一些形式符号,这些形式符号的意义是由具体的解释给出的.概率逻辑是在标准概率空间上建立的一种逻辑体系,是CPC的随机事件语义,对联结词的解释就是集合运算,对形式公式的解释就是事件函数,对逻辑蕴涵和逻辑等价的解释就是事件(集合)包含和事件相等=.由于不存在处处适用的真值函数(算子),概率逻辑不能在CPC内实现概率演算,但可在CPC内实现事件演算,CPC完全适用于概率命题演算.     

带有不同否定的模糊命题逻辑的形式演绎系统

对于模糊知识及其否定关系,潘正华指出应该明确地分为矛盾否定关系、对立否定关系和中介否定关系,并建立了一种具有矛盾否定、对立否定和中介否定的模糊集FScom（fuzzy sets with contradictory negation, opposite negation and medium negation）,随后建立了一种改进的模糊集IFScom（improved FScom）。为给模糊集FScom及其改进IFScom提供一种逻辑工具,提出了一种带有矛盾否定、对立否定和中介否定的模糊命题逻辑演算系统FPcom,并在给定无穷值语义赋值模型以及可满足性定义下,证明了FPcom具有可靠性和完备性。FPcom在一定意义上可视为对中介命题演算系统的改进。     

相干命题逻辑系统R的一种演绎生成算法

本文提出了相干命题逻辑系统R的一种演绎生成算法--试探法。该算法采用后向推理法,依据推理规则将待证命题逐步分解成子命题并构造一棵证明树,对系统R中的定理证明取得了较好的效果。     

Independent Choices and the Interpretation of IF Logic

In this paper it is argued that Hintikka's game theoreticalsemantics for Independence Friendly logic does not formalize theintuitions about independent choices; it rather is aformalization of imperfect information. Furthermore it is shownthat the logic has several remarkable properties (e.g.,renaming of bound variables is not allowed). An alternativesemantics is proposed which formalizes intuitions aboutindependence.     

命题中介逻辑的可靠和完备Gentzen推导系统

中介逻辑是朱梧槚先生提出的一个3-值逻辑.给出了一个命题中介逻辑,其中引入中介连接词~、反对连接词◁以及蕴涵连接词→,并且定义否定连接词.给出了一个Gentzen-型的推导系统,使得该系统关于中介逻辑的3-值语义是可靠的和完备的.