Algorithm of quantification elimination for deciding the real numbers theory
Imagine your have your formula, e.g ∃x, x² + 5x + 2 = 0 or
∀x, (x>0 → ∃y, x = y²).
First, rewrite your formula such that it contains only:
- real numbers operators + and ×;
- predicates of the form P = 0, Q > 0 ;
- Boolean operators and, or;
- existential quantifier ∃;
- and the negation connectors notonly appear just in front ∃.
Now, look at a subformula ∃x,
φ where φ does not contain any other quantification ∃