One player (E) has the goal of choosing values so as to make the formula
true, and selects values for the variables that are existentially quantified with
The opposing player (A) has the goal of making the formula
false, and selects values for the variables that are universally quantified with
The players take turns according to the order of the quantifiers, each assigning a value to the next bound variable in the original formula.
Once all variables have been assigned values, Player E wins if the resulting expression is true.
In computational complexity theory, the language FORMULA-GAME is defined as all formulas
FORMULA-GAME is PSPACE-complete because it is exactly the same decision problem as True quantified Boolean formula.