Reset Early, Reset Often, Eliminate Models

Martin S. Fixman, Fredrik Rømming, Sean B. Holden

Connection-tableau provers typically construct closed tableaux by backtracking search. This gives lightweight proof procedures, but their low-memory search state leaves little deri…