Quantifier elimination QE decides truth of real arithmetic formulas.

QE may potentially take a long time. Reducing the number of variables that occur in formulas helps. Use Editabbrv to simplify formulas together with hideL and hideR to hide irrelevant assumptions and alternatives prior to QE.

See also

Learning resources