A Maeh ine-Or lented Log ic Based on the Reso lu t ion P r inc ip le

:tb.~tract. Theorem-proving on the computer, using procedures based on the fund~-mental theorem of Herbrand concerning the first-order predicate tdeulus, is examined with ~ view towards improving the efticieney and widening the range of practical applicability of these procedures. A elose analysis of the process of substitution (of terms for variables), and the process of truth-functional analysis of the results of such substitutions, reveals that both processes can be combined into a single new process (called resolution), iterating which is vastty more ef[ieient han the older cyclic procedures consisting of substitution stages alternating with truth-functional analysis stages. The theory of the resolution process is presented in the form of a system of first<~rder logic with.just one inference principle (the resolution principle). The completeness of the system is proved; the simplest proof-procedure based oil the system is then the direct im-plementation of the proof of completeness. Howew~r, this procedure is quite inefficient, ~nd the paper concludes with a discussion of several principles (called search principles) which are applicable to the design of efficient proof-procedures mploying resolution as the basle logical process