Decidable fragment of first-order temporal logics
Decidable fragment of first-order temporal logics
复制标题
DOI：
10.1016/s0168-0072(00)00018-x
复制
发表时间：
2000-12
期刊：
影响因子：
--
通讯作者：
I. Hodkinson;F. Wolter;M. Zakharyaschev
中科院分区：
文献类型：
--
作者：
I. Hodkinson;F. Wolter;M. Zakharyaschev
在本文中，我们引入了一种新的一阶时间语言片段，称为单片片段，其中所有以时间运算符（Since或Until）开头的公式至多有一个自由变量。我们证明了各种线性时间结构中一元公式的可满足性问题可以简化为经典一阶逻辑的某个片段的可满足性问题。然后，使用这种归约来挑选出一阶时序逻辑和二排序一阶逻辑的多个可判定片段，其中一种用于时序推理。除了标准的一阶时间结构外，我们还考虑那些只有有限一阶域的时间结构，并将上述结果扩展到有限域的时态逻辑。我们通过三种不同的方式证明可判定性：在预期的时间流上使用一元二阶逻辑的可判定性，通过对具有自然数时间的结构进行显式分析，以及通过在有限多个步骤中从片段构建模型的组合方法。
In this paper, we introduce a new fragment of the first-order temporal language, called the monodic fragment, in which all formulas beginning with a temporal operator (Since or Until) have at most one free variable. We show that the satisfiability problem for monodic formulas in various linear time structures can be reduced to the satisfiability problem for a certain fragment of classical first-order logic. This reduction is then used to single out a number of decidable fragments of first-order temporal logics and of two-sorted first-order logics in which one sort is intended for temporal reasoning. Besides standard first-order time structures, we consider also those that have only finite first-order domains, and extend the results mentioned above to temporal logics of finite domains. We prove decidability in three different ways: using decidability of monadic second-order logic over the intended flows of time, by an explicit analysis of structures with natural numbers time, and by a composition method that builds a model from pieces in finitely many steps.