Controlling Deduction with Proof Condensation and Heuristics. - Franz Oppacher; E. Suen (CADE, 1986)

HARP: A Tableau-Based Theorem Prover. - Franz Oppacher; E. Suen (J. Autom. Reason., 1988)