Labelled splitting
Labelled splitting
复制标题
DOI：
10.1007/s10472-009-9150-9
复制
发表时间：
2009-02-01
影响因子：
1.2
通讯作者：
Weidenbach, Christoph
中科院分区：
文献类型：
--
作者：
Fietzke, Arnaud;Weidenbach, Christoph
我们在标号子句的基础上定义了一个显式分裂的迭加演算。我们第一次展示了一个具有显式的非时间顺序回溯规则的叠加演算，它是合理和完整的。新的回溯规则使用Spass已知的分支凝聚推进回溯。对新规则实现的实验评估表明，它比以前的SPASS分裂实现有了很大的改进。最后，我们讨论了标记一阶分裂和DPLL风格分裂与智能回溯和子句学习的关系。
We define a superposition calculus with explicit splitting on the basis of labelled clauses. For the first time we show a superposition calculus with an explicit non-chronological backtracking rule sound and complete. The new backtracking rule advances backtracking with branch condensing known from SPASS. An experimental evaluation of an implementation of the new rule shows that it improves considerably on the previous SPASS splitting implementation. Finally, we discuss the relationship between labelled first-order splitting and DPLL style splitting with intelligent backtracking and clause learning.