| 本文已被：浏览 4416次 下载 7290次 |
码上扫一扫！ |
|
|
| 正则模型类的时态可定义性 |
|
王善侠1,2, 马明辉1, 陈武3, 邓辉文1,3
|
|
1.西南大学 逻辑与智能研究中心, 重庆 400715;2.河南师范大学 计算机与信息工程学院, 河南 新乡 453007;3.西南大学 计算机与信息科学学院, 重庆 400715
|
|
| 摘要: |
| 正则模型是非正规模态逻辑的模型，通过定义正则模型的不相交并、C2t-互模拟、生成子模型、C2t-超滤扩张等模型上的运算，可以证明一个正则模型类在时态语言中可定义当且仅当它在不相交并、满C2t-互模拟像、C2t-超滤扩张下封闭，并且它的补类在C2t-超滤扩张下封闭.该刻画定理说明了时态语言在正则模型类上的表达力. |
| 关键词: 正则模型 时态语言 C2t-互模拟 C2t-超滤扩张 时态可定义性 |
| DOI：10.13328/j.cnki.jos.005208 |
| 分类号: |
| 基金项目:国家社会科学基金重大项目（14ZDB016） |
|
| Temporal Definability of Regular Model Classes |
|
WANG Shan-Xia1,2, MA Ming-Hui1, CHEN Wu3, DENG Hui-Wen1,3
|
|
1.Institute for Logic and Intelligence, Southwest University, Chongqing 400715, China;2.School of Computer and Information Engineering, Henan Normal University, Xinxiang 453007, China;3.School of Computer and Information Science, Southwest University, Chongqing 400715, China
|
| Abstract: |
| Regular models are models for non-normal modal logics. By defining some model operations, including disjoint union, C2t- bisimulation, generated submodel, and C2t-ultrafilter extension, this study proves that a class of regular models can be defined in the temporal language if and only if it is closed under disjoint unions, surjective C2t-bisimulations and C2t-ultrafilter extensions, while its complement is closed under ultrafilter extensions. This characterization theorem explains the expressive power of temporal language over regular models. |
| Key words: regular model temporal language C2t- bisimulation C2t- ultrafilter extension temporal definability |
