TQBF

Le langage TQBF est un langage formel fondé sur la True Qantified Boolean Formula (vraie formule booléenne quantifiée).

Une formule booléenne (entièrement) quantifiée est une formule de la logique propositionnelle quantifiée dans laquelle chaque variable est quantifiée (ou liée), à l'aide de quantificateurs existentiels ou universels, au début de la phrase. Une telle formule est équivalente à true ou à false (puisqu'il n'y a pas de variables libres). Si une telle formule a la valeur true, elle est dans le langage TQBF. Il est également appelé QSAT (Quantified SAT).