Quantifier Elimination

---

Quantifier elimination is the removal of all quantifiers (the universal quantifier  and existential quantifier ) from a quantified system. A first-order theory allows quantifier elimination if, for each quantified formula, there exists an equivalent quantifier-free formula. Examples of such theories include the real numbers with , , , and , and the theory of complex numbers with , , and . Quantifier elimination is implemented in as Resolve[expr].

Unfortunately, the worst-case time-complexity for real quantifier elimination is doubly exponential in the number of quantifier blocks (Weispfenning 1988, Davenport and Heintz 1988, Heintz et al. 1989, Caviness and Johnson 1998).

---

REFERENCES

Caviness, B. F. and Johnson, J. R. (Eds.). Quantifier Elimination and Cylindrical Algebraic Decomposition. New York:Springer-Verlag, 1998.

Collins, G. E. "Quantifier Elimination for Real Closed Fields by Cylindrical Algebraic Decomposition." In Proc. 2nd GI Conf. Automata Theory and Formal Languages. New York:Springer-Verlag, pp. 134-183, 1975.

Collins, G. E. "Quantifier Elimination by Cylindrical Algebraic Decomposition--Twenty Years of Progress." In Quantifier Elimination and Cylindrical Algebraic Decomposition (Ed. B. F. Caviness and J. R. Johnson). New York:Springer-Verlag, pp. 8-23, 1998.

Collins, G. E. and Hong, H. "Partial Cylindrical Algebraic Decomposition for Quantifier Elimination." J. Symb. Comput. 12, 299-328, 1991.

Davenport, J. H. "Computer Algebra for Cylindrical Algebraic Decomposition." Report TRITA-NA-8511, NADA, KTH, Stockholm, Sept. 1985.Davenport, J. and Heintz, J. "Real Quantifier Elimination Is Doubly Exponential." J. Symb. Comput. 5, 29-35, 1988.

Dolzmann, A. and Sturm, T. "Simplification of Quantifier-Free Formulae over Ordered Fields." J. Symb. Comput. 24, 209-231, 1997.

Dolzmann, A. and Weispfenning, V. "Local Quantifier Elimination." http://www.fmi.uni-passau.de/~dolzmann/refs/MIP-0003.ps.Z.Heintz, J.; Roy, R.-F.; and Solerno, P. "Complexité du principe de Tarski-Seidenberg." C. R. Acad. Sci. Paris Sér. I Math. 309, 825-830, 1989.

Loos, R. and Weispfenning, V. "Applying Lattice Quantifier Elimination." Comput. J. 36, 450-461, 1993.

Strzebonski, A. "Solving Algebraic Inequalities." Mathematica J. 7, 525-541, 2000.Weispfenning, V. "The Complexity of Linear Problems in Fields." J. Symb. Comput. 5, 3-27, 1988.

اخر الاخبار

اخبار العتبة العباسية المقدسة

جولة تفقدية لمتابعة خطة تنظيم مداخل المعزّين المشاركين في عزاء ركضة طويريج

لتعزيز التعاون الأكاديمي والبحثي.. جامعة الكفيل توقع اتفاقيتي توأمة مع جامعتين عراقيتين

المجمَع العلميّ يواصل إقامة مجلسه العزائي بذكرى شهادة الإمام الحسين (عليه السلام) في النجف الأشرف

قسم حفظ النظام يواصل تنفيذ خطته لتنظيم سير المواكب والزائرين في شهر المحرم

المزيد

الآخبار الصحية

لهذا السبب.. إغلاق 25 مركزًا لعلاج الإدمان في مصر ؟

خلافا للاعتقاد الشائع.. علماء يكشفون أسرار بذور البطيخ ؟!

هذا ما يحدث لجسمك عند تناولك الطماطم بانتظام !

تعرف على أطعمة تسرّع "تعافي الجسم" من حروق الشمس

المزيد

الآخبار التكنلوجية

الثلوج تغطي الصحراء الأكثر جفافا في العالم!

بتلسكوب "ألما".. التقاط صورا غير مسبوقة لبدايات الكون !

هل هاتفك مراقب؟.. 5 علامات خطيرة تكشف التجسس عليك

دبي تطلق أول رحلة تجريبية للتاكسي الجوي

المزيد

مواضيع ذات صلة

Lemma

Proof

Zeno,s Paradoxes

Unexpected Hanging Paradox

Strange Loop

Sorites Paradox

Simpson,s Paradox

Russell,s Antinomy

Paradox

Newcomb,s Paradox

Missing Dollar Paradox

Line Point Picking