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).