suivant: Thématique abordée
Proposition d'Action Spécifique STIC-CNRS
ALGORITHMIQUE ET PROBLÉMATIQUE EXPÉRIMENTALE POUR
L'ÉVALUATION DE FORMULES BOOLÉENNES QUANTIFIÉES
Date: vendredi 30 août 2002
Animateurs : Philippe Chatalic, Laurent Simon (LRI, Orsay),
Daniel Le Berre (CRIL, Lens)
Résumé:
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.