Ola Jose,
Nao sei se ajuda, mas segue anexo um brevíssimo resumo sobre QBF´s (complementa a nota anterior sobre lógica modal).
No final da nota segue a referencia que havia lhe falado (Cook, Ladner e stockmayer).
Há outros textos que aplicam o método de tableaux semântico junto com algoritmos que tratam qbf´s em problemas de model checking (um deles é o Fabio Massacci).
Ate +,
Flavio.
Forum