Arrêt de service programmé du vendredi 10 juin 16h jusqu’au lundi 13 juin 9h. Pour en savoir plus
Accéder directement au contenu Accéder directement à la navigation
Article dans une revue

Une nouvelle stratégie de mise sous forme prénexe pour des formules booléennes quantifiées avec bi-implications

Résumé :

La plupart des procédures pour résoudre le problème de validitédes formules booléennes quantifiées prennent en entrée seulement des formules sous forme normale négative, voire sous forme normale conjonctive, et donc prénexes. Mais, il est rarement naturel d’exprimer un problème directement sous cette forme. Par exemple, en spécification, des symboles propositionnels existentiellement quantifiés sont insérés, selon un même motif, pour capturer des résultats intermédiaires. Ainsi, pour pouvoir utiliser les solveurs de l’état de l’art, il est nécessaire de convertir toute formule booléenne quantifiée sous forme prénexe. Un problème majeur de cette mise sous forme prénexe est qu’elle détruit complètement la structure originale de la formule. De plus, lors de la mise sous forme prénexe des bi-implications il y a duplication de leurs sous-formules, ceci incluant les quantificateurs. Cela conduit généralement à une croissance exponentielle de la taille de la formule. Dans ce travail, nous nous focalisons sur le motif très courant des résultats intermédiaires. Nous mettons en évidence des équivalences logiques qui permettent d’extraire les sous-formules améliorant ainsi nettement les performances des solveurs de l’état de l’art.

Type de document :
Article dans une revue
Liste complète des métadonnées

https://hal.univ-angers.fr/hal-03350575
Contributeur : Okina Univ Angers Connectez-vous pour contacter le contributeur
Soumis le : mardi 21 septembre 2021 - 14:22:51
Dernière modification le : mercredi 20 octobre 2021 - 03:19:09
Archivage à long terme le : : mercredi 22 décembre 2021 - 19:02:04

Fichier

i309.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-03350575, version 1
  • OKINA : ua4259

Collections

Citation

Benoit da Mota, Igor Stéphan, Pascal Nicolas. Une nouvelle stratégie de mise sous forme prénexe pour des formules booléennes quantifiées avec bi-implications. Revue I3 - Information Interaction Intelligence, Cépaduès, 2009, 9 (2), Non spécifié. ⟨hal-03350575⟩

Partager

Métriques

Consultations de la notice

3

Téléchargements de fichiers

10