The algorithm I use in 'EliminateVariables' is pretty ad-hoc and has built up as I throw more situations at it.

If you want to look up how the big time guys do it, I believe Mathematica's 'Reduce' performs full on quantifier elimination via cylindrical algebraic decomposition. There aren't many open-source implementations of CAD that I know of besides the venerable C-based QEPCAD.

PS: Big fan of your Neo4J tutorials. :-)