Skip to Main content Skip to Navigation
Conference papers

Algorithmes d'élimination de quantificateurs pour le calcul des politiques des formules booléennes quantifées

Résumé : Le problème de validité d'une formule booléenne quantifiée est une généralisation du problème de satisfiabilité d'une formule booléenne. Les formules booléennes quantifiées sont utiles pour représenter par exemple des stratégies dans un jeu à deux joueurs mais dans de telles applications c'est une solution au problème de recherche associé qui est nécessaire. La plupart des procédures de décision récentes pour les formules booléennes quantifiées sont des extensions de la procédure de recherche dite de Davis-Putnam et peuvent être aisément étendues au problème de recherche. Ce n'est pas le cas pour les algorithmes basés sur l'élimination de quantificateurs. Dans cet article nous montrons comment des algorithmes d'élimination de quantificateurs peuvent être étendus pour le problème de recherche associé aux formules booléennes quantifiées.
Complete list of metadata

https://hal.inria.fr/inria-00000078
Contributor : Christine Solnon <>
Submitted on : Thursday, May 26, 2005 - 12:46:14 PM
Last modification on : Monday, June 1, 2020 - 4:54:02 PM
Long-term archiving on: : Thursday, April 1, 2010 - 9:33:38 PM

Files

Identifiers

  • HAL Id : inria-00000078, version 1

Collections

Citation

Igor Stéphan. Algorithmes d'élimination de quantificateurs pour le calcul des politiques des formules booléennes quantifées. Premières Journées Francophones de Programmation par Contraintes, CRIL - CNRS FRE 2499, Jun 2005, Lens, pp.79-88. ⟨inria-00000078⟩

Share

Metrics

Record views

112

Files downloads

366