Towards the implementation of first-order temporal resolution: the expanding domain case
Towards the implementation of first-order temporal resolution: the expanding domain case
复制标题
实现一阶时间分辨率：扩展域情况
DOI：
--
复制
发表时间：
2003
期刊：
影响因子：
--
通讯作者：
U. Hustadt
中科院分区：
文献类型：
--
作者：
B. Konev;A. Degtyarev;C. Dixon;Michael Fisher;U. Hustadt
一阶时态逻辑是一种简洁而强大的符号，在计算机科学和人工智能中都有许多潜在的应用。虽然完整的逻辑是高度复杂的，但最近关于一阶一阶时态逻辑的工作已经确定了重要的可列举甚至可判定的片段。本文针对扩域上一阶时态逻辑的单周期片段，提出了一种子句归结方法。我们首先定义了一元公式的范式，然后引入了可以应用于该范式的公式的新的归结演算。我们陈述了该方法的正确性和完备性结果。我们用一个综合的例子说明了该方法。该方法基于经典的一阶分辨率，因此可以有效地实现。
First-order temporal logic is a concise and powerful notation, with many potential applications in both Computer Science and Artificial Intelligence. While the full logic is highly complex, recent work on monodic first-order temporal logics has identified important enumerable and even decidable fragments. In this paper, we develop a clausal resolution method for the monodic fragment of first-order temporal logic over expanding domains. We first define a normal form for monodic formulae and then introduce novel resolution calculi that can be applied to formulae in this normal form. We state correctness and completeness results for the method. We illustrate the method on a comprehensive example. The method is based on classical first-order resolution and can, thus, be efficiently implemented.