Robinson, J. Alan. A Machine-Oriented Logic Based on the Resolution Principle. Journal of the ACM. 1965, 12 (1): 23–41. doi:10.1145/321250.321253.
Leitsch, Alexander. The Resolution Calculus. Springer. 1997.
Gallier, Jean H. Logic for Computer Science: Foundations of Automatic Theorem Proving. Harper & Row Publishers. 1986.
Lee, Chin-Liang Chang, Richard Char-Tung. Symbolic logic and mechanical theorem proving reprint. San Diego: Academic Press. 1987. ISBN 0-12-170350-9.
Approaches to non-clausal resolution, i.e. resolution of first-order formulas that need not be in clausal normal form, are presented in:
D. Wilkins. QUEST — A Non-Clausal Theorem Proving System (Master's Thesis). Univ. of Essex, England. 1973.
Neil V. Murray. A Proof Procedure for Quantifier-Free Non-Clausal First Order Logic (Technical report). Syracuse Univ. Feb 1979. 2-79. (Cited from Manna, Waldinger, 1980 as: "A Proof Procedure for Non-Clausal First-Order Logic", 1978)
Zohar Manna, Richard Waldinger. A Deductive Approach to Program Synthesis. ACM Transactions on Programming Languages and Systems. Jan 1980, 2: 90–121. doi:10.1145/357084.357090. A preprint appearead in Dec 1978 as SRI Technical Note 177
N. V. Murray. Completely Non-Clausal Theorem Proving. Artificial Intelligence. 1982, 18: 67–85. doi:10.1016/0004-3702(82)90011-x.