Deciding the real numbers theory
The real numbers logic language is the set of all well-formed closed formulas written with the following symbols :
real number operators :
comparaison operators :
=, >, <, ≤, ≥
boolean operators :
and, or, not,
universal and existential quantifiers :
Here are examples of well-formed closed formulas:
- ∃x, x² + 5x + 2 = 0.
- ∀x, (x>0 → ∃y, x = y²).
Deciding if such a formula is true is
Algorithm of quantification elimination for deciding the real numbers theory
This explaination looks like a
Bibliography: this gamebook is inspired by the Chapter 1, paragraph 3 from "Foundations of Mathematics" from Erwin Engeler, edition Springer-Verlag.