Smart quantifier elimination smartQE attempts to speed up QE by first expanding special functions and hiding irrelevant assumptions. It falls back to ordinary QE in case hiding was too aggressive.

See also

Learning resources