可计算性逻辑中若干形式系统及算子的研究

发布时间：2024-03-11 06:05

　　可计算性逻辑是新近提出的关于可计算性的形式理论.它采取交互的博弈语义,是一种资源逻辑.经典逻辑、直觉逻辑和线性逻辑(在广义上)只是可计算性逻辑的三个特殊部分.相比于传统逻辑,可计算性逻辑具有更强的表达能力和更高的证明效率,这使得它有望在知识库系统、人工智能行为规划系统、电路等价性验证等领域得到广泛的应用. 本文主要利用可计算性逻辑的Cirquent演算方法,对其若干形式系统及算子进行了研究,主要工作和创新概括如下： ●证明了Cirquent演算系统CL6关于可计算性逻辑语义的可靠性与完备性.首先给出与证明相关的所有语法定义；然后利用形式系统CL2关于可计算性逻辑语义的可靠完备性,间接地从语法角度证明了系统CL6的可靠完备性,从而得到既是经典命题逻辑又是Cirquent演算系统CL5的扩张. ●揭示了平行复发算子与不可数分支复发算子的关系.首先给出关于平行复发算子的Cirquent演算系统；其次定义关于平行复发算子的Cirquent的语义;然后在此定义基础上证明关于平行复发算子的Cirquent演算系统的可靠性,得到由不可数分支复发算子诱导的逻辑是由平行复发算子诱导的逻辑的真子集；最后,...

【文章页数】：113 页

【学位级别】：博士

【文章目录】：
作者简介
算子符号说明
摘要
ABSTRACT
第一章 绪论
    1.1 可计算性逻辑的背景与现状
        1.1.1 研究背景与意义
        1.1.2 研究进展与现状
    1.2 博弈语义
    1.3 形式系统CL4
    1.4 Cirquent演算系统CL8
    1.5 本文的主要工作与结构安排
第二章 Cirquent演算系统CL6的可靠性与完备性
    2.1 引言
    2.2 Cirquent、系统CL5及系统CL2
    2.3 形式系统CL6
    2.4 形式系统CL6的可靠性与完备性
    2.5 小结
第三章 平行复发算子与不可数分支复发算子的关系
    3.1 引言
    3.2 关于平行复发算子的形式系统CL15
    3.3 Cirquent的语义
    3.4 平行复发算子与不可数分支复发算子的关系
    3.5 小结
第四章 可数分支复发算子与不可数分支复发算子的关系
    4.1 引言
    4.2 关于可数分支复发算子的形式系统CL15
    4.3 可数分支复发算子的新定义
    4.4 Cirquent的语义
    4.5 可数分支复发算子与不可数分支复发算子的关系
    4.6 小结
第五章 可计算性逻辑的优越性
    5.1 引言
    5.2 命题逻辑公式的压缩表示及其相应的形式系统
    5.3 Cirquent演算系统CL8S的演绎定理及其证明复杂度
    5.4 基于可计算性逻辑的知识库系统
    5.5 小结
结束语
致谢
参考文献
在读博士期间撰写(发表)的论文
在读期间参加研究的科研项目



本文编号：3925937