The sentences in (6.10) and (6.11) lead to
an interesting problem. Consider the set of all Tarski sentences that
have no free variables. The subset of these that are TRUE comprise
the *first-order theory of the reals*. Can an algorithm be
developed to determine whether such a sentence is true? This is
called the *decision problem* for the first-order theory of the
reals. At first it may appear hopeless because
is uncountably
infinite, and an algorithm must work with a finite set. This is a
familiar issue faced throughout motion planning. The sampling-based
approaches in Chapter 5 provided one kind of
solution. This idea could be applied to the decision problem, but the
resulting lack of completeness would be similar. It is not possible
to check all possible points in
by sampling. Instead, the
decision problem can be solved by constructing a combinatorial
representation that exactly represents the decision problem by
partitioning
into a finite collection of regions. Inside of
each region, only one point needs to be checked. This should already
seem related to cell decompositions in motion planning; it turns out
that methods developed to solve the decision problem can also conquer
motion planning.

Steven M LaValle 2020-08-14