Une mise sous forme prénexe préservant les résultats intermédiaires pour les formules booléennes quantifiées

La plupart des procédures pour résoudre le problème de validité desformules booléennes quantifiées prennent en entrée seulement des formules sous forme normale conjonctive. Mais, il est rarement naturel d’exprimer un problème directement sous cette forme et il est plus courant d’utiliser des variables existentielles pour représenter des résultats intermédiaires. Or, lors de la mise sous forme prénexe, l’équivalence est exprimée en fonction d’autres opérateurs logiques et les variables intermédiares sont multipliées. Dans ce travail, nous mettons en évidence des équivalences logiques qui permettent aux résultats intermédiaires de traverser les équivalences. Les résultats expérimentaux montrent qu’utiliser ces équivalences logiques avant de transformer la formule sous forme prénexe améliore le temps de résolution par les différentes procédures.