Équivalences et forme prénexe pour les formules booléennes quantifiées.

DocumentCommentaireFichier
Fichier pdf chargé le 30/10/2014 à 10:00:30
Accès libre
(version auteur)
version avant corrections mineures de l'éditeurfichier
TitreÉquivalences et forme prénexe pour les formules booléennes quantifiées.
Type de publicationArticle de revue
AuteurDa Mota, Benoit
EditeurLavoisier
TypeArticle scientifique dans une revue à comité de lecture
Année2011
LangueFrançais
Date2011
Numéro6
Pagination717 - 742
Volume25
Titre de la revueRevue d'Intelligence Artificielle
ISSN0992-499X
Mots-clésforme prénexe, Formules Booléennes Quantifiées, fusion de quantificateurs, vérification formelle
Résumé en français

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. Or, il est rarement naturel d’exprimer un problème directement sous cette forme. Dans ce travail, nous exhibons un motif possédant d’intéressantes propriétés, particulièrement lors de la mise sous forme prénexe. Les résultats expérimentaux montrent qu’utiliser nos équivalences logiques améliore le temps de résolution par les différentes procédures.

URL de la noticehttp://okina.univ-angers.fr/publications/ua4260