Labelled splitting

摘要

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.