Élimination des quantificateurs
Un article de Wikipédia, l'encyclopédie libre.
 |
Cet article est une ébauche concernant les mathématiques.
Vous pouvez partager vos connaissances en l’améliorant. (Comment ?).
|
En algorithmique ou en logique mathématique, l'élimination des quantificateurs est l'action de remplacer une formule d'une certaine logique contenant éventuellement des quantificateurs ∀ ou ∃ par une formule équivalente (admettant les mêmes modèles), mais sans quantificateurs.
Ainsi, si l'on considère la théorie des corps réels clos, la formule ∃x x²+bx+c=0 peut être remplacée par la formule équivalente b²-c≥0.
On dit qu'une théorie admet l'élimination des quantificateurs si toute formule de la théorie peut être remplacée par une formule sans quantificateurs, équivalente.
Un algorithme d'élimination des quantificateurs est un algorithme qui au vu d'une formule produit une formule sans quantificateurs équivalente, mais avec les mêmes variables libres. Une formule sans variables libres sera donc transformée en une formule sans variable tout court. Dans de nombreuses logiques, les formules sans variables sont facilement décidables ; l'algorithme d'élimination des quantificateurs peut donc servir de procédure de décision pour cette logique.
