Another important problem was exemplified in (6.12). Consider the set of all Tarski sentences of the form (6.9), which may or may not have free variables. Can an algorithm be developed that takes a Tarski sentence and produces an equivalent quantifier-free formula ? Let denote the free variables. To be equivalent, both must take on the same true values over , which is the set of all assignments for the free variables.
Given a Tarski sentence, , the quantifier-elimination problem is to find a quantifier-free formula such that
Once again, the problem is defined on , which is uncountably infinite, but an algorithm must work with a finite representation. This will be achieved by the cell decomposition technique presented in Section 6.4.2.
Steven M LaValle 2012-04-20