Elimination des quantificateurs

Elimination des quantificateurs

Élimination des quantificateurs

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

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

Article connexe

Références

  1. ↑ Jeanne Ferrante et Charles Rackoff, A decision procedure for the first order theory of real addition with order, SIAM Journal of Computation, mars 1975, vol 4, n⁰1, pp. 69-76
  2. ↑ Aaron R. Bradley et Zohar Manna, The Calculus of Computation: Decision Procedures with Applications to Verification, Springer, octobre 2007, ISBN 3540741127
  3. ↑ Rüdiger Loos et Volker Weispfenning, Applying linear quantifier elimination, The Computer Journal, 1993, vol 36, n⁰5, pp. 450-462 DOI:doi:10.1093/comjnl/36.5.450, PDF
  • Portail des mathématiques Portail des mathématiques
  • Portail de la logique Portail de la logique
Ce document provient de « %C3%89limination des quantificateurs ».

Wikimedia Foundation. 2010.

Contenu soumis à la licence CC-BY-SA. Source : Article Elimination des quantificateurs de Wikipédia en français (auteurs)

Игры ⚽ Нужен реферат?

Regardez d'autres dictionnaires:

  • Élimination des quantificateurs — 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… …   Wikipédia en Français

  • MODÈLES (THÉORIE DES) — «Modèle» est un terme qui appartient au vocabulaire de la plupart des sciences et qui a des significations multiples [cf. MODÈLE]. Ainsi, dans les sciences humaines, on entend généralement par modèle une théorie conçue pour expliquer un ensemble… …   Encyclopédie Universelle

  • Liste des articles de mathematiques — Projet:Mathématiques/Liste des articles de mathématiques Cette page recense les articles relatifs aux mathématiques, qui sont liés aux portails de mathématiques, géométrie ou probabilités et statistiques via l un des trois bandeaux suivants  …   Wikipédia en Français

  • Projet:Mathématiques/Liste des articles de mathématiques — Cette page n est plus mise à jour depuis l arrêt de DumZiBoT. Pour demander sa remise en service, faire une requête sur WP:RBOT Cette page recense les articles relatifs aux mathématiques, qui sont liés aux portails de mathématiques, géométrie ou… …   Wikipédia en Français

  • Méthode des tableaux — Représentation graphique d un tableau propositionnel partiellement construit En théorie de la démonstration, les tableaux sémantiques sont une méthode de résolution du problème de la décision pour le calcul des propositions et les logiques… …   Wikipédia en Français

  • Calcul Des Séquents — En logique mathématique et plus précisément en théorie de la démonstration, le calcul des séquents est un système de déduction créé par Gerhard Gentzen[1][2]. Le nom de ce formalisme fait référence à un style particulier de déduction qui manipule …   Wikipédia en Français

  • Calcul des sequents — Calcul des séquents En logique mathématique et plus précisément en théorie de la démonstration, le calcul des séquents est un système de déduction créé par Gerhard Gentzen[1][2]. Le nom de ce formalisme fait référence à un style particulier de… …   Wikipédia en Français

  • Calcul des séquents — En logique mathématique et plus précisément en théorie de la démonstration, le calcul des séquents est un système de déduction créé par Gerhard Gentzen[1],[2]. Le nom de ce formalisme fait référence à un style particulier de déduction qui… …   Wikipédia en Français

  • MATHÉMATIQUES (FONDEMENTS DES) — Au sens premier et fort, le mot «fondement» désigne la base, jugée inébranlable, sur laquelle repose un corps d’énoncés, un système de connaissances, un complexe de croyances ou de conduites. «Reposer sur la base» signifie ici «trouver en elle à… …   Encyclopédie Universelle

  • Calcul des propositions — Pour les articles homonymes, voir Déduction. Le calcul des propositions ou calcul propositionnel est une théorie logique qui définit les lois formelles du raisonnement. C est la version moderne de la logique stoïcienne. C est aussi la première… …   Wikipédia en Français

Share the article and excerpts

Direct link
… Do a right-click on the link above
and select “Copy Link”