Fórmula booleana cuantificada verdadera

Una formula booleana cuantificada verdadera es una fórmula de Boole que contiene cuantificadores, en la que además toda variable está ligada a un cuantificador, de tal manera que la fórmula completa no tienen variables libres por una fórmula de la forma:

Toda fórmula como la anterior debe ser cierta o falsa según una cierta interpretación de la teoría de modelos. El conjunto de todas las fórmulas de la forma anterior que son verdaderas forma un lenguaje formal llamado lenguaje TQBF (Totally Quantified Boolean Formulae) usado en ciencia computacional y que contiene fórmulas booleanas verdaderas completamente cuantificadas.

Una fórmula booleana plenamente cuantificada es una fórmula en lógica de primer orden donde toda variable es cuantificada (o atada), utilizando o el cuantificador existencial o el universal al principio de cada sentencia. Cualquier fórmula de este tipo es siempre verdadera o falsa (ya que no hay variables independientes). Si tal fórmula se evalúa como verdadera, entonces la fórmula está en el lenguaje TQBF. También es conocido como QSAT (SAT Cuantificado).