Relationship between Tactics of the Inverse Method and the Resolution Method

Abstract

Of the theorem-proving (deducibility-establishing) methods used in recent years with orientation toward the synthesis of machine algorithms and programs, the resolution method proposed in 1964 by J. A. Robinson [1,2] has gained the greatest reputation and enjoyed the most theoretical development. Concurrently and independently, the present author proposed the so-called “inverse method”, which is also designed for the automation of theorem proving [3,4,5]. The domain of applicability of the inverse method is wider, but in application to the same calculus (the classical predicate calculus with function symbols) and to the same standardization of the initial formulas as the resolution method it is very convenient to compare and interfuse the two methods. The purpose of the present article is to establish a relationship between the methods whereby it will be possible to transfer the results obtained by one method to the other (we are thinking by and large in terms of results bearing on the completeness of particular deducibility-establishing tactics).