The complexity of theorem-proving procedures

TLDR

Reduced means that a nondeterministic polynomial‑time recognition problem can be solved deterministically in polynomial time if an oracle for propositional tautology is available. The authors aim to introduce a method for measuring the complexity of proof procedures in predicate calculus. They propose a framework that quantifies proof complexity in predicate calculus. They show that any polynomial‑time nondeterministic recognition problem reduces to propositional tautology, define polynomial degrees of difficulty, and prove that tautology and subgraph isomorphism share the same degree, with additional examples discussed.

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.