论文部分内容阅读
认知逻辑是研究知识推理和信念变化的模态逻辑的一个分支,在人工智能、多agent系统以及对策论等领域有着广泛应用。长期以来,学术界在经典逻辑的基础上对认知逻辑开展了深入而广泛的研究,针对不同知识类型建立了相应的逻辑系统加以刻画。近年来,一批学者将直觉主义构造性观点和认知逻辑相结合,在直觉主义逻辑基础上对认知逻辑展开研究。这种研究为强调构造性和能行性的计算机科学相关领域的研究提供了新的逻辑工具。众所周知,直觉主义逻辑除了基于证明概念的BHK(Brouwer-Heyting-Kolmogrov)语义、基于Heyting代数的代数语义还有基于真值的Kripke语义。Kripke结构是模态逻辑的重要语义结构之一,易于理解且与形式化方法中诸多结构相似,在此结构上的逻辑语言可以作为描述计算系统性质的规范语言。所以,直觉主义认知逻辑的诸多研究基于Kripke结构展开。但是,由于兼顾认知模态词和直觉主义否定词的语义解释,这些Kripke结构的可达关系需要满足更多的约束性质,这就给相关逻辑系统完备性证明中模型的构造带来困难。尤其是对含有公共知识这种具有不动点语义特性的模态词的逻辑系统而言,通常的典范模型方法在许多情形都不奏效。本文将在Marti等人已有工作基础上,对带公共知识和分布式知识的直觉主义认知逻辑系统开展进一步研究,主要工作包括如下方面:1.在带分布式知识的直觉主义认知逻辑IDK的基础上,通过模型变换完成了刻画满足正向内省性的直觉主义分布式知识的公理系统IDS4的完备可靠性证明,并统一了IDK、IDT及IDS4的完备性证明。2.在直觉主义逻辑框架下同时处理公共知识和分布式知识,针对不同可达关系特性,建立了含分布式知识和公共知识的两个直觉主义认知逻辑公理系统ICDK和ICDT,通过对模型逐次变换构造了典范模型并给出了完备可靠性证明。