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
- Tools → QE for quantifier elimination without hiding.
- Tools → Counterexample to get potentially faster feedback whether the sequent is suspected true or false.
- Tools → Find assumptions to get hints on how to strengthen the assumptions to make the sequent provable.
Learning resources