A true quantized Boolean formula is a Boolean formula that contains quantifiers, where every variable is bound to a quantizer, so that the complete formula has no free variables for a formula of the form:
Q 1 x 1 & # xA0; Q 2 x 2 & # x2026; & # xA0; Q n x n : P ( x 1 , x 2 , & # x2026; , x n ) {\displaystyle Q_{1}x_{1}\ Q_{2}x_{2}\dots \ Q_{n}x_{n}:P(x_{1},x_{2},\dots ,x_{n})}
Any formula like the above must be true or false according to a certain interpretation of model theory. The set of all formulas of the previous form that are true forms a formal language called TQBF (Totally Quantified Boolean Formula) language used in computational science and containing fully quantified true Boolean formulas.
A fully quantized Boolean formula is a formula in first order logic where every variable is quantized (or bound), using either the existential or universal quantifier at the beginning of each statement. Any formula of this type is always true or false (since there are no independent variables). If such a formula is evaluated as true, then the formula is in the TQBF language. It is also known as QSAT (Quantized SAT).
wiki