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

摘要

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