Dans ce papier, nous présentons une nouvelle architecture parallèle ouverte pour répondre à différents problèmes portant sur les formules booléennes quantifiées, dont la validité. La principale caractéristique de notre approche est qu'elle est basée sur un découpage syntaxique de la formule pour le traitement de sous-formules indépendantes. Elle est liée au choix de traiter des formules booléennes quantifiées sans restriction syntaxique, comme la forme prénexe ou la forme normale conjonctive. Dans ce cadre parallèle général ouvert, nous sommes capables d'introduire différents oracles, sous la forme d'algorithmes séquentiels pour l'élimination de quantificateurs. Nous présentons nos premières expérimentations en instanciant un unique oracle et en rapportons les résultats.