A formula game is an artificial game represented by a fully quantified Boolean formula. Players' turns alternate and the space of possible moves is denoted by

bound variables In mathematics, and in other disciplines involving formal languages, including mathematical logic and computer science, a free variable is a notation (symbol) that specifies places in an expression where substitution may take place and is not ...

. If a variable is

universally quantified In mathematical logic, a universal quantification is a type of quantifier, a logical constant which is interpreted as "given any" or "for all". It expresses that a predicate can be satisfied by every member of a domain of discourse. In other w ...

, the formula following it has the same

truth value In logic and mathematics, a truth value, sometimes called a logical value, is a value indicating the relation of a proposition to truth, which in classical logic has only two possible values (''true'' or '' false''). Computing In some progr ...

as the formula beginning with the universal quantifier regardless of the move taken. If a variable is

existentially quantified In predicate logic, an existential quantification is a type of quantifier, a logical constant which is interpreted as "there exists", "there is at least one", or "for some". It is usually denoted by the logical operator symbol ∃, which, whe ...

, the formula following it has the same truth value as the formula beginning with the existential quantifier for at least one move available at the turn. Turns alternate, and a player loses if he cannot move at his turn. In

computational complexity theory In theoretical computer science and mathematics, computational complexity theory focuses on classifying computational problems according to their resource usage, and relating these classes to each other. A computational problem is a task solved by ...

, the language FORMULA-GAME is defined as all formulas

\Phi

such that Player 1 has a winning strategy in the game represented by

\Phi

. FORMULA-GAME is

PSPACE-complete In computational complexity theory, a decision problem is PSPACE-complete if it can be solved using an amount of memory that is polynomial in the input length (polynomial space) and if every other problem that can be solved in polynomial space can b ...

References

* Sipser, Michael. (2006). ''Introduction to the Theory of Computation''. Boston: Thomson Course Technology. Satisfiability problems Boolean algebra PSPACE-complete problems {{comp-sci-stub