# A Curiously Effective Backtracking Strategy for Connection Tableaux

arXiv: https://arxiv.org/abs/2106.13722 · HTML: https://mlsanity.com/paper/2106.13722/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 25 Jun 2021.

## Built on by (most cited first, 2 of 2)

- [Imitation Learning for Connection-Tableau Construction](https://mlsanity.com/paper/2608.26009/) (2026)
- [Reset Early, Reset Often, Eliminate Models](https://mlsanity.com/paper/2610.18204/) (2026)

## Abstract (arXiv)

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.