Projective Quantifier Elimination for Equational Constraint Solving ?

The Projective Quantifier Elimination (PQE) technique for solving equational constraints (in particular, deciding their satisfiability) that performs an algebraic-style transformation of expressions instead of handling first-order formulas is presented.