arski's Theorem

---

Tarski's theorem says that the first-order theory of reals with , , , and  allows quantifier elimination. Algorithmic quantifier elimination implies decidability assuming that the truth values of sentences involving only constants can be computed. However, the converse is not true. For example, the first-order theory of reals with , , and  is decidable, but does not allow quantifier elimination.

Tarski's theorem means that the solution set of a quantified system of real algebraic equations and inequations is a semialgebraic set (Tarski 1951, Strzebonski 2000).

Although Tarski proved that quantifier elimination was possible, his method was totally impractical (Davenport and Heintz 1988). A much more efficient procedure for implementing quantifier elimination is called cylindrical algebraic decomposition. It was developed by Collins (1975) and is implemented as CylindricalDecomposition[ineqs, vars].

---

REFERENCES

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.

Davenport, J. and Heintz, J. "Real Quantifier Elimination Is Doubly Exponential." J. Symb. Comput. 5, 29-35, 1988.

Marker, D. "Model Theory and Exponentiation." Not. Amer. Math. Soc. 43, 753-759, 1996.

Strzebonski, A. "Solving Algebraic Inequalities." Mathematica J. 7, 525-541, 2000.

Tarski, A. "Sur les ensembles définissables de nombres réels." Fund. Math. 17, 210-239, 1931.

Tarski, A. A Decision Method for Elementary Algebra and Geometry. Manuscript. Santa Monica, CA: RAND Corp., 1948.

Republished as A Decision Method for Elementary Algebra and Geometry, 2nd ed. Berkeley, CA: University of California Press, 1951.

اخر الاخبار

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

قسم الشعائر يواصل تحضيراته لتنظيم عمل المواكب الحسينية في زيارة الأربعين

قسم شؤون المعارف يناقش تحضيرات المؤتمر العلمي الأول لمركز تراث البصرة

قسم الشؤون الفكرية يقيم دورة تطويرية لملاكات هيأة المساءلة والعدالة في الأرشفة الإلكترونية

المجمع العلمي ينظم مجلس عزاء في قضاء الهندية

المزيد

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

نصائح عملية للحد من التعرق المفرط في الصيف

أطباء يحذرون: مكمل غذائي شائع قد يدمر الجهاز العصبي

تحذير طبي من تأثير جانبي "غير متوقع" لحقن التخسيس

حمامات الثلج قد تكون خطيرة وأحيانا مميتة.. ما السبب؟

المزيد

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

أكبر جدارية شمسية في العالم تدخل موسوعة غينيس.. مشروع ضخم

تسارع دوران الأرض يثير القلق.. وتحذيرات من "كوارث محتملة" ؟

"سوذبيز" تطرح أكبر قطعة من المريخ على الأرض في مزاد علني

أوبن أيه آي تعتزم إطلاق متصفح إنترنت يعمل بالذكاء الاصطناعي

المزيد

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

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