Abstract
The theory of J. A. Robinson’s resolution principle, an inference rule for first-order predicate calculus, is unified and extended. A theorem-proving computer program based on the new theory is proposed and the proposed semantic resolution program is compared with hyper-resolution and set-of-support resolution programs. Renamable and semantic resolution are defined and shown to be identical. Given a model M, semantic resolution is the resolution of a latent clash in which each “electron” is at least sometimes false under M; the nucleus is at least sometimes true under M.
The completeness theorem for semantic resolution and all previous completeness theorems for resolution (including ordinary, hyper-, and set-of-support resolution) can be derived from a slightly more general form of the following theorem. If U is a finite, truth-functionally un-satisfiable set of nonempty clauses and if M is a ground model, then there exists an unresolved maximal semantic clashE 1 , E 2 , ..., E q , C with nucleus C such that any set containing C and one or more of the electrons E1, E2, ..., Eq is an unresolved semantic clash in U.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Davis, M., and Putnam, H. A computing procedure for quantification theory. J. ACM 7 (1960), 201–215.
Davis, M., and Putnam, H. Eliminating the irrelevant from mechanical proofs. Proc. 15th Symp. in Appl. Math., Amer. Math. Soc., Providence, R. I., 1963, pp. 15–30.
Feigenbaum, E., and Feldman, J. (Eds.). Computers and Thought. McGraw-Hill, New York, 1963.
Gelernter, H. Realization of a geometry theorem proving machine. Proc. Int. Conf. on Information Processing, UNESCO House, Paris, 1959, pp. 273–282. (Reprinted in [3], pp. 134–152.)
Gelernter, H., Hansen, J. R., and Loveland, D. W. Empirical explorations of the geometry theorem machine. Proc. 1960 Western Joint Comput. Conf., Vol. 17, pp. 143–147. (Reprinted in [3], pp. 153–163.)
Gilmore, P. C. A program for the production of proofs for theorems derivable within the first order predicate calculus from axioms. Proc. Int. Conf. on Information Processing, UNESCO House, Paris, 1959.
Mccarthy, J. Programs with common sense. Proc. Conf. on Mechanization of Thought Processes. English National Physical Laboratory, Teddington, Middlesex, England, 1959.
Meltzer, B. Theorem proving for computers: some results on resolution and renaming. Computer J. 8 (1966), 341–343.
Newell, A., Shaw, J. C., and Simon, H. Empirical explorations of the logic theory machine, a case study in heuristic. Proc. 1957 Western Joint Comput. Conf., Vol. 11, pp. 218–230. (Reprinted in [3], pp. 109–133.)
Reynolds, J. Unpublished seminar notes. Stanford University, Palo Alto, Calif., fall 1965.
Robinson, J. A. A machine-oriented logic based on the resolution principle. J. ACM 12,1 (Jan. 1965), 23–41.
Robinson, J. A.. Automatic deduction with hyper-resolution. Int. J. Computer Math. 1 (1965), 227–234.
Robinson, J. A.. A review of automatic theorem proving. Proc. Symp. in Appl. Math., Amer. Math. Soc., Providence, R. I., 1967.
Slagle, J. R. A multipurpose, theorem proving, heuristic program that learns. Information Processing 1965, Proc. IFIP Congress 1965, Vol. 2, pp. 323–324.
Slagle, J. R.. A proposed preference strategy using sufficiency resolution for answering questions. UCRL-14361, Lawrence Radiation Lab., Livermore, Calif., Aug. 1965.
Slagle, J. R.. Experiments with a deductive, question-answering program. Comm. ACM 8 (Dec. 1965), 792–798.
Wang, H. Formalization and automatic theorem proving. Information Processing 1965, Proc. IFIP Congress 1965, Vol. 1, pp. 51–58.
Wos, L., Carson, D. F., and Robinson, G. A. The unit preference strategy in theorem proving. Proc. AFIPS 1964 Fall Joint Comput. Conf., Vol. 26, pp. 616–621.
Wos, L., Robinson, G. A., and Carson, D. F. Efficiency and completeness of the set of support strategy in theorem proving. J. ACM 12, 4 (Oct. 1965), 536–541.
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1967 Association for Computing Machinery, Inc.
About this chapter
Cite this chapter
Slagle, J.R. (1967). Automatic Theorem Proving With Renamable and Semantic Resolution. 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_4
Download citation
DOI: https://doi.org/10.1007/978-3-642-81955-1_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-81957-5
Online ISBN: 978-3-642-81955-1
eBook Packages: Springer Book Archive