A study of SL-resolution for automatic theorem-proving

Automatic theorem-proving by resolution was first proposed by J. A. Robinson in 1965. Since then, quite a number of restricted versions of resolution have been proposed all with the aim of providing more efficient proof procedures. In this paper, SL-resolution - linear resolution with selection function - recently proposed by Kowalski and Keuhner, is studied. A version of SL-resolution was implemented by means of a LISP program, and its efficiency tested on a number of examples. In the original paper, a long and tedious proof for the completeness of this inference system was given. A more elegant proof is given here, using the basic technique developed by Anderson and Bledsoe.