Élimination des quantificateurs
- É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 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.
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 de théories admettant l'élimination des quantificateurs :
Articles connexes
Liens externes
- Explication d'un algorithme d'éliminations des quantificateurs [1]
Bibliographie
Références
- ↑ 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
- ↑ Aaron R. Bradley et Zohar Manna, The Calculus of Computation: Decision Procedures with Applications to Verification, Springer, octobre 2007, ISBN 3-540-74112-7
- ↑ 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
Wikimedia Foundation.
2010.
Contenu soumis à la licence CC-BY-SA. Source : Article Élimination des quantificateurs de Wikipédia en français (auteurs)
Regardez d'autres dictionnaires:
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… … 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
