|
软件学报 2015
具有模态词□φ=□1v□2φ且可靠与完备的公理系统DOI: 10.13328/j.cnki.jos.004748, PP. 2286-2296 Abstract: 提出具有模态词□φ=□1v□2φ的命题模态逻辑,给出其语言、语法与语义,其公理化系统是可靠与完备的,其中,□1与□2是给定的模态词.该逻辑的公理化系统具有与公理系统s5相似的语言,但具有不同的语法与语义.对于任意的公式φ,□φ=□1v□2φ;框架定义为三元组w,r1,r2,模型定义为四元组w,r1,r2,i;在完备性定理证明过程中,需要在由所有极大协调集所构成的集合上构造出两个等价关系,其典型模型的构建方法与经典典型模型的构建方法不同.如果□1的可达关系r1等于□2的可达关系r2,那么该逻辑的公理化系统变成s5.
|