Base littérale et certificat pour les formules booléennes quantifiées

Nous étudions dans cet article une nouvelle forme normale, celle des bases littérales, pour les formules booléennes quantifiées (prénexes). Un des aspects majeurs d\u27une base littérale est que le certificat (qui permet de vérifier a posteriori qu\u27une décision positive sur une formule booléenne quantifiée est correcte ou non) en est un cas particulier. Notre principal résultat est un algorithme orienté recherche qui calcule un certificat associé à une formule booléenne quantifiée dans le cas où elle est valide. Un autre aspect majeur d\u27une base littérale est qu\u27elle peut être vue comme étant le résultat d\u27une compilation de la formule booléenne quantifiée qui respecte des propriétés d\u27optimalité en terme de construction de la solution et de minimalité en terme de modèles propositionnels de la matrice