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
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.

Type de document :
Communication dans un congrès
Liste complète des métadonnées

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

Fichier

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

Identifiants

  • HAL Id : hal-03350656, version 1
  • OKINA : ua4540

Collections

Citation

Benoit da Mota, Igor Stéphan, Pascal Nicolas. Une mise sous forme prénexe préservant les résultats intermédiaires pour les formules booléennes quantifiées. Journées Nationales de l’IA Fondamentale, 2008, Paris, France. ⟨hal-03350656⟩

Partager

Métriques

Consultations de la notice

2

Téléchargements de fichiers

2