The authors describe computational techniques for deciding formulae in set theory. The eventual aim of such a work is to automate simple proofs over a wide range of mathematical areas. This volume reports on a successful series of investigations in one of the most important sub-domains:elementary set theory.