Automatic Theorem Proving With Renamable and Semantic Resolution

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 unsatisfiable set of nonempty clauses and if M is a ground model, then there exists an unresolved maximal semantic clash [E1, E2, · · ·, Eq, 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.

REFERENCES

• 1: Martin Davis , Hilary Putnam, A Computing Procedure for Quantification Theory, Journal of the ACM (JACM), v.7 n.3, p.201-215, July 1960 [doi>10.1145/321033.321034]
• 2: ----, Eliminating the irrelevant from mechanical proofs. Proc. 15th Symp. in Appl. Math., Amer. Math. Soc., Providence, R. I., 1963, pp. 15-30.
• 3: Edward A. Feigenbaum , Julian Feldman, Computers and Thought, McGraw-Hill, Inc., New York, NY, 1963
• 4: H. Gelernter, Realization of a geometry-theorem proving machine, Computers & thought, MIT Press, Cambridge, MA, 1995
• 5: ----, 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.)
• 6: GILMORZ, P. C. A program for the production of proofs for theorems derivable within the first order predicate calculus from axiome. Proc. Int. Conf. on Information Processing, UNESCO House, paris, 1959.
• 7: MCCARTHY, J. Programs with common sense. Proc. Conf. on Mechanization of Thought Processes. English National Physical Laboratory, Teddington, Middlesex, England, 1959.
• 8: MELTZER, B. Theorem proving for computers:some results on resolution and renaming Computer J. 8 (1966), 341-343.
• 9: Allen Newell , J. C. Shaw , H. A. Simon, Empirical explorations with the logic theory machine: a case study in heuristics, Computers & thought, MIT Press, Cambridge, MA, 1995
• 10: REYNOLDS, J. Unpublished seminar notes. Stanford University, Palo Alto. Calif. fall 1965.
• 11: J. A. Robinson, A Machine-Oriented Logic Based on the Resolution Principle, Journal of the ACM (JACM), v.12 n.1, p.23-41, Jan. 1965 [doi>10.1145/321250.321253]
• 12: ----, Automatic deduction with hyper-resolution Int. J. Computer Math. 1 (1965), 227- 234.
• 13: ----, A review of automatic theorem proving. Proc. Symp. in Appl. Math. Amer. Math. Soc., Providence, R. I., 1967.
• 14: SLAGLE, J. R. A multipurpose, theorem proving, heuristic program that learns. Information Processing 1965, Proc. IFIP Congress 1965, Vol. 2, pp. 323-324.
• 15: ----, A proposed preference strategy using sufficiency resolution for answering questions. UCRL-14361, Lawrence Radiation Lab., Livermore, Calif., Aug., 1965.
• 16: James R. Slagle, Experiments with a deductive question-answering program, Communications of the ACM, v.8 n.12, p.792-798, Dec. 1965 [doi>10.1145/365691.365960]
• 17: WANG, H. Formalization and automatic theorem proving. Information Processing 1965, Proc. IFIP Congress 1965, Vol. 1, pp. 51-58.
• 18: 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.
• 19: Lawrence Wos , George A. Robinson , Daniel F. Carson, Efficiency and Completeness of the Set of Support Strategy in Theorem Proving, Journal of the ACM (JACM), v.12 n.4, p.536-541, Oct. 1965 [doi>10.1145/321296.321302]

INDEX TERMS

Primary Classification:
  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE

Additional Classification:
  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
      F.1.3 Complexity Measures and Classes
          Subjects: Reducibility and completeness

General Terms:
Design, Languages, Theory, Verification