Reset Early, Reset Often, Eliminate Models.

arXiv:2610.18204v1 Announce Type: cross Abstract: Connection-tableau provers typically construct closed tableaux by backtracking search. This gives lightweight proof procedures, but their low-memory search state leaves little derived information to reuse after