Anderson, Robert B.2022-06-282022-06-28197213678754https://hdl.handle.net/10657/10140Automatic 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.application/pdfenThis item is protected by copyright but is made available here under a claim of fair use (17 U.S.C. Section 107) for non-profit research and educational purposes. Users of this work assume the responsibility for determining copyright status prior to reusing, publishing, or reproducing this item for purposes other than what is allowed by fair use or other copyright exemptions. Any reuse of this item in excess of fair use or other copyright exemptions requires express permission of the copyright holder.Thesisreformatted digital