Browsing by Author "Au Yeung Woon Chi, Mary"
Now showing 1 - 1 of 1
- Results Per Page
- Sort Options
Item A study of SL-resolution for automatic theorem-proving(1972) Au Yeung Woon Chi, Mary; Anderson, Robert B.; Huang, Jung-Chang; Schmidt, JürgenAutomatic 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.