Loveland, D. W. (1968) . Journal of the ACM, 15, 236—251.

Mechanical theorem-proving by model elimination