Existential theory of the reals

In mathematical logic, a theory is a formal language consisting of a set of sentences written using a fixed set of symbols. The first-order theory of real closed fields has the following symbols:

• the constants 0 and 1,
• a countable collection of variables $X\_i$,
• the addition, subtraction, multiplication, and (optionally) division operations,
• symbols <, ≤, =, ≥, >, and ≠ for comparisons of real values,
• the logical connectives ∧, ∨, ¬, and ⇔,
• parentheses, and
• the universal quantifier ∀ and the existential quantifier ∃

A sequence of these symbols forms a sentence that belongs to the first-order theory of the reals if it is grammatically well formed, all its variables are properly quantified, and (when interpreted as a mathematical statement about the real numbers) it is a true statement. As Tarski showed, this theory can be described by an axiom schema and a decision procedure that is complete and effective: for every fully quantified and grammatical sentence, either the sentence or its negation (but not both) can be derived from the axioms. The same theory describes every real closed field, not just the real numbers. However, there are other number systems that are not accurately described by these axioms; in particular, the theory defined in the same way for integers instead of real numbers is undecidable, even for existential sentences (Diophantine equations) by Matiyasevich's theorem.{{citation

| last = Matiyasevich | first = Yu. V. | author-link = Yuri Matiyasevich

| contribution = Hilbert's tenth problem: Diophantine equations in the twentieth century

| doi = 10.1007/3-540-29462-7_10

| mr = 2182785

| pages = 185–213

| publisher = Springer-Verlag | location = Berlin

| title = Mathematical events of the twentieth century

| year = 2006| bibcode = 2006metc.book.....A | isbn = 978-3-540-23235-3 }}.

The existential theory of the reals is the fragment of the first-order theory consisting of sentences in which all the quantifiers are existential and they appear before any of the other symbols. That is, it is the set of all true sentences of the form

$$\backslash exists\; X\_1\; \backslash cdots\; \backslash exists\; X\_n\; \backslash ,\; F(X\_1,\backslash dots,\; X\_n),$$

where $F(X\_1,\backslash dots\; X\_n)$ is a quantifier-free formula involving equalities and inequalities of real polynomials. The decision problem for the existential theory of the reals is the algorithmic problem of testing whether a given sentence belongs to this theory; equivalently, for strings that pass the basic syntactical checks (they use the correct symbols with the correct syntax, and have no unquantified variables) it is the problem of testing whether the sentence is a true statement about the real numbers. The set of $n$-tuples of real numbers $(X\_1,\backslash dots\; X\_n)$ for which $F(X\_1,\backslash dots\; X\_n)$ is true is called a semialgebraic set, so the decision problem for the existential theory of the reals can equivalently be rephrased as testing whether a given semialgebraic set is nonempty.

In determining the time complexity of algorithms for the decision problem for the existential theory of the reals, it is important to have a measure of the size of the input. The simplest measure of this type is the length of a sentence: that is, the number of symbols it contains. However, in order to achieve a more precise analysis of the behavior of algorithms for this problem, it is convenient to break down the input size into several variables, separating out the number of variables to be quantified, the number of polynomials within the sentence, and the degree of these polynomials.

The golden ratio $\backslash varphi$ may be defined as the root of the polynomial $x^2-x-1$. This polynomial has two roots, only one of which (the golden ratio) is greater than one. Thus, the existence of the golden ratio may be expressed by the sentence

$$\backslash exists\; X\_1(\; X\_1\; >\; 1\; \backslash wedge\; X\_1\backslash times\; X\_1\; -\; X\_1\; -\; 1\; =\; 0).$$

Because the golden ratio is not transcendental, this is a true sentence, and belongs to the existential theory of the reals. The answer to the decision problem for the existential theory of the reals, given this sentence as input, is the Boolean value true.

The inequality of arithmetic and geometric means states that, for every two non-negative numbers $x$ and $y$, the following inequality holds:

