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.

اخر الاخبار

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

العتبة العباسية المقدسة: نهج البلاغة مصدر صافٍ للفكر والمعرفة ومحصِّنٌ من الشبهات

العتبة العباسية المقدسة تطلق محاضرات محفل نهج البلاغة الأسبوعي في ذي قار

العتبتان المقدستان الحسينية والعباسية تدعوان للمشاركة في مهرجان الشموع بنسخته السادسة والعشرين

بالتعاون مع مستشفى الكفيل.. قسم الشؤون الطبّية يواصل إقامة البرنامج التدريبي لملاكاته النسوية

المزيد

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

الصحة العالمية تكشف حقيقة انتشار فيروس نيباه خارج الهند

متى يصبح محيط الخصر "مؤشر خطر"؟

دراسة تكشف دور "العوامل الوراثية" في تحديد عمر الإنسان

رائحة كريهة في الجسم.. "علامة خفية" أخطر مما تتصور

المزيد

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

مايكروسوفت تكشف عن الجيل الثاني من شرائحها للذكاء الاصطناعي

خرافة "ثمانية أكواب يوميا".. كم من الماء يحتاج جسمك فعليا؟

هل توجد حياة خارج كوكبنا؟.. اكتشاف جديد يثير اهتمام العلماء

اكتشاف الخلايا المسؤولة عن فقدان ذاكرة الطفولة

المزيد

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

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