|
L'objet de cette action est de proposer des algorithmes efficaces (en
pratique) de résolution de formules booléennes
quantifiées (QBF, logique propositionnelle). Pour accompagner
l'émergence de ces nouveaux algorithmes, un important travail
de réflexion sur leur évaluation expérimentale
est nécessaire. Celui-ci doit non seulement permettre de mieux
appréhender — avant tout d'un point de vue pratique — les
verrous scientifiques liés à la résolution de ces
problèmes fondamentaux, mais aussi de déboucher sur des
propositions d'évaluations expérimentales
concrètes, naturellement généralisables à
d'autres problématiques de démonstration et
déduction automatique.
Une Journée de Travail sur les Formules Booléennes
Quantifiées a été organisée le 21 novembre
2003
|