发帖
雷达卡
摘要翻译：
基于饱和度的推理方法是目前理论上发展最快的一种推理方法，也是大多数最先进的一阶逻辑推理方法所采用的一种推理方法。在过去的十年里，这类系统的性能有了急剧的提高，我把这归因于先进演算的使用和对实现技术的加强研究。然而，如今我们正在目睹性能进步的放缓，这可能被认为是基于饱和的技术正在达到其固有极限的标志。我在本文中试图提出的立场是，这种怀疑还为时过早，通过采用新的饱和架构原则，性能可能会得到大幅改善。基于饱和定理的顶级算法和相应的设计至少有两个固有的缺陷：所使用的推理选择机制不够灵活，以及缺乏智能排序搜索方向的手段。在这份立场文件中，我分析了这些缺点，并就如何克服这些缺点提出了两个想法。特别是，我提出了一个灵活的低成本高精度的推理选择机制，旨在克服与当前使用的基于子句选择的过程实例相关的问题。本文还提出了一种基于搜索空间的搜索方向智能排序方法。我讨论了与实现所建议的体系结构原则相关的一些技术问题，并概述了可能的解决方案。
---
英文标题：
《New Implementation Framework for Saturation-Based Reasoning》
---
作者：
Alexandre Riazanov
---
最新提交年份：
2008
---
分类信息：
一级分类：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中的材料。
--
一级分类：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（形式语言）中的一些材料在这里也可能是合适的，尽管计算复杂性通常是更合适的主题领域。
--
---
英文摘要：
The saturation-based reasoning methods are among the most theoretically developed ones and are used by most of the state-of-the-art first-order logic reasoners. In the last decade there was a sharp increase in performance of such systems, which I attribute to the use of advanced calculi and the intensified research in implementation techniques. However, nowadays we are witnessing a slowdown in performance progress, which may be considered as a sign that the saturation-based technology is reaching its inherent limits. The position I am trying to put forward in this paper is that such scepticism is premature and a sharp improvement in performance may potentially be reached by adopting new architectural principles for saturation. The top-level algorithms and corresponding designs used in the state-of-the-art saturation-based theorem provers have (at least) two inherent drawbacks: the insufficient flexibility of the used inference selection mechanisms and the lack of means for intelligent prioritising of search directions. In this position paper I analyse these drawbacks and present two ideas on how they could be overcome. In particular, I propose a flexible low-cost high-precision mechanism for inference selection, intended to overcome problems associated with the currently used instances of clause selection-based procedures. I also outline a method for intelligent prioritising of search directions, based on probing the search space by exploring generalised search directions. I discuss some technical issues related to implementation of the proposed architectural principles and outline possible solutions.
---
PDF链接：
https://arxiv.org/pdf/0802.2127
京公网安备 11010802022788号
