基于破坏性表列的模态公理系统

摘要：

表列适于作为模态定理机器证明的基础.在破坏性模态表列的基础上,构造分析性模态公理系统,这种公理系统的定理很容易证明,因此也适于作为模态定理机器证明的基础.沿着安德森等人开创的方向,将分析性公理系统的应用从经典逻辑推广到模态逻辑.称一个公理系统是分析的,即它的每一推理规则的前提和结论中的命题变元相同.为了便于表述这种系统中的公理,可以先定义一种广义谢弗竖M,给出模态表达式的一种新记法,以此改进现有的破坏性模态表列,并以这种改进的结果为基础构造分析性模态公理系统.

关键词：语义表列、模态逻辑、完全性、证明理论、谢弗竖

所属期刊栏目：12

分类号：B815.1(逻辑学(论理学))

在线出版日期：2009-04-15（万方平台首次上网日期，不代表论文的发表时间）

页数：共5页

页码：41-45