Decidable Theory

A theory is decidable if there exists an algorithm that, given any sentence in the theory's language, determines in finite time whether that sentence is a consequence of the theory (i.e., whether the sentence belongs to the theory's set of theorems).