avatar avatar 我的文献 Stit逻辑的判定问题 作者 张炎 单位 武汉大学 关键词 Stit 逻辑; Agency逻辑; 时态逻辑; 认知逻辑; 滤模型; 拟模型; 解释
摘要
在这篇论文中,我们讨论若干stit逻辑的判定问题。这些逻辑的语言中除了stit算子,还包括时态算子、历史必然算子与知识算子等。本文获得三个主要结论。第一个主要结论是以非决定论的X,Y-时态逻辑为基础的某一类逻辑的可判定性。为了得出这一结论,我们使用子模型和滤模型的方法证明该类逻辑都具有强有穷框架性。这一结论可以被应用于许多具体的逻辑,其中包含我们所关心的结合agency、时态及认知的逻辑,不过语言中的时态算子只能有X(下一步)和Y(上一步)。本文得出的第二个主要结论是包含时态算子U(到…为止)和S(从…以来)、历史必然算子及cstit算子的逻辑的可判定性。我们证明基于离散的时间结构的stit框架的两个子类决定的逻辑是可判定的。在建立这个结果的证明中,我们使用拟模型和解释的技巧,先把模态公式的可满足性问题转换为拟模型存在性问题,再借助Rabin定理证明拟模型存在性问题是可判定的。本文得出的第三个主要结论是包含多个astit算子的astit逻辑的可判定性。我们证明astit框架类的两个子类决定的astit逻辑的都是可判定的。这两个子类分别是不包含有界的无穷选择链的带族astit框架类和不包含有界的无穷选择链的全族astit框架类。与上述第二个主要结论的证明类似,我们使用拟模型和解释的方法证明这两个子类决定的逻辑都是可判定的。除此之外,我们还得出这两个子类决定的逻辑是相同的。
下载 cnki {{liketext}}
©2020 - iData {{ message }} 关闭