Finding resolution proofs and using duplicate goals in and/or trees. - James R. Slagle; Deena A. Koniver (Inf. Sci., 1971)