Stephen A. Cook
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.
- 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).Google Scholar
Cross Ref
- 2.S. A. Cook: Characterizations of Pushdown Machines in terms of Time-Bounded Computers. |J. Assoc. Computing Machinery,\ Vol. 18, No. 1, Jan. 1971, pp 4-18. Google ScholarDigital Library
- 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.Google Scholar
- 4.D. G. Corneil and C. C. Gotlieb: An Efficient Algorithm for Graph Isomorphism. J. Assoc Computing Machinery Vol. 17, No. 1, Jan. 1970, pp 51-64. Google ScholarDigital Library
- 5.M. Davis and H. Putnam: A Computing Procedure for Quantification Theory. J. Assoc. Computing Machinery, 1960, pp. 201-215. Google ScholarDigital Library
- 6.J. H. Bennett: On Spectra. Doctoral Dissertation, Princeton University, 1962.Google Scholar
- 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.Google Scholar
- 8.John Hopcroft and Jeffrey Ullman: Formal Languages and their Relation to Automata. Addison-Wesley, 1969. Google ScholarDigital Library
Index Terms
- The complexity of theorem-proving procedures
Recommendations
Theorem Proving Modulo
AbstractDeduction modulo is a way to remove computational arguments from proofs by reasoning modulo a congruence on propositions. Such a technique, issued from automated theorem proving, is of general interest because it permits one to separate ...
Comments