A Curiously Effective Backtracking Strategy for Connection Tableaux

TL;DR

This paper introduces a new backtracking strategy for connection tableaux proof search that balances completeness and efficiency, significantly improving proof search times in the meanCoP prover.

Contribution

A novel backtracking strategy based on exclusive cuts is proposed and implemented, enhancing proof search efficiency while maintaining near-completeness.

Findings

MeanCoP outperforms leanCoP with previous strategies

Significant reduction in proof search time

Strategy maintains high proof success rate

Abstract

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.