The Entscheidungsproblem (The Decision Problem) is a machine that: Given an input of a Predicate formula F Gives an output of true if and only if F is a tautology.