On Computable Numbers, with an Application to the Entscheidungsproblem
Turing introduced an abstract model of computation—later called the Turing machine—to make precise the notion of a function being effectively calculable, defining 'computable numbers' as those whose decimals can be produced by such a machine. He proved the existence of a universal machine able to simulate any other and showed that some well-defined problems, including the halting problem, are not computable. Using these results he demonstrated that Hilbert's Entscheidungsproblem (decision problem) for first-order logic has no general algorithmic solution.