正则模型类的时态可定义性

来源：软件学报杂志2017年第5期北京时间：

作者：王善侠,马明辉,陈武,邓辉文

单位：王善侠，西南大学 逻辑与智能研究中心, 重庆 400715;河南师范大学 计算机与信息工程学院, 河南 新乡 45300711,马明辉，西南大学 逻辑与智能研究中心, 重庆 40071502,陈武，西南大学 计算机与信息科学学院, 重庆 40071503,邓辉文，西南大学 逻辑与智能研究中心, 重庆 400715;西南大学 计算机与信息科学学院, 重庆 40071504

摘要：正则模型是非正规模态逻辑的模型，通过定义正则模型的不相交并、C2t-互模拟、生成子模型、C2t-超滤扩张等模型上的运算，可以证明一个正则模型类在时态语言中可定义当且仅当它在不相交并、满C2t-互模拟像、C2t-超滤扩张下封闭，并且它的补类在C2t-超滤扩张下封闭.该刻画定理说明了时态语言在正则模型类上的表达力.

关键词：正则模型;时态语言;C2t_-互模拟;C2t_-超滤扩张;时态可定义性

基金资助：国家社会科学基金重大项目（14ZDB016）