Skolem problem

The Skolem problem is a decision problem in mathematical logic concerning the satisfiability of certain types of logical formulas, particularly those expressed in first-order logic. Named after the mathematician Thoralf Skolem, the problem deals specifically with the question of whether a given first-order formula (often in prenex normal form, which has all its quantifiers at the front) has a model (i.e., an interpretation under which the formula is true).