Theorem-Proving for Computers: Some Results on Resolution and Renaming

Abstract

It is shown that J. A. Robinson's P1—deduction is a special case of a large class of types of deduction by resolution, an optimum choice from which should be possible for any particular theorem to be proved. Some further results, based on the operation of renaming literals by means of their negations, are obtained and suggest an alternative approach to automatic deduction.