Action spécifique QBF

Présentation

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

siteasqbf@cril.univ-artois.fr