 |
Communication dans un congrès
Une mise sous forme prénexe préservant les résultats intermédiaires pour les formules booléennes quantifiées
Résumé :
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.
https://hal.univ-angers.fr/hal-03350656
Contributeur : Okina Univ Angers Connectez-vous pour contacter le contributeur
Soumis le : mardi 21 septembre 2021 - 14:45:21
Dernière modification le : mercredi 20 octobre 2021 - 03:19:09
Archivage à long terme le : : mercredi 22 décembre 2021 - 19:04:53
Contributeur : Okina Univ Angers Connectez-vous pour contacter le contributeur
Soumis le : mardi 21 septembre 2021 - 14:45:21
Dernière modification le : mercredi 20 octobre 2021 - 03:19:09
Archivage à long terme le : : mercredi 22 décembre 2021 - 19:04:53
Fichier
iaf08.pdf
Fichiers produits par l'(les) auteur(s)