摘要翻译：
本文给出了Horn事务逻辑（状态更新的常规Horn逻辑程序的推广）的有效计算算法。我们提出了两种互补的方法来优化事务逻辑的实现。第一种方法是基于列表的，我们将证明理论修改为基于状态的表调用和答案（实际上相当于动态规划）。呼叫应答表被索引到呼叫和进行呼叫的状态的签名。应答列包含应答统一和调用执行后的状态签名。使用基于尝试和计数的技术有效地对状态进行签名。第二种方法是基于增量计算的，它适用于数据oracle包含派生关系的情况。删除和插入（在transaction oracle中执行）会更改数据库的状态。使用惯性的启发式（响应基本更新，只有一部分状态发生变化），在大多数情况下，只计算状态中的变化比从头重新计算整个状态更便宜。这两种方法是互补的，因为第一种方法在相同状态下重复呼叫时优化评估，而第二种方法在未通过排线机制找到呼叫-状态对时优化新状态的评估（即第一种方法）。事务逻辑的证明理论在其模型理论方面是健全和完备的，它采用了表列和增量评价的方法。
---
英文标题：
《Efficient Tabling Mechanisms for Transaction Logic Programs》
---
作者：
Paul Fodor
---
最新提交年份：
2007
---
分类信息：

一级分类：Computer Science        计算机科学
二级分类：Logic in Computer Science        计算机科学中的逻辑
分类描述：Covers all aspects of logic in computer science, including finite model theory, logics of programs, modal logic, and program verification. Programming language semantics should have Programming Languages as the primary subject area. Roughly includes material in ACM Subject Classes D.2.4, F.3.1, F.4.0, F.4.1, and F.4.2; some material in F.4.3 (formal languages) may also be appropriate here, although Computational Complexity is typically the more appropriate subject area.
涵盖计算机科学中逻辑的所有方面，包括有限模型理论，程序逻辑，模态逻辑和程序验证。程序设计语言语义学应该把程序设计语言作为主要的学科领域。大致包括ACM学科类D.2.4、F.3.1、F.4.0、F.4.1和F.4.2中的材料；F.4.3（形式语言）中的一些材料在这里也可能是合适的，尽管计算复杂性通常是更合适的主题领域。
--
一级分类：Computer Science        计算机科学
二级分类：Artificial Intelligence        人工智能
分类描述：Covers all areas of AI except Vision, Robotics, Machine Learning, Multiagent Systems, and Computation and Language (Natural Language Processing), which have separate subject areas. In particular, includes Expert Systems, Theorem Proving (although this may overlap with Logic in Computer Science), Knowledge Representation, Planning, and Uncertainty in AI. Roughly includes material in ACM Subject Classes I.2.0, I.2.1, I.2.3, I.2.4, I.2.8, and I.2.11.
涵盖了人工智能的所有领域，除了视觉、机器人、机器学习、多智能体系统以及计算和语言（自然语言处理），这些领域有独立的学科领域。特别地，包括专家系统，定理证明（尽管这可能与计算机科学中的逻辑重叠），知识表示，规划，和人工智能中的不确定性。大致包括ACM学科类I.2.0、I.2.1、I.2.3、I.2.4、I.2.8和I.2.11中的材料。
--

---
英文摘要：
  In this paper we present efficient evaluation algorithms for the Horn Transaction Logic (a generalization of the regular Horn logic programs with state updates). We present two complementary methods for optimizing the implementation of Transaction Logic. The first method is based on tabling and we modified the proof theory to table calls and answers on states (practically, equivalent to dynamic programming). The call-answer table is indexed on the call and a signature of the state in which the call was made. The answer columns contain the answer unification and a signature of the state after the call was executed. The states are signed efficiently using a technique based on tries and counting. The second method is based on incremental evaluation and it applies when the data oracle contains derived relations. The deletions and insertions (executed in the transaction oracle) change the state of the database. Using the heuristic of inertia (only a part of the state changes in response to elementary updates), most of the time it is cheaper to compute only the changes in the state than to recompute the entire state from scratch. The two methods are complementary by the fact that the first method optimizes the evaluation when a call is repeated in the same state, and the second method optimizes the evaluation of a new state when a call-state pair is not found by the tabling mechanism (i.e. the first method). The proof theory of Transaction Logic with the application of tabling and incremental evaluation is sound and complete with respect to its model theory.
---
PDF链接：
https://arxiv.org/pdf/0709.1699