TABLEAUX '98 Bernhard Beckert and Ulrike Hartmer Set theory is the common language of mathematics. Therefore, set theory plays an important role in many important applications of automated deduction. In this paper, we present an improved tableau calculus for the decidable fragment of set theory called multi-level syllogistic with singleton (MLSS). Furthermore, we describe an extension of our calculus for the bigger fragment consisting of MLSS enriched with free (uninterpreted) function symbols (MLSSF).