Quantifier elimination is a concept in mathematical logic, model theory, and theoretical computer science. One way of classifying formulas is by the amount of quantification. Formulae with less depth of quantifier alternation are thought of as simpler and the quantifier free formulae as the simplest.

PropertyValue
dbpprop:abstract
  • Quantifier elimination is a concept in mathematical logic, model theory, and theoretical computer science. One way of classifying formulas is by the amount of quantification. Formulae with less depth of quantifier alternation are thought of as simpler and the quantifier free formulae as the simplest. A theory has quantifier elimination if for every formula <math>\alpha</math> there exists a formula <math>\alpha_{QF}</math> without quantifiers which is equivalent to it (modulo the theory).
  • 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 : Corps réels clos (théorème de Tarski-Seidenberg; algorithme CAD) Corps algébriquement clos (via les bases de Gröbner et le théorème d'extension) Théorie linéaire des rationnels ou des réels (algorithmes de Ferrante & Rackoff, de Loos & Weispfenning) Théorie linéaire des entiers, dite aussi arithmétique de Presburger
  • В математической логике элиминация кванторов — это процесс, порождающий по заданной логической формуле, другую, эквивалентную ей формулу, свободную от вхождений кванторов. Элиминация кванторов далеко не всегда возможна, но когда это так, алгоритм элиминации кванторов приносит исключительную пользу для исследователя.
  • 量詞消去是數理邏輯、模型論與計算機科學中的一類技巧。我們稱一個理論<math>T</math>可消去量詞，若且唯若對每個公式φ皆存在另一個不帶量詞的公式ψ，使得兩者在該理論中等價，即：<math>T \models \phi \leftrightarrow \psi</math>。 量詞消去在模型論有多種刻劃；即使一個理論可消去量詞，也不保證存在一個相應的演算法。 一個理論的量詞消去演算法係將一個帶量詞的公式轉成一個等價但不帶量詞的公式。利用這個演算法，我們能將任一句子（不帶自由變量的公式）轉成一個不帶變量的句子，後者通常可藉簡單的計算判定。因此，量詞消去演算法的存在性蘊含該理論的可判定性。
dbpprop:hasPhotoCollection
rdfs:comment
  • Quantifier elimination is a concept in mathematical logic, model theory, and theoretical computer science. One way of classifying formulas is by the amount of quantification. Formulae with less depth of quantifier alternation are thought of as simpler and the quantifier free formulae as the simplest.
  • 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.
  • В математической логике элиминация кванторов — это процесс, порождающий по заданной логической формуле, другую, эквивалентную ей формулу, свободную от вхождений кванторов.
rdfs:label
  • Quantifier elimination
  • Élimination des quantificateurs
  • Элиминация кванторов
  • 量詞消去
owl:sameAs
skos:subject
foaf:page
is dbpprop:redirect of