  We show that the first-order logical theory of the binary overlap-free words
(and, more generally, the ${\alpha}$-free words for rational ${\alpha}$, $2 <
{\alpha} \leq 7/3$), is decidable. As a consequence, many results previously
obtained about this class through tedious case- based proofs can now be proved
"automatically", using a decision procedure.
