Get 20M+ Full-Text Papers For Less Than $1.50/day. Start a 14-Day Trial for You or Your Team.

Learn More →

The complexity of theorem-proving procedures

The complexity of theorem-proving procedures The Complexity of Theorem-Proving Procedures Stephen A. Cook University of Toronto Summary It is shown that any recognition problem solved by a polynomial timebounded 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. Throughout this paper, a set of strings means a set of strings o n some fixed, large, finite alphabet Z. This alphabet is large enough to include symbols for all sets described here. All Turing machines are deterministic recognition devices, unless the contrary is explicitly stated. i. Tautologies and Polynomial ReReducibility. Let us fix a formalism for the propositional calculus in which formulas http://www.deepdyve.com/assets/images/DeepDyve-Logo-lg.png

The complexity of theorem-proving procedures

Association for Computing Machinery — May 3, 1971

Loading next page...
/lp/association-for-computing-machinery/the-complexity-of-theorem-proving-procedures-0a9Vy8kiAF

References

References for this paper are not available at this time. We will be adding them shortly, thank you for your patience.

Datasource
Association for Computing Machinery
Copyright
Copyright © 1971 by ACM Inc.
doi
10.1145/800157.805047
Publisher site
See Article on Publisher Site

Abstract

The Complexity of Theorem-Proving Procedures Stephen A. Cook University of Toronto Summary It is shown that any recognition problem solved by a polynomial timebounded 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. Throughout this paper, a set of strings means a set of strings o n some fixed, large, finite alphabet Z. This alphabet is large enough to include symbols for all sets described here. All Turing machines are deterministic recognition devices, unless the contrary is explicitly stated. i. Tautologies and Polynomial ReReducibility. Let us fix a formalism for the propositional calculus in which formulas

There are no references for this article.