题目：模态逻辑中若干问题的研究

从经典命题逻辑的观点来看,命题不真即假. 但是,如果我们对这些命题做更深入的分析, 就会发现,无论是真命题还是假命题都可以分为两类: 一类是必然的;一类是偶然的.如果我们把必然性和可能性看作是命题和真值发生某种关系的方式,并且把这类含有可能和必然概念的命题称为模态命题, 那么经典的命题逻辑显然不涵盖这些模态命题,就更不能反应它们之间的关系及推理的有效性,从而新的逻辑----模态逻辑系统就诞生了.模态逻辑通过引入了新的模态算子, 达到了形式化各种模态概念的目的,并讨论这些概念之间的逻辑关系.模态系统的语义理论是基于莱布尼茨关于可能世界的思想展开的,从而一个模态命题的真值情况就和 一个与它相关联的更大的空间密不可分,这个空间就是可能世界之集,它当中的元素可以是世界、时间、理论和计算状态等等.
本文从两个方面对模态逻辑做了进一步的研究:
第一章将程度化的思想引入模态逻辑, 对可能世界进行了细致地分析和讨论,首先提出了标准模型的概念,并且在标准模型下定义了公式的Borel型区间值真度的概念,建立了区间值真度理论. 并且得到了和谐定理,即,若公式不含任何模态词,那么它对应的Borel型区间值真度的上下真度值相等,从而区间值就退化为一个点, 并且这个点就是该公式的Borel型真度值. 之后,还研究了区间值真度的性质以及它与极大相容理论之间的对应关系.
第二章研究了常见的模态系统S4,S5中极大相容理论的性质,提出了对于一个极大相容理论,任意一公式关于这个理论的存在状态,状态描述等一系列概念,最后给出了S5中的极大相容理论的一个刻画,证明了任何一个极大相容理论都是所有简单合取和析取公式的某一存在状态之集的理论闭包.
描述逻辑作为形式化地表示知识及其推理的有效工具,是一阶谓词逻辑的一个可判定子系统.因为描述逻辑系统具有较强的语言表达能力和可判定性,它所提供的判定性推理服务总能保证推理算法最终停止,所以在众多知识表示的形式化方法中, 描述逻辑一直受到人们的特别关注.描述逻辑的研究对象是Tbox和Abox, Tbox中的元素是术语 (terminology), 它提供一个概念的定义,这个概念被语义地解释为论域上的一个子集,而Abox中的元素是断言 (assertion), 它用来储存论域上的知识.描述逻辑中的许多问题如包含检测、一致性问题、实例检验等都可最终归约为可满足性问题,这就使得可满足性问题成为描述逻辑的核心问题,判定一个给定的Tbox和Abox是否可满足也就相应地成为描述逻辑的第一任务.
为了能用计算机来自动判断描述逻辑中的可满足性问题,Schmidt-Schaub和Smolka首先建立了基于描述逻辑ALC的Tableau算法, 该算法能在多项式时间内判断描述逻辑ALC概念的可满足性问题. 目前, Tableau算法已用于描述逻辑对应的各种语言中(如ALCN, ALCQ等).
第三章针对上述这一重要的算法, 指出在最广泛的语言形式ALCN中,如果对Tableau算法中6条规则的使用顺序不加任何约束或者限制,那么就会出现算法循环永不终止的情形. 针对这一弊端,本章对其进行了简化和改进,提出了标准tableau-based算法,使得基于这个新算法,判定ALCN Abox相容性的问题可以在有限步终止,并且这个新算法不再对其中六条规则的施行顺序加以任限制和约束,从而说明新算法的实用性.
最后,本文第四章针对模糊模态逻辑和模糊描述逻辑中经常要使用的工具--三角模,做了进一步深入的研究,在广义三角模和广义剩余蕴涵等概念的基础上,讨论了广义三角模和广义剩余蕴涵的性质之间的对应关系,完善和修正了过去已有的一些定理结论,证明广义三角模和广义剩余蕴涵两者之间存在着两大类的对应关系.