実在論的実在理論
Quantified formulas with real-number variables

数理論理学、計算複雑性理論、およびコンピュータサイエンスにおいて、実数の存在理論と は、変数が実数値を持つと解釈され、実多項式の等式と不等式を含む量指定子のない式である、という形式のすべての真文の集合 である。この形式の文は、式に代入すると真となるすべての変数の値を見つけることができる場合、真である。[1] ∃ X 1 ⋯ ∃ X n F ( X 1 , … , X n ) , {\displaystyle \exists X_{1}\cdots \exists X_{n}\,F(X_{1},\dots ,X_{n}),} X i {\displaystyle X_{i}} F ( X 1 , … X n ) {\displaystyle F(X_{1},\dots X_{n})} F {\displaystyle F}

実数体の存在理論における決定問題は、各文が真か偽かを決定するアルゴリズムを見つける問題である。これは、与えられた半代数集合が空でないかどうかを判定する問題と同義である。[1]この決定問題はNP困難であり、 PSPACE [ 2]に属するため、実数体の一階理論において存在量化子に制限されない文を決定するアルフレッド・タルスキの量化子除去手続きよりも大幅に計算量が低い。[1]しかし、実際には、これらの問題を解決するには、一階理論の一般的な手法が依然として好ましい選択肢である。[3]

計算量クラスは、 この形式の等価な文に翻訳可能な計算問題のクラスを記述するために定義されている。構造計算量理論では、 NPとPSPACEの中間に位置する。幾何学的グラフ理論における多くの自然な問題、特に幾何学的交差グラフの認識や交差を持つグラフ描画の辺の直線化といった問題は、このクラスに属し、このクラスに対して完全である。ここで完全性とは、任意の実数上の文から、与えられた問題の等価な例への逆方向の翻訳が存在することを意味する。[4] ∃ R {\displaystyle \exists \mathbb {R} } ∃ R {\displaystyle \exists \mathbb {R} }

背景

数理論理学において、理論とは、一定の記号集合を用いて書かれた文の集合からなる形式言語である。実閉体の一階理論には、以下の記号が含まれる。[5]

  • 定数0と1、
  • 可算な変数の集合、 X i {\displaystyle X_{i}}
  • 加算、減算、乗算、および（オプションで）除算の演算、
  • 実数値の比較には記号<、≤、=、≥、>、≠を使用します。
  • 論理接続詞∧、∨、¬、⇔、
  • 括弧、および
  • 全称量化子∀ と存在量化子∃

これらの記号の列は、文法的に整形式であり、そのすべての変数が適切に量化されており、（実数についての数学的ステートメントとして解釈された場合）それが真のステートメントである場合、実数に関する第一階理論に属する文を形成します。タルスキが示したように、この理論は、公理図式と完全かつ有効な決定手続きによって記述できます。つまり、完全に量化され文法的に正しいすべての文について、文またはその否定（両方ではない）のいずれかを公理から導くことができます。同じ理論は、実数だけでなく、すべての実閉体を説明します。 [6]しかし、これらの公理では正確に記述できない他の数体系も存在します。特に、実数ではなく整数に対して同じように定義された理論は、マティヤセビッチの定理によって存在文（ディオファントス方程式）に対してでさえ決定不可能です。[5] [7]

実数体の存在理論は、すべての量指定子が存在的であり、他のどの記号よりも前に現れる文からなる一階理論の 一部である。つまり、 は実多項式の等式と不等式を含む量指定子のない式 である、という形式のすべての真の文の集合である。実数体の存在理論の決定問題は、与えられた文がこの理論に属するかどうかをテストするアルゴリズムの問​​題である。同様に、基本的な構文チェックを通過する文字列（正しい構文で正しい記号を使用し、量指定されていない変数を持たない文字列）の場合、その文が実数に関する真のステートメントであるかどうかをテストする問題である。が真となる実数の組の集合は半代数的集合と呼ばれるので、実数体の存在理論の決定問題は、与えられた半代数的集合が空でないかどうかをテストすることと同義に言い換えることができる。[1] ∃ X 1 ⋯ ∃ X n F ( X 1 , … , X n ) , {\displaystyle \exists X_{1}\cdots \exists X_{n}\,F(X_{1},\dots ,X_{n}),} F ( X 1 , … X n ) {\displaystyle F(X_{1},\dots X_{n})} n {\displaystyle n} ( X 1 , … X n ) {\displaystyle (X_{1},\dots X_{n})} F ( X 1 , … X n ) {\displaystyle F(X_{1},\dots X_{n})}

