单调时间分辨率
Monodic temporal resolution
摘要：
直到最近，一阶时态逻辑（FOTL）还很少被理解。虽然众所周知，完整的逻辑没有有限的公理化，但以前没有对逻辑片段进行更详细的分析。然而，霍金森等人的一项突破，识别一个可公理化的片段，称为单音片段，已经导致了对FOTL的更好理解。然而，为了利用这些理论上的进步，重要的是要有适当的证明技术的单旋律片段。在本文中，我们修改和扩展的小句的时间分辨率技术，最初开发的命题时间逻辑，使其在这样的单调片段。我们开发了一个特定的范式的公式FOTL，并提供了一个完整的解决演算的公式在这种形式。这种分句解析技术不仅可以作为某些单音节类别的实用证明技术，而且这种方法的使用为我们提供了对单音节片段的更多理解。特别是，我们在这里展示了如何建立的单音FOTL的几个功能的子句时间分辨率方法的完整性结果的推论。这些包括新的可判定的单节类的定义，简化现有的单节类的减少，并在单节逻辑与扩展域的情况下，一个具有重要意义的情况下，在理论和实践中的子句时间分辨率的完整性。
英文摘要：
Until recently, First-Order Temporal Logic (FOTL) has been little understood. While it is well known that the full logic has no finite axiomatisation, a more detailed analysis of fragments of the logic was not previously available. However, a breakthrough by Hodkinson et.al., identifying a finitely axiomatisable fragment, termed the monodic fragment, has led to improved understanding of FOTL. Yet, in order to utilise these theoretical advances, it is important to have appropriate proof techniques for the monodic fragment. In this paper, we modify and extend the clausal temporal resolution technique, originally developed for propositional temporal logics, to enable its use in such monodic fragments. We develop a specific normal form for formulae in FOTL, and provide a complete resolution calculus for formulae in this form. Not only is this clausal resolution technique useful as a practical proof technique for certain monodic classes, but the use of this approach provides us with increased understanding of the monodic fragment. In particular, we here show how several features of monodic FOTL are established as corollaries of the completeness result for the clausal temporal resolution method. These include definitions of new decidable monodic classes, simplification of existing monodic classes by reductions, and completeness of clausal temporal resolution in the case of monodic logics with expanding domains, a case with much significance in both theory and practice.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
