Comparison of Natural Deduction and Locking Resolution Implementations. - Steven Greenbaum; A. Nagasaka; Paul O'Rorke; David A. Plaisted (CADE, 1982)

The Illinois Prover: A General Purpose Resolution Theorem Prover. - Steven Greenbaum; David A. Plaisted (CADE, 1986)

A Structure-Preserving Clause Form Translation. - David A. Plaisted; Steven Greenbaum (J. Symb. Comput., 1986)

Input Transformations and Resolution Implementation Techniques for Theorem Proving in First-Order Logic (Clause Form, Discrimination Networks, Heuristic Search, Locking Resolution) - Steven Greenbaum (1986)