SOLAR: An automated deduction system for consequence finding
SOLAR: An automated deduction system for consequence finding
复制标题
DOI：
10.3233/aic-2010-0465
复制
发表时间：
2010-04
期刊：
影响因子：
--
通讯作者：
Hidetomo Nabeshima;K. Iwanuma;Katsumi Inoue;O. Ray
中科院分区：
文献类型：
--
作者：
Hidetomo Nabeshima;K. Iwanuma;Katsumi Inoue;O. Ray
SOLAR （SOL for Advanced Reasoning）是一个基于SOL （Skip Ordered Linear）表演算的一阶子句推理系统。发现公理集的非平凡结果的能力在人工智能的许多应用中都很有用，例如定理证明，查询回答和非单调推理。SOL是一种连接表演算，用于发现子句理论的非包含结果。SOLAR是SOL的一种有效实现，它使用几种方法来修剪搜索空间的冗余分支。本文介绍了在SOLAR中实现的一些关键修剪和控制策略，并展示了它们在一系列基准问题上的有效性。
SOLAR (SOL for Advanced Reasoning) is a first-order clausal consequence finding system based on the SOL (Skip Ordered Linear) tableau calculus. The ability to find non-trivial consequences of an axiom set is useful in many applications of Artificial Intelligence such as theorem proving, query answering and nonmonotonic reasoning. SOL is a connection tableau calculus which is complete for finding the non-subsumed consequences of a clausal theory. SOLAR is an efficient implementation of SOL that employs several methods to prune away redundant branches of the search space. This paper introduces some of the key pruning and control strategies implemented in SOLAR and demonstrates their effectiveness on a collection of benchmark problems.