Automated Deduction - CADE-24
Automated Deduction - CADE-24
复制标题
自动扣除 - CADE-24
DOI：
10.1007/978-3-642-38574-2_33
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
Hoder K
中科院分区：
文献类型：
--
作者：
Hoder K
通常情况下，一阶问题包含命题变量，并且证明搜索会生成许多子句，这些子句可以分成具有不相交变量集的组件。对于来自某些应用程序的问题尤其如此，其中问题中出现了许多基本文字，甚至生成了更多。到目前为止，处理此类子句的问题已经通过使用带回溯的拆分（如在 Spass [14] 中）或不带回溯的拆分（如在 Vampire [7] 中）来解决。然而，文献[6]中描述的唯一广泛的实验表明，平均而言，使用分裂解决的问题较少，但也有一些问题只能使用分裂来解决。我们试图找出有助于分辨率定理证明器处理分裂效率的基本问题，并通过处理分裂的新选项、算法和数据结构增强了定理证明器 Vampire。本文描述了这些选项、算法和数据结构，并在 TPTP 库 [12] 上进行的大量实验中分析了它们的性能。本文的另一个贡献是微积分将命题推理与一阶推理分开。
It is often the case that first-order problems contain propositional variables and that proof-search generates many clauses that can be split into components with disjoint sets of variables. This is especially true for problems coming from some applications, where many ground literals occur in the problems and even more are generated.The problem of dealing with such clauses has so far been addressed using either splitting with backtracking (as in Spass [14]) or splitting without backtracking (as in Vampire [7]). However, the only extensive experiments described in the literature [6] show that on the average using splitting solves fewer problems, yet there are some problems that can be solved only using splitting.We tried to identify essential issues contributing to efficiency in dealing with splitting in resolution theorem provers and enhanced the theorem prover Vampire with new options, algorithms and datastructures dealing with splitting. This paper describes these options, algorithms and datastructures and analyses their performance in extensive experiments carried out over the TPTP library [12]. Another contribution of this paper is a calculusReProseparating propositional reasoning from first-order reasoning.