Deciding the real numbers theory


The real numbers logic language is the set of all well-formed closed formulas written with the following symbols :
  • rational numbers;
  • 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 decidable.

Algorithm of quantification elimination for deciding the real numbers theory

Remark :
This explaination looks like a gamebook. :)

Contact :


Bibliography: this gamebook is inspired by the Chapter 1, paragraph 3 from "Foundations of Mathematics" from Erwin Engeler, edition Springer-Verlag.