Élimination des quantificateurs

Un article de Wikipédia, l'encyclopédie libre.
Aller à : navigation, rechercher

En algorithmique ou en logique mathématique, l'élimination des quantificateurs est l'action consistant à remplacer une formule d'une certaine logique contenant éventuellement des quantificateurs ∀ ou ∃ par une formule équivalente (admettant les mêmes modèles), mais sans quantificateur.

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²-4c≥0.

Définitions[modifier | modifier le code]

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 transforme une formule en 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 du tout. 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.

Exemples[modifier | modifier le code]

Exemples de théories admettant l'élimination des quantificateurs :

Notes et références[modifier | modifier le code]

  1. (en) Jeanne Ferrante et Charles Rackoff, « A decision procedure for the first order theory of real addition with order », SIAM J. on Computing, vol. 4, no 1,‎ mars 1975, p. 69-76 (DOI 10.1137/0204006)
  2. (en) Aaron R. Bradley et Zohar Manna, The Calculus of Computation: Decision Procedures with Applications to Verification, Springer,‎ octobre 2007 (ISBN 978-3-540-74112-1)
  3. (en) Rüdiger Loos et Volker Weispfenning, « Applying linear quantifier elimination », The Computer Journal, vol. 36, no 5,‎ 1993, p. 450-462 (DOI 10.1093/comjnl/36.5.450), PDF

Voir aussi[modifier | modifier le code]

Articles connexes[modifier | modifier le code]

Bibliographie[modifier | modifier le code]

  • Jean-Louis Krivine et Georg Kreisel, Éléments de logique mathématique (théorie des modèles), Paris, Dunod, 1966, chap. 4, pdf
  • Jean-François Pabion, Logique mathématique, chapitre VI "Élimination des quantificateurs" pp.191-210, Hermann, Paris 1976 (ISBN 2-7056 5830-0)