of checking tautologies is equivalent to this problem, because verifying that a sentence S is a tautology is equivalent to verifying that there is no valuation satisfying . It is known that the Boolean satisfiability problem is NP complete, and widely believed that there is no polynomial-time algorithm that can perform it. Consequently, tautology is co-NP-complete. Current research focuses on finding algorithms that perform well on special classes of formulas, or terminate quickly on average even though some inputs may cause them to take much longer. Tautologies versus validities in first-order logic The fundamental definition of a tautology is in the context of propositional logic. The definition can be extended, however, to sentences in first-order logic. These sentences may contain quantifiers, unlike sentences of propositional logic. In the context of first-order logic, a distinction is maintained between logical validities, sentences that are true in every model, and tautologies (or, tautological validities), which are a proper subset of the first-order logical validities. In the context of propositional logic, these two terms coincide. A tautology in first-order logic is a sentence that can be obtained by taking a tautology of propositional logic and uniformly replacing each propositional variable by a first-order formula (one formula per propositional variable). For example, because is a tautology of propositional logic, is a tautology in first order logic. Similarly, in a first-order language with a unary relation symbols R,S,T, the following sentence is a tautology: It is obtained by replacing with , with , and with in the propositional tautology . Not all logical validities are tautologies in first-order logic. For example, the sentence is true in any first-order interpretation, but it corresponds to the propositional sentence which is not a tautology of propositional logic. See also Normal forms Algebraic normal form Conjunctive normal form Disjunctive normal form Logic optimization Related logical topics Boolean algebra Boolean domain Boolean function Contradiction False (logic) Syllogism List of logic symbols Logic synthesis Logical consequence Logical graph Logical truth Vacuous truth References Further reading Bocheński, J. M. (1959) Précis of Mathematical Logic, translated from the French and German editions by Otto Bird, Dordrecht, South Holland: D. Reidel. Enderton, H. B. (2002) A Mathematical Introduction to Logic, Harcourt/Academic Press, . Kleene, S. C. (1967) Mathematical Logic, reprinted 2002, Dover Publications, . Reichenbach, H. (1947). Elements of Symbolic Logic, reprinted 1980, Dover, Wittgenstein, L. (1921). "Logisch-philosophiche Abhandlung", Annalen der Naturphilosophie (Leipzig), v. 14,