S'il est clair que l'étude des performances d'algorithmes passe en pratique par leur évaluation expérimentale, ce domaine reste encore émergeant, notamment en déduction automatique. La comparaison de systèmes demande non seulement une bonne connaissance de ceux-ci et des problèmes abordés, mais aussi une importante réflexion sur les techniques employées pour les comparaisons. Souvent, la comparaison du temps CPU seul ne suffit pas et la qualité des solutions doit être prise en compte. On retrouve dans tous les cas des critères de reproduction des résultats, de transparence et d'objectivité, ainsi qu'un critère d'incrémentalité, de manière à introduire de nouveaux algorithmes à moindre coût dans l'échelle des comparaisons de tous les algorithmes déjà considérés. L'expertise acquise sur la comparaison de démonstrateurs SAT, via SAT-EX, peut être adaptée au cas des QBF. Nous projetons, comme pour le problème SAT, d'identifier un certain nombre d'instances de test, pouvant servir de base commune pour la comparaison expérimentale de démonstrateurs QBF. L'étude des spécificités des instances structurées par rapport aux instances aléatoires est également un point important.