单调的时间分辨率
摘要：第一阶时态逻辑(FOTL)直到最近还很少被理解。虽然人们知道该逻辑没有有限的公理化，但之前还没有对该逻辑的片段进行更详细的分析。然而，Hodkinson等人的一项突破，确定了一个有限公理化的片段，称为monodic片段，从而改进了对FOTL的理解。然而，为了利用这些理论进展，有必要对monodic片段有适当的证明技巧。在本文中，我们修改和扩展了最初用于命题时态逻辑的子句时态推理技术，以使其适用于这些monodic片段。我们为FOTL中的公式开发了一个特定的正常形式，并为具有该形式的公式提供了一个完全的推理演算法。这种子句推理技术不仅可作为某些monodic类的实用证明技巧，而且使用这种方法可以增加对monodic片段的理解。具体而言，我们在这里展示了如何将monodic FOTL的几个特征作为子句时态推理方法的完备性结果的推论来建立。这包括定义新的可判定的monodic类，通过缩减简化现有的monodic类，以及在扩展域的monodic逻辑的情况下子句时态推理的完备性，这种情况在理论和实践中都非常重要。
作者：Anatoly Degtyarev, Michael Fisher, and Boris Konev
论文ID：cs/0306041
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2007-05-23