Regressive Merging in Model Elimination Tableau-Based Theorem Provers. - Kevin Wallace; Graham Wrightson (Log. J. IGPL, 1995)