El lenguaje TQBF es un lenguaje formal de la ciencia computacional que contiene Fórmulas Booleanas Verdaderas Totalmente 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)