Suppose T is a theory (i.e., a set of sentences) in a formal language L of logic. A decision procedure for T is a mechanical procedure for calculating whether any given sentence of L is a logical consequence of T. We say that T is decidable if it has a decision procedure and undecidable if not. The decision problem for T is to determine whether or not T is decidable. (One can avoid the slightly vague notion of a mechanical procedure by noting that a theory T is decidable if and only if the set of its logical consequences is computable.)

Quantifier elimination and related model-theoretic techniques have yielded proofs that many important first-order theories are decidable. Examples are the theory of addition of integers (Presburger 1930), the theories of real-closed fields and algebraically closed fields (Tarski 1951), the theory of abelian groups...