実数の存在理論の決定問題に対するアルゴリズムの時間計算量を決定するには、入力の大きさを測る尺度を持つことが重要である。この種の最も単純な尺度は文の長さ、すなわち文に含まれる記号の数である。 [5]しかし、この問題に対するアルゴリズムの挙動をより正確に分析するためには、入力の大きさを複数の変数に分解し、量化すべき変数の数、文に含まれる多項式の数、そしてこれらの多項式の次数を分離することが便利である。[8]

例

黄金比は 多項式の根として定義できます。この多項式には2つの根があり、そのうちの1つ（黄金比）のみが1より大きいです。したがって、黄金比の存在は次の文で表現できます。 黄金比は超越的ではないため、これは真の文であり、実数の存在理論に属します。この文を入力として与えられた場合、実数の存在理論の決定問題の答えはブール値 true です。 φ {\displaystyle \varphi } x 2 − x − 1 {\displaystyle x^{2}-x-1} ∃ X 1 ( X 1 > 1 ∧ X 1 × X 1 − X 1 − 1 = 0 ) . {\displaystyle \exists X_{1}(X_{1}>1\wedge X_{1}\times X_{1}-X_{1}-1=0).}

算術平均と幾何平均の不等式は、任意の2つの非負数とに対して、次の不等式が成り立つことを述べています。上述 のように、これは実数に関する一階述語文ですが、存在量指定子ではなく全称量指定子を用いており、また、実数に関する一階述語論では許されない除算、平方根、そして数2といった記号を追加で用いています。しかし、両辺を二乗することで、次の存在文に変換することができ、これは不等式に反例があるかどうかを問うているように解釈できます。 x {\displaystyle x} y {\displaystyle y} x + y 2 ≥ x y . {\displaystyle {\frac {x+y}{2}}\geq {\sqrt {xy}}.}

∃ X 1 ∃ X 2 ( X 1 ≥ 0 ∧ X 2 ≥ 0 ∧ ( X 1 + X 2 ) × ( X 1 + X 2 ) < ( X 1 + X 1 ) × ( X 2 + X 2 ) ) . {\displaystyle \exists X_{1}\exists X_{2}{\bigl (}X_{1}\geq 0\wedge X_{2}\geq 0\wedge (X_{1}+X_{2})\times (X_{1}+X_{2})<(X_{1}+X_{1})\times (X_{2}+X_{2}){\bigr )}.}

この文を入力として与えられた場合、実数体の存在理論の決定問題に対する答えはブール値falseである。すなわち、反例は存在しない。したがって、この文は文法的には正しい形式であるにもかかわらず、実数体の存在理論には属さない。

アルゴリズム

アルフレッド・タルスキの量限定子消去法（1948 年）は、実数の存在理論（およびより一般的には実数の第一階理論）がアルゴリズム的に解けることを示したが、その複雑さには基本的な限界がなかった。 [9] [6]ジョージ・E・コリンズ（1975 年）による円筒代数分解法は、時間依存性を二重指数に改善し、[9] [10]の形式と なった。 ここで、 は値を決定する文の係数を表すために必要なビット数、は文中の多項式の数、は多項式の総次数、は変数の数である。[8] 1988年までに、ディマ・グリゴリエフとニコライ・ボロビョフは、 の多項式で複雑性が指数関数的であることを示しました。[8] [11] [12] また、1992年に発表された一連の論文で、ジェームズ・レネガーはこれを の単一指数依存性に改良しました。[ 8] [13] [14] [15] 一方、1988年に、ジョン・キャニーは、やはり指数時間依存性を持つが、空間複雑度は多項式のみである別のアルゴリズムを説明しました。つまり、彼は、問題がPSPACEで解けることを示しまし た。[2] [9] L 3 ( m d ) 2 O ( n ) {\displaystyle L^{3}(md)^{2^{O(n)}}} L {\displaystyle L} m {\displaystyle m} d {\displaystyle d} n {\displaystyle n} n {\displaystyle n} L ( m d ) n 2 {\displaystyle L(md)^{n^{2}}} n {\displaystyle n} L log ⁡ L log ⁡ log ⁡ L ( m d ) O ( n ) . {\displaystyle L\log L\log \log L(md)^{O(n)}.}

これらのアルゴリズムの漸近的な計算複雑性は誤解を招く可能性がある。なぜなら、実際には非常に小さなサイズの入力でしか実行できないからである。1991年の比較で、Hoon Hongは、Collinsの二重指数手順では、上記のすべてのパラメータを2に設定することによって記述されるサイズの問題を1秒未満で解くことができるが、Grigoriev、Vorbjov、およびRenegarのアルゴリズムでは100万年以上かかると推定した。[8] 1993年に、Joos、Roy、およびSolernóは、指数時間手順に小さな変更を加えることで、理論上だけでなく実際にも円筒代数的決定よりも高速にすることができるはずだと示唆した。[16]しかし、2009年時点では、実数の一階理論に対する一般的な手法は、実数の存在理論に特化した単​​指数アルゴリズムよりも実際には優れているというのが現状である。[3]

完全な問題

計算複雑性と幾何学的グラフ理論におけるいくつかの問題は、実数の存在理論にとって完全であると分類できる。つまり、実数の存在理論におけるあらゆる問題は、これらの問題の1つの例への多項式時間多対一還元を持ち、そしてこれらの問題は実数の存在理論に還元可能である。[4] [17]

この種の問題の多くは、特定の種類の交差グラフの認識に関するものである。これらの問題では、入力は無向グラフであり、特定の図形のクラスの幾何学的図形を、それらの関連付けられた図形が空でない交差を持つ場合にのみ、2つの頂点がグラフ内で隣接しているような方法でグラフの頂点に関連付けることができるかどうかを判断することが目標である。実数の存在理論に対して完全なこの種の問題には、平面上の線分の交差グラフの認識、 [4] [18] [5]単位円グラフ の認識、[19] 平面上の凸集合の交差グラフの認識がある。[4]

平面上に交差のないグラフを描く場合、ファリーの定理によれば、グラフの辺が直線で描かれるか任意の曲線で描かれるかに関わらず、同じクラスの平面グラフが得られる。しかし、この同値性は他の描画タイプには当てはまらない。例えば、グラフの交差数（任意の曲線の辺を持つ描画における交差の最小数）はNPで決定できるが、直線交差数（平面上に直線の辺を持つ描画において、交差する辺のペアの最小数）に関して与えられた上限を満たす描画が存在するかどうかを実数の存在理論が決定することは完全である。[4] [20] また、実数の存在理論は、与えられたグラフが平面上に直線の辺を持ち、与えられた辺のペアの集合を交差点として描くことができるかどうか、あるいはそれと同等に、交差点を持つ曲線の描画を交差点を保存する方法で直線化できるかどうかをテストすることも完全である。[21]

実数の存在理論に関するその他の完全な問題には次のものがあります。

これに基づいて、計算量クラスは 実数の存在理論への多項式時間多対一還元を持つ問題の集合として定義されています。[4] ∃ R {\displaystyle \exists \mathbb {R} }

参照

参考文献

  1. ^ abcd Basu, Saugata; Pollack, Richard ; Roy, ​​Marie-Françoise (2006)、「実数の存在理論」、Algorithms in Real Algebraic Geometry、Algorithms and Computation in Mathematics、第10巻（第2版）、Springer-Verlag、pp.  505– 532、doi :10.1007/3-540-33099-2_14、ISBN 978-3-540-33098-1。
  2. ^ ab Canny, John (1988)、「PSPACEにおける代数的および幾何学的計算」、第20回ACMコンピューティング理論シンポジウム（STOC '88、シカゴ、イリノイ州、米国）の議事録、ニューヨーク、ニューヨーク州、米国：ACM、pp.  460– 467、doi：10.1145/62212.62257、ISBN 0-89791-264-0、S2CID  14535463
  3. ^ ab Passmore, Grant Olney; Jackson, Paul B. (2009)「実数の存在理論のための結合決定手法」、Intelligent Computer Mathematics: 第 16 回シンポジウム、Calculemus 2009、第 8 回国際会議、MKM 2009、CICM 2009 の一環として開催、カナダ、グランドベンド、2009 年 7 月 6 ～ 12 日、議事録、パート II、Lecture Notes in Computer Science、vol. 5625, Springer-Verlag, pp.  122– 137, doi :10.1007/978-3-642-02614-0_14, hdl : 20.500.11820/b2cc91c8-6b87-4146-bab6-a2021b3006b2 , ISBN 978-3-642-02613-3、S2CID  1160351。
  4. ^ abcdefg Schaefer, Marcus (2010)、「いくつかの幾何学的および位相的問題の複雑性」（PDF）、グラフ描画、第17回国際シンポジウム、GD 2009、シカゴ、イリノイ州、米国、2009年9月、改訂論文、Lecture Notes in Computer Science、vol. 5849、Springer-Verlag、pp.  334– 344、doi：10.1007/978-3-642-11805-0_32、ISBN 978-3-642-11804-3。
  5. ^ abcd Matoušek、Jiří (2014)、「セグメントの交差グラフと」、arXiv : 1406.2636 [cs.CG] ∃ R {\displaystyle \exists \mathbb {R} }
  6. ^ ab Tarski, Alfred (1948), A Decision Method for Elementary Algebra and Geometry , RAND Corporation, Santa Monica, California, MR  0028796。
  7. ^ Matiyasevich, Yu. V. (2006)、「ヒルベルトの第10問題：20世紀のディオファントス方程式」、20世紀の数学的出来事、ベルリン：シュプリンガー・フェアラーク、pp.  185– 213、Bibcode :2006metc.book.....A、doi :10.1007/3-540-29462-7_10、ISBN 978-3-540-23235-3、MR  2182785。
  8. ^ abcde Hong, Hoon (1991年9月11日). 「実数の存在理論のためのいくつかの決定アルゴリズムの比較」. RISC Linz ( FTP ). 技術レポート.[デッド FTP リンク] (ドキュメントを表示するには、ヘルプ:FTP を参照してください)。
  9. ^ abcd Schaefer, Marcus (2013)、「グラフとリンクの実現可能性」、Pach, János (ed.)、Thirty Essays on Geometric Graph Theory、Springer-Verlag、pp.  461– 482、doi :10.1007/978-1-4614-0110-0_24、ISBN 978-1-4614-0109-4。
  10. ^ Collins, George E. (1975), 「円筒代数分解による実閉体に対する量指定子除去」,オートマトン理論と形式言語 (第2回GI会議, カイザースラウテルン, 1975) ,コンピュータサイエンス講義ノート, 第33巻, ベルリン: Springer-Verlag, pp.  134– 183, MR  0403962。
  11. ^ Grigor'ev, D. Yu. (1988)、「タルスキ代数の決定の複雑さ」、Journal of Symbolic Computation、5 ( 1– 2): 65– 108、doi : 10.1016/S0747-7171(88)80006-3、MR  0949113。
  12. ^ Grigor'ev, D. Yu. ; Vorobjov, NN Jr. (1988)、「指数関数時間で多項式不等式系を解く」(PDF)、Journal of Symbolic Computation、5 ( 1– 2): 37– 64、doi :10.1016/S0747-7171(88)80005-1、MR  0949112、S2CID  39376619。
  13. ^ レネガー、ジェームズ (1992)、「実数体第一階理論の計算複雑性と幾何学について。I. 序論。予備的考察。半代数集合の幾何学。実数体の存在理論における決定問題」、Journal of Symbolic Computation、13 (3): 255– 299、doi : 10.1016/S0747-7171(10)80003-3、MR  1156882。
  14. ^ レネガー、ジェームズ (1992)、「実数第一階理論の計算複雑性と幾何学について。II. 一般決定問題。量限定子除去のための準備」、Journal of Symbolic Computation、13 (3): 301– 327、doi : 10.1016/S0747-7171(10)80004-5、MR  1156883。
  15. ^ レネガー、ジェームズ (1992)、「実数第一階理論の計算複雑性と幾何学について。III. 量指定子除去」、Journal of Symbolic Computation、13 (3): 329– 352、doi : 10.1016/S0747-7171(10)80005-7、MR  1156884。
  16. ^ Heintz, Joos ; Roy, ​​Marie-Françoise ; Solernó, Pablo (1993)、「実数の存在理論の理論的および実践的複雑さについて」、The Computer Journal、36 (5): 427– 431、doi : 10.1093/comjnl/36.5.427、MR  1234114。
  17. ^ abcd Cardinal, Jean (2015年12月)、「計算幾何学コラム62」、SIGACT News、46 (4): 69–78、doi :10.1145/2852040.2852053、S2CID  17276902。
  18. ^ クラトフヴィル、ヤン; Matoušek、Jiří (1994)、「セグメントの交差グラフ」、Journal of Combinatorial Theory、シリーズ B、62 (2): 289–315、doi : 10.1006/jctb.1994.1071、MR  1305055。
  19. ^ Kang, Ross J.; Müller, Tobias (2011)、「グラフの球面表現とドット積表現」、第27回計算幾何学シンポジウム(SCG'11)の議事録、2011年6月13～15日、フランス、パリ、pp.  308～ 314。
  20. ^ ビエンストック、ダニエル（1991）、「いくつかの証明困難な交差数問題」、離散幾何学と計算幾何学、6（5）：443-459、doi：10.1007/BF02574701、MR  1115102、S2CID  38465081。
  21. ^ Kynčl, Jan (2011)、「Pにおける完全な抽象位相グラフの単純実現可能性」、Discrete & Computational Geometry、45 (3): 383– 399、doi : 10.1007/s00454-010-9320-x、MR  2770542、S2CID  12419381。
  22. ^ アブラハムセン、ミッケル;アダマシェク、アンナ。ミルツォウ、ティルマン (2022)、「アート ギャラリーの問題は完全です」、Journal of the ACM、69 (1): A4:1–A4:70、doi :10.1145/3486220、hdl : 1874/424939、MR  4402363 ∃ R {\displaystyle \exists {\mathbb {R}}}
  23. ^ Abrahamsen, Mikkel; Kleist, Linda; Miltzow, Tillmann (2021)、「ニューラルネットワークのトレーニングは ∃ R {\displaystyle \exists \mathbb {R} } -完全である」、Ranzato, Marc'Aurelio; Beygelzimer, Alina; Dauphin, Yann N.; Liang, Percy; Vaughan, Jennifer Wortman (編)、Advances in Neural Information Processing Systems 34: Annual Conference on Neural Information Processing Systems 2021、NeurIPS 2021、2021年12月6日～14日、バーチャル、pp.  18293– 18306、arXiv : 2102.09798
  24. ^ アブラハムセン、ミッケル;ミルツォウ、ティルマン。 Seiferth、Nadja (2020)、「二次元パッキング問題の完全性のためのフレームワーク」、第 61 回コンピューターサイエンスの基礎に関する IEEE 年次シンポジウム、FOCS 2020、米国ノースカロライナ州ダラム、2020 年 11 月 16 ～ 19 日、IEEE、pp.  1014–1021、arXiv : 2004.07558、doi :10.1109/FOCS46700.2020.00098、ISBN ∃ R {\displaystyle \exists \mathbb {R} }  978-1-7281-9621-3、S2CID  216045462
  25. ^ Mnëv, NE (1988)、「配置多様体と凸多面体多様体の分類問題に関する普遍性定理」、トポロジーと幾何学 — ローリンセミナー、数学講義ノート、第1346巻、ベルリン：シュプリンガー出版社、pp.  527– 543、doi :10.1007/BFb0082792、ISBN 978-3-540-50237-1、MR  0970093。
  26. ^ Shor, Peter W. (1991)、「擬似直線の伸縮性はNP困難である」、応用幾何学と離散数学、DIMACSシリーズ離散数学と理論計算機科学、第4巻、プロビデンス、ロードアイランド州：アメリカ数学会、pp.  531– 554、MR  1116375。
  27. ^ Herrmann, Christian; Ziegler, Martin (2016)、「量子充足可能性の計算複雑性」、Journal of the ACM、vol. 63、pp.  1– 31、arXiv : 1004.1696、doi :10.1145/2869073、S2CID  2253943。
  28. ^ ベネディクト、マイケル、レンハート、ラスティスラフ、ウォレル、ジェームズ (2013)、「LTLモデル検査による区間マルコフ連鎖」、システム構築と分析のためのツールとアルゴリズム。TACAS 2013、コンピュータサイエンス講義ノート、第7795巻、pp.  32– 46、doi :10.1007/978-3-642-36742-7_3、ISBN 978-3-642-36741-0
  29. ^ Björner, Anders ; Las Vergnas, Michel ; Sturmfels, Bernd ; White, Neil ; Ziegler, Günter M. (1993) 「Oriented Matroids」『Encyclopedia of Mathematics and its Applications』第46巻、ケンブリッジ：ケンブリッジ大学出版局、Corollary 9.5.10、p. 407、ISBN 0-521-41836-4、MR  1226888。
  30. ^ Richter-Gebert, Jürgen; Ziegler, Günter M. (1995), "Realization spaces of 4-polytopes are universal", Bulletin of the American Mathematical Society , New Series, 32 (4): 403– 412, arXiv : math/9510217 , Bibcode :1995math.....10217R, doi :10.1090/S0273-0979-1995-00604-X, MR  1316500, S2CID  7940964。
  31. ^ ドビンズ、マイケル・ジーン; ホルムセン、アンドレアス; フバード、アルフレド (2017)、「凸体の配置の実現空間」、離散幾何学と計算幾何学、58 (1): 1– 29、arXiv : 1412.0371、doi :10.1007/s00454-017-9869-8、MR  3658327、S2CID  39856606。
  32. ^ Garg, Jugal; Mehta, Ruta; Vazirani, Vijay V .; Yazdanbod, Sadra (2015)、「ETR完全性のためのマルチプレイヤー（対称）ナッシュ均衡の決定バージョン」、Proc. 42nd International Colloquium on Automata, Languages, and Programming (ICALP)、Lecture Notes in Computer Science、vol. 9134、Springer、pp.  554– 566、doi :10.1007/978-3-662-47672-7_45、ISBN 978-3-662-47671-0。
  33. ^ Bilo, Vittorio; Mavronicolas, Marios (2016)、「マルチプレイヤーゲームにおけるナッシュ均衡に関するETR完全決定問題のカタログ」、第33回国際コンピュータサイエンス理論シンポジウム論文集、LIPIcs、第47巻、Schloss Dagstuhl--Leibnitz Zentrum fuer Informatik、pp. 17:1–17:13、doi : 10.4230/LIPIcs.STACS.2016.17、ISBN 978-3-95977-001-9。
  34. ^ Bilo, Vittorio; Mavronicolas, Marios (2017)、「対称マルチプレイヤーゲームにおける対称ナッシュ均衡に関するETR完全決定問題」、第34回国際コンピュータサイエンス理論シンポジウム論文集、LIPIcs、第66巻、Schloss Dagstuhl--Leibnitz Zentrum fuer Informatik、pp. 13:1–13:14、doi : 10.4230/LIPIcs.STACS.2017.13、ISBN 978-3-95977-028-6。
  35. ^ Herrmann, Christian; Sokoli, Johanna; Ziegler, Martin (2013)、「実非決定性多時間Blum-Shub-Smaleマシンにおけるクロス積項の充足可能性は完全である」、第6回機械・計算・普遍性会議(MCU'13)の議事録、第128巻、arXiv : 1309.1043、doi : 10.4204/EPTCS.128、S2CID  2151889。
  36. ^ Hoffmann, Udo (2016)、「平面傾斜数」、第28回カナダ計算幾何学会議論文集 (CCCG 2016)。
  37. ^ Schaefer, Marcus (2021)、「RAC描画可能性は完全である」、第29回グラフ描画およびネットワーク可視化国際シンポジウム (GD 2021) の議事録、arXiv : 2107.11663 ∃ R {\displaystyle \exists \mathbb {R} }
  38. ^ ロバート・ブライデル;ギアツ、フロリス。ヴァン・デン・ブッシュ、ヤン。 Weerwag、Timmy (2019)、「行列のクエリ言語の表現力について」、データベース システム上の ACM トランザクション、44 (4)、ACM: 15:1–15:31、arXiv : 1709.08359、doi :10.1145/3331445、hdl : 1942/30378、S2CID  204714822。
  39. ^ Bertsimas, Dimitris; Cory-Wright, Ryan; Pauphilet, Jean (2021)、「混合射影円錐最適化：ランク制約のモデリングのための新しいパラダイム」、オペレーションズ・リサーチ、70 (6): 3321– 3344、arXiv : 2009.10395、doi :10.1287/opre.2021.2182、S2CID  221836263。
Retrieved from "https://en.wikipedia.org/w/index.php?title=Existential_theory_of_the_reals&oldid=1301706803"