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).
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
Literature Cited
J.A. Robinson, “A machine-oriented logic based on the resolution principle,” J. Assoc. Comput. Mach., 12 (1): 23–41 (1965).
J.A. Robinson, “A review of automatic theorem proving,” Proc. Sympos. Appl. Math., Amer. Math. Soc., 19: 1–18 (1967).
S.Yu. Maslov, “An inverse method of establishing deducibility in the classical predicate calculus,” Dokl. Akad. Nauk SSSR, 159 (1): 17–20 (1964).
S.Yu. Maslov, “Application of the inverse method of establishing deducibility to the theory of decidable fragments of the classical predicate calculus,” Dokl. Akad. Nauk SSSR, 171 (6): 1282–1285 (1966).
S.Yu. Maslov, “An inverse method of establishing deducibility for logical calculi,” Trudy Matem. Inst. AN SSSR, 98: 26–87 (1968).
J.R. Slagle, “Automatic theorem proving with renamable and semantic resolution,” J. Assoc. Comput. Mach., 14 (4): 687–697 (1967).
G.S. Tseitin, “On the complexity of derivation in propositional calculus,” Seminars in Mathematics, Vol. 8, Consultants Bureau, New York (1970), pp. 115–125.
L. Wos, D. Carson, and G.A. Robinson, “The unit preference strategy in theorem proving,” AFIPS, Conf. Proc., 26: 615–621 (1964).
S.Yu Maslov, “Deduction-search tactics based on unification of the order of members in favorable assemblages,” this volume, p. 64.
P.B. Andrews, “Resolution with merging,” J. Assoc. Comput. Mach., 15 (3): 367–381 (1968).
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1983 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Maslov, S.Y. (1983). Relationship between Tactics of the Inverse Method and the Resolution Method. In: Siekmann, J.H., Wrightson, G. (eds) Automation of Reasoning. Symbolic Computation. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-81955-1_16
Download citation
DOI: https://doi.org/10.1007/978-3-642-81955-1_16
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-81957-5
Online ISBN: 978-3-642-81955-1
eBook Packages: Springer Book Archive