$$\backslash frac\{x+y\}\{2\}\; \backslash ge\; \backslash sqrt\{xy\}.$$

As stated above, it is a first-order sentence about the real numbers, but one with universal rather than existential quantifiers, and one that uses extra symbols for division, square roots, and the number 2 that are not allowed in the first-order theory of the reals. However, by squaring both sides it can be transformed into the following existential statement that can be interpreted as asking whether the inequality has any counterexamples:

:

The answer to the decision problem for the existential theory of the reals, given this sentence as input, is the Boolean value false: there are no counterexamples. Therefore, this sentence does not belong to the existential theory of the reals, despite being of the correct grammatical form.

Alfred Tarski's method of quantifier elimination (1948) showed the existential theory of the reals (and more generally the first order theory of the reals) to be algorithmically solvable, but without an elementary bound on its complexity.{{citation

| last = Tarski | first = Alfred | author-link = Alfred Tarski

| mr = 0028796

| publisher = RAND Corporation, Santa Monica, Calif.

| title = A Decision Method for Elementary Algebra and Geometry

| year = 1948}}. The method of cylindrical algebraic decomposition, by George E. Collins (1975), improved the time dependence to doubly exponential,{{citation

| last = Collins | first = George E. | author-link = George E. Collins

| contribution = Quantifier elimination for real closed fields by cylindrical algebraic decomposition

| mr = 0403962

| pages = 134–183

| series = Lecture Notes in Computer Science

| volume = 33

| publisher = Springer-Verlag | location = Berlin

| title = Automata theory and formal languages (Second GI Conf., Kaiserslautern, 1975)

| year = 1975}}. of the form

$$L^3\; (md)^\{2^\{O(n)\}\}$$

where $L$ is the number of bits needed to represent the coefficients in the sentence whose value is to be determined, $m$ is the number of polynomials in the sentence, $d$ is their total degree, and $n$ is the number of variables.{{citation

| last = Hong

| first = Hoon

| date = September 11, 1991

| publisher = RISC Linz

| series = Technical Report

| title = Comparison of Several Decision Algorithms for the Existential Theory of the Reals

| url = ftp://crow.risc.uni-linz.ac.at/pub/techreports/1991/91-41.ps.gz

| volume = 91-41

}}{{Dead link|date=December 2019 |bot=InternetArchiveBot |fix-attempted=yes }}.

By 1988, Dima Grigoriev and Nicolai Vorobjov had shown the complexity to be exponential in a polynomial of $n$,{{citation

| last = Grigor'ev | first = D. Yu. | author-link = Dima Grigoriev

| doi = 10.1016/S0747-7171(88)80006-3

| issue = 1–2

| journal = Journal of Symbolic Computation

| mr = 949113

| pages = 65–108

| title = Complexity of deciding Tarski algebra

| volume = 5

| year = 1988| doi-access = free

}}.{{citation

| last1 = Grigor'ev | first1 = D. Yu. | author1-link = Dima Grigoriev

| last2 = Vorobjov | first2 = N. N. Jr. | author2-link = Nikolai Nikolayevich Vorobyov (mathematician)

| doi = 10.1016/S0747-7171(88)80005-1

| issue = 1–2

| journal = Journal of Symbolic Computation

| mr = 949112

| pages = 37–64

| title = Solving systems of polynomial inequalities in subexponential time

| volume = 5

| year = 1988| s2cid = 39376619 | url = https://hal.archives-ouvertes.fr/hal-03053133/file/grigoriev1_201205%5B1%5D.pdf }}.

$$L(md)^\{n^2\}$$

and in a sequence of papers published in 1992 James Renegar improved this to a singly exponential dependence {{nobr|1=on $n$,{{citation

| last = Renegar | first = James

| doi = 10.1016/S0747-7171(10)80003-3

| issue = 3

| journal = Journal of Symbolic Computation

| mr = 1156882

| pages = 255–299

| title = On the computational complexity and geometry of the first-order theory of the reals. I. Introduction. Preliminaries. The geometry of semi-algebraic sets. The decision problem for the existential theory of the reals

| volume = 13

| year = 1992| doi-access = free

}}.{{citation

| last = Renegar | first = James

| doi = 10.1016/S0747-7171(10)80004-5

| issue = 3

| journal = Journal of Symbolic Computation

| mr = 1156883

| pages = 301–327

| title = On the computational complexity and geometry of the first-order theory of the reals. II. The general decision problem. Preliminaries for quantifier elimination

| volume = 13

| year = 1992| doi-access = free

}}.{{citation

| last = Renegar | first = James

| doi = 10.1016/S0747-7171(10)80005-7

| issue = 3

| journal = Journal of Symbolic Computation

| mr = 1156884

| pages = 329–352

| title = On the computational complexity and geometry of the first-order theory of the reals. III. Quantifier elimination

| volume = 13

| year = 1992| doi-access = free

}}.}}

$$L\backslash log\; L\backslash log\backslash log\; L(md)^\{O(n)\}.$$

In the meantime, in 1988, John Canny described another algorithm that also has exponential time dependence, but only polynomial space complexity; that is, he showed that the problem could be solved in PSPACE.

The asymptotic computational complexity of these algorithms may be misleading, because in practice they can only be run on inputs of very small size. In a 1991 comparison, Hoon Hong estimated that Collins' doubly exponential procedure would be able to solve a problem whose size is described by setting all the above parameters to 2, in less than a second, whereas the algorithms of Grigoriev, Vorbjov, and Renegar would instead take more than a million years. In 1993, Joos, Roy, and Solernó suggested that it should be possible to make small modifications to the exponential-time procedures to make them faster in practice than cylindrical algebraic decision, as well as faster in theory.{{citation

| last1 = Heintz | first1 = Joos | author1-link = Joos Ulrich Heintz

| last2 = Roy | first2 = Marie-Françoise | author2-link = Marie-Françoise Roy

| last3 = Solernó | first3 = Pablo

| doi = 10.1093/comjnl/36.5.427

| issue = 5

| journal = The Computer Journal

| mr = 1234114

| pages = 427–431

| title = On the theoretical and practical complexity of the existential theory of reals

| volume = 36

| year = 1993| doi-access = free

}}. However, as of 2009, it was still the case that general methods for the first-order theory of the reals remained superior in practice to the singly exponential algorithms specialized to the existential theory of the reals.{{citation

| last1 = Passmore | first1 = Grant Olney

| last2 = Jackson | first2 = Paul B.

| contribution = Combined decision techniques for the existential theory of the reals

| doi = 10.1007/978-3-642-02614-0_14

| pages = 122–137

| publisher = Springer-Verlag

| series = Lecture Notes in Computer Science

| title = Intelligent Computer Mathematics: 16th Symposium, Calculemus 2009, 8th International Conference, MKM 2009, Held as Part of CICM 2009, Grand Bend, Canada, July 6-12, 2009, Proceedings, Part II

| volume = 5625

| year = 2009| s2cid = 1160351

| url = https://www.research.ed.ac.uk/portal/en/publications/combined-decision-techniques-for-the-existential-theory-of-the-reals(b2cc91c8-6b87-4146-bab6-a2021b3006b2).html

| hdl = 20.500.11820/b2cc91c8-6b87-4146-bab6-a2021b3006b2

| isbn = 978-3-642-02613-3

| hdl-access = free

}}.

Several problems in computational complexity and geometric graph theory may be classified as complete for the existential theory of the reals. That is, every problem in the existential theory of the reals has a polynomial-time many-one reduction to an instance of one of these problems, and in turn these problems are reducible to the existential theory of the reals.

A number of problems of this type concern the recognition of intersection graphs of a certain type. In these problems, the input is an undirected graph; the goal is to determine whether geometric shapes from a certain class of shapes can be associated with the vertices of the graph in such a way that two vertices are adjacent in the graph if and only if their associated shapes have a non-empty intersection. Problems of this type that are complete for the existential theory of the reals include

recognition of intersection graphs of line segments in the plane,{{citation

| last1 = Kratochvíl | first1 = Jan | author1-link = Jan Kratochvíl

| last2 = Matoušek | first2 = Jiří | author2-link = Jiří Matoušek (mathematician)

| doi = 10.1006/jctb.1994.1071

| issue = 2

| journal = Journal of Combinatorial Theory, Series B

| mr = 1305055

| pages = 289–315

| title = Intersection graphs of segments

| volume = 62

| year = 1994| doi-access = free

}}.{{cite arXiv| last = Matoušek | first = Jiří | author-link = Jiří Matoušek (mathematician) | title = Intersection graphs of segments and $\backslash exists\backslash mathbb\{R\}$ | year = 2014 | class = cs.CG | eprint = 1406.2636|mode=cs2}}

recognition of unit disk graphs,{{citation|last1=Kang|first1=Ross J.|last2=Müller|first2=Tobias|year=2011|contribution=Sphere and dot product representations of graphs|title=Proceedings of the Twenty-Seventh Annual Symposium on Computational Geometry (SCG'11), June 13–15, 2011, Paris, France|pages=308–314}}.

and recognition of intersection graphs of convex sets in the plane.

For graphs drawn in the plane without crossings, Fáry's theorem states that one gets the same class of planar graphs regardless of whether the edges of the graph are drawn as straight line segments or as arbitrary curves. But this equivalence does not hold true for other types of drawing. For instance, although the crossing number of a graph (the minimum number of crossings in a drawing with arbitrarily curved edges) may be determined in NP, it is complete for the existential theory of the reals to determine whether there exists a drawing achieving a given bound on the rectilinear crossing number (the minimum number of pairs of edges that cross in any drawing with edges drawn as straight line segments in the plane).{{citation

| last = Bienstock | first = Daniel

| doi = 10.1007/BF02574701 | doi-access=free

| issue = 5

| journal = Discrete & Computational Geometry

| mr = 1115102

| pages = 443–459

| title = Some provably hard crossing number problems

| volume = 6

| year = 1991| s2cid = 38465081}}.

It is also complete for the existential theory of the reals to test whether a given graph can be drawn in the plane with straight line edges and with a given set of edge pairs as its crossings, or equivalently, whether a curved drawing with crossings can be straightened in a way that preserves its crossings.{{citation

| last = Kynčl | first = Jan

| doi = 10.1007/s00454-010-9320-x | doi-access=free

| issue = 3

| journal = Discrete & Computational Geometry

| mr = 2770542

| pages = 383–399

| title = Simple realizability of complete abstract topological graphs in P

| volume = 45

| year = 2011| s2cid = 12419381}}.

Other complete problems for the existential theory of the reals include:

• the art gallery problem of finding the smallest number of points from which all points of a given polygon are visible.{{citation | last1 = Abrahamsen | first1 = Mikkel | last2 = Adamaszek | first2 = Anna | last3 = Miltzow | first3 = Tillmann | doi = 10.1145/3486220 | issue = 1 | journal = Journal of the ACM | mr = 4402363 | pages = A4:1–A4:70 | title = The art gallery problem is $\backslash exists\backslash Bbb\; R$-complete | volume = 69 | year = 2022| hdl = 1874/424939 | hdl-access = free }}
• training neural networks.{{citation | last1 = Abrahamsen | first1 = Mikkel | last2 = Kleist | first2 = Linda | last3 = Miltzow | first3 = Tillmann | editor1-last = Ranzato | editor1-first = Marc'Aurelio | editor2-last = Beygelzimer | editor2-first = Alina | editor3-last = Dauphin | editor3-first = Yann N. | editor4-last = Liang | editor4-first = Percy | editor5-last = Vaughan | editor5-first = Jennifer Wortman | arxiv = 2102.09798 | contribution = Training neural networks is $\backslash exists\backslash R$-complete | contribution-url = https://proceedings.neurips.cc/paper/2021/hash/9813b270ed0288e7c0388f0fd4ec68f5-Abstract.html | pages = 18293–18306 | title = Advances in Neural Information Processing Systems 34: Annual Conference on Neural Information Processing Systems 2021, NeurIPS 2021, December 6-14, 2021, virtual | year = 2021}}
• the packing problem of deciding whether a given set of polygons can fit in a given square container.{{citation | last1 = Abrahamsen | first1 = Mikkel | last2 = Miltzow | first2 = Tillmann | last3 = Seiferth | first3 = Nadja | arxiv = 2004.07558 | contribution = Framework for $\backslash exists\backslash mathbb\{R\}$-completeness of two-dimensional packing problems | doi = 10.1109/FOCS46700.2020.00098 | pages = 1014–1021 | publisher = IEEE | title = 61st IEEE Annual Symposium on Foundations of Computer Science, FOCS 2020, Durham, NC, USA, November 16-19, 2020 | year = 2020| isbn = 978-1-7281-9621-3 | s2cid = 216045462 }}
• recognition of unit distance graphs, and testing whether the dimension or Euclidean dimension of a graph is at most a given value.{{citation

| last = Schaefer | first = Marcus

| editor-last = Pach | editor-first = János | editor-link = János Pach

| contribution = Realizability of graphs and linkages

| doi = 10.1007/978-1-4614-0110-0_24

| pages = 461–482

| publisher = Springer-Verlag

| title = Thirty Essays on Geometric Graph Theory

| year = 2013| isbn = 978-1-4614-0109-4

}}.

• stretchability of pseudolines (that is, given a family of curves in the plane, determining whether they are homeomorphic to a line arrangement);{{citation

| last = Mnëv | first = N. E.

| contribution = The universality theorems on the classification problem of configuration varieties and convex polytopes varieties

| doi = 10.1007/BFb0082792

| location = Berlin

| mr = 970093

| pages = 527–543

| publisher = Springer-Verlag

| series = Lecture Notes in Mathematics

| title = Topology and Geometry — Rohlin Seminar

| volume = 1346

| isbn = 978-3-540-50237-1

| year = 1988}}.{{citation

| last = Shor | first = Peter W. | author-link = Peter Shor

| contribution = Stretchability of pseudolines is NP-hard

| location = Providence, RI

| mr = 1116375

| pages = 531–554

| publisher = American Mathematical Society

| series = DIMACS Series in Discrete Mathematics and Theoretical Computer Science

| title = Applied Geometry and Discrete Mathematics

| volume = 4

| year = 1991}}.

• both weak and strong satisfiability of geometric quantum logic in any fixed dimension >2;{{citation

| last1 = Herrmann | first1 = Christian

| last2 = Ziegler | first2 = Martin

| doi = 10.1145/2869073

| year = 2016

| contribution = Computational Complexity of Quantum Satisfiability

| title = Journal of the ACM

| volume = 63

| number = 19| pages = 1–31

| arxiv = 1004.1696

| s2cid = 2253943

}}.

• Model checking interval Markov chains with respect to unambiguous automata.{{citation

| last1 = Benedikt | first1 = Michael

| last2 = Lenhardt | first2 = Rastislav

| last3 = Worrell | first3 = James

| doi = 10.1007/978-3-642-36742-7_3

| year = 2013

| contribution = LTL Model Checking of Interval Markov Chains

| title = Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2013

| series = Lecture Notes in Computer Science

| volume = 7795

| pages = 32–46| isbn = 978-3-642-36741-0

}}

• the algorithmic Steinitz problem (given a lattice, determine whether it is the face lattice of a convex polytope), even when restricted to 4-dimensional polytopes;{{citation

| last1 = Björner | first1 = Anders | author1-link = Anders Björner

| last2 = Las Vergnas | first2 = Michel | author2-link = Michel Las Vergnas

| last3 = Sturmfels | first3 = Bernd | author3-link = Bernd Sturmfels

| last4 = White | first4 = Neil

| last5 = Ziegler | first5 = Günter M. | author5-link = Günter Ziegler

| at = Corollary 9.5.10, p. 407

| isbn = 0-521-41836-4

| location = Cambridge

| mr = 1226888

| publisher = Cambridge University Press

| series = Encyclopedia of Mathematics and its Applications

| title = Oriented Matroids

| volume = 46

| year = 1993}}.{{citation

| last1 = Richter-Gebert | first1 = Jürgen

| last2 = Ziegler | first2 = Günter M. | author2-link = Günter M. Ziegler

| doi = 10.1090/S0273-0979-1995-00604-X

| issue = 4

| journal = Bulletin of the American Mathematical Society

| mr = 1316500

| pages = 403–412

| series = New Series

| title = Realization spaces of 4-polytopes are universal

| volume = 32

| year = 1995| arxiv = math/9510217| bibcode = 1995math.....10217R

| s2cid = 7940964

}}.

• realization spaces of arrangements of certain convex bodies{{citation

| last1 = Dobbins | first1 = Michael Gene

| last2 = Holmsen | first2 = Andreas

| last3 = Hubard | first3 = Alfredo

| arxiv = 1412.0371

| doi = 10.1007/s00454-017-9869-8

| issue = 1

| journal = Discrete & Computational Geometry

| mr = 3658327

| pages = 1–29

| title = Realization spaces of arrangements of convex bodies

| volume = 58

| year = 2017| s2cid = 39856606

}}.

• various properties of Nash equilibria of multi-player games{{citation

| last1 = Garg | first1 = Jugal

| last2 = Mehta | first2 = Ruta

| last3 = Vazirani | first3 = Vijay V. | author3-link = Vijay Vazirani

| last4 = Yazdanbod | first4 = Sadra

| pages = 554–566

| series = Lecture Notes in Computer Science

| title = Proc. 42nd International Colloquium on Automata, Languages, and Programming (ICALP)

| contribution = ETR-Completeness for Decision Versions of Multi-player (Symmetric) Nash Equilibria

| publisher = Springer

| volume = 9134

| doi = 10.1007/978-3-662-47672-7_45

| year = 2015| isbn = 978-3-662-47671-0

}}.{{citation

| last1 = Bilo | first1 = Vittorio

| last2 = Mavronicolas | first2 = Marios

| pages = 17:1–17:13

| series = LIPIcs

| title = Proceedings of 33rd International Symposium on Theoretical Aspects of Computer Science

| contribution = A Catalog of ETR-Complete Decision Problems about Nash Equilibria in Multi-Player Games

| publisher = Schloss Dagstuhl--Leibnitz Zentrum fuer Informatik

| doi = 10.4230/LIPIcs.STACS.2016.17

| year = 2016| volume = 47

| doi-access = free

| isbn = 978-3-95977-001-9

}}.{{citation

| last1 = Bilo | first1 = Vittorio

| last2 = Mavronicolas | first2 = Marios

| pages = 13:1–13:14

| series = LIPIcs

| title = Proceedings of 34th International Symposium on Theoretical Aspects of Computer Science

| contribution = ETR-Complete Decision Problems about Symmetric Nash Equilibria in Symmetric Multi-Player Games

| publisher = Schloss Dagstuhl--Leibnitz Zentrum fuer Informatik

| url = http://drops.dagstuhl.de/opus/volltexte/2017/7020

| year = 2017| volume = 66

| doi = 10.4230/LIPIcs.STACS.2017.13

| doi-access = free

| isbn = 978-3-95977-028-6

}}.

• embedding a given abstract complex of triangles and quadrilaterals into three-dimensional Euclidean space;{{citation|title=Computational geometry column 62|first=Jean|last=Cardinal|journal=SIGACT News|volume=46|issue=4|date=December 2015|pages=69–78|doi=10.1145/2852040.2852053|s2cid=17276902}}.
• embedding multiple graphs on a shared vertex set into the plane so that all the graphs are drawn without crossings;
• recognizing the visibility graphs of planar point sets;
• (projective or non-trivial affine) satisfiability of an equation between two terms over the cross product;{{citation

| last1 = Herrmann | first1 = Christian

| last2 = Sokoli | first2 = Johanna

| last3 = Ziegler | first3 = Martin

| doi = 10.4204/EPTCS.128

| year = 2013

| contribution = Satisfiability of cross product terms is complete for real nondeterministic polytime Blum-Shub-Smale machines

| title = Proceedings of the 6th Conference on Machines, Computations and Universality (MCU'13)| volume = 128

| s2cid = 2151889

| doi-access = free| arxiv = 1309.1043}}.

• determining the minimum slope number of a non-crossing drawing of a planar graph;{{citation

| last = Hoffmann | first = Udo

| contribution = The planar slope number

| title = Proceedings of the 28th Canadian Conference on Computational Geometry (CCCG 2016)

| year = 2016}}.

• recognizing graphs that can be drawn with all crossings at right angles;{{citation|first=Marcus|last=Schaefer|year=2021|contribution=RAC-drawability is $\backslash exists\backslash mathbb\{R\}$-complete|arxiv=2107.11663|title=Proceedings of the 29th International Symposium on Graph Drawing and Network Visualization (GD 2021)}}
• the partial evaluation problem for the MATLANG+eigen matrix query language.{{citation

| last1 = Brijder | first1 = Robert

| last2 = Geerts | first2 = Floris

| last3 = Van den Bussche | first3 = Jan

| last4 = Weerwag | first4 = Timmy

| pages = 15:1–15:31

| journal = ACM Transactions on Database Systems

| title = On the Expressive Power of Query Languages for Matrices.

| publisher = ACM

| volume = 44

| number = 4

| doi = 10.1145/3331445

| year = 2019| hdl = 1942/30378

| s2cid = 204714822

| url = https://drops.dagstuhl.de/opus/volltexte/2018/8600/

| hdl-access = free

}}.

• the low-rank matrix completion problem.{{cite journal

| last1 = Bertsimas | first1 = Dimitris

| last2 = Cory-Wright | first2 = Ryan

| last3 = Pauphilet | first3 = Jean

| title = Mixed-Projection Conic Optimization: A New Paradigm for Modeling Rank Constraints

| journal = Operations Research

| arxiv = 2009.10395

| year = 2021 | volume = 70

| issue = 6

| pages = 3321–3344

| doi = 10.1287/opre.2021.2182

| s2cid = 221836263

|mode=cs2}}.

Based on this, the complexity class $\backslash exists\; \backslash mathbb\{R\}$ has been defined as the set of problems having a polynomial-time many-one reduction to the existential theory of the reals.{{citation|first=Marcus|last=Schaefer|contribution=Complexity of some geometric and topological problems|contribution-url=http://ovid.cs.depaul.edu/documents/convex.pdf|title=Graph Drawing, 17th International Symposium, GD 2009, Chicago, IL, USA, September 2009, Revised Papers|series=Lecture Notes in Computer Science|publisher=Springer-Verlag|volume=5849|pages=334–344|doi=10.1007/978-3-642-11805-0_32|year=2010|doi-access=free|isbn=978-3-642-11804-3 }}.

• Hilbert's tenth problem, on the (undecidable) existential theory of the integers

{{reflist|colwidth=30em}}

Category:Formal theories of arithmetic

Category:Computational complexity theory

Category:Real algebraic geometry