Automated proof search with connection tableaux, such as implemented by Otten's leanCoP prover, depends on backtracking for completeness. Otten's restricted backtracking strategy loses completeness, yet for many problems, it significantly reduces the time required to find a proof. I introduce a new, less restricted backtracking strategy based on the notion of exclusive cuts. I implement the strategy in a new prover called meanCoP and show that it greatly improves upon the previous best strategy in leanCoP.

翻译：基于连接Tableaux的自动证明搜索（如Otten的leanCoP证明器所实现）依赖于回溯来实现完备性。Otten的受限回溯策略虽丧失完备性，但对许多问题而言，它能显著缩短找到证明所需的时间。本文提出一种基于独占切割概念的新型非受限制回溯策略，并在新证明器meanCoP中加以实现。实验表明，该策略在leanCoP中显著优于先前最优策略。