The complexity of theorem-proving procedures

ABSTRACT

It is shown that any recognition problem solved by a polynomial time-bounded nondeterministic Turing machine can be “reduced” to the problem of determining whether a given propositional formula is a tautology. Here “reduced” means, roughly speaking, that the first problem can be solved deterministically in polynomial time provided an oracle is available for solving the second. From this notion of reducible, polynomial degrees of difficulty are defined, and it is shown that the problem of determining tautologyhood has the same polynomial degree as the problem of determining whether the first of two given graphs is isomorphic to a subgraph of the second. Other examples are discussed. A method of measuring the complexity of proof procedures for the predicate calculus is introduced and discussed.

REFERENCES

• 1: D. L. Kreider and R. W. Ritchie: Predictably Computable Functionals and Definitions by Recursion. Zeitschrift für math. Logik und Grundlagen der Math., Vol. 10, 65-80 (1964).
• 2: Stephen A. Cook, Characterizations of Pushdown Machines in Terms of Time-Bounded Computers, Journal of the ACM (JACM), v.18 n.1, p.4-18, Jan. 1971 [doi>10.1145/321623.321625]
• 3: Cobham, Alan: The intrinsic computational difficulty of functions. Proc. of the 1964 International Congress for Logic, Methodology, and the Philosophy of Science, North Holland Publishing Co., Amsterdam, pp. 24-30.
• 4: D. G. Corneil , C. C. Gotlieb, An Efficient Algorithm for Graph Isomorphism, Journal of the ACM (JACM), v.17 n.1, p.51-64, Jan. 1970 [doi>10.1145/321556.321562]
• 5: 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]
• 6: J. H. Bennett: On Spectra. Doctoral Dissertation, Princeton University, 1962.
• 7: Hao Wang: Dominoes and the AEA case of the decision problems. Proc. of the Symposium on Mathematical Theory of Automata, at Polytechnic Institute of Brooklyn, 1962. pp. 23-55.
• 8: John E. Hopcroft , Jeffrey D. Ullman, Formal languages and their relation to automata, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1969

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.2 ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY
      F.2.2 Nonnumerical Algorithms and Problems
          Subjects: Complexity of proof procedures

Additional Classification:
  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
      F.1.1 Models of Computation
          Subjects: Bounded-action devices (e.g., Turing machines, random access machines)
      F.1.3 Complexity Measures and Classes
          Subjects: Reducibility and completeness

General Terms:
Theory