A decision or recognition problem concerns the issue of determining if an element (input string) is in a given set (language).
We want to study the complexity of such problems. We can do this by considering ordinary (multi-tape) Turing machines as well as
non-deterministic Turing machines. There are two main results in the paper concerning propositional logic:
The first states that every problem that can be solved in polynomial time by a non-deterministic Turing machine can be reduced to checking whether a given logical proposition expressed in disjunctive normal form is a tautology. In more modern terminology, we would say that checking if a logical proposition in the disjunctive normal form is a tautology is NP-complete. In other words, if we solve the tautology problem, we also solve also all problems in the NP class, namely all problems that can be
solved in polynomial time by a non-deterministic Turing machine.
The second result establishes that checking whether a logical proposition is a tautology in its disjunctive normal form has the same degree of difficulty of the following problems:
- checking whether a proposition (expressed in any form) is a
tautology; - checking whether a proposition in disjunctive normal form where each disjunct has at most three conjunctions is a tautology;
- given two finite undirected graphs, checking whether the former is isomorphic to a subgraph of the latter.
To sum up, in general, it is a hard problem to determine if a given
logical proposition is a tautology even if it is expressed in disjunctive normal forms. Another consequence is that it is fruitless to develop a polynomial algorithm for solving the subgraph isomorphism decision problem on a deterministic Turing machine: it is isomorphic to the tautology problem.
Bibliography
S. A. Cook, The Complexity of Theorem-Proving Procedures, Proceedings
of the third annual ACM symposium on theory of computing, 1971
HEIN RESEARCH 