A Tableau Calculus for Quantifier-Free Set Theoretic Formulae

Abstract. Set theory is the common language of mathematics. Therefore, set theory plays an important r^ole 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).

• Type: Conference
• Year: 1998
• Where: TABLEAUX
• Authors: Bernhard Beckert, Ulrike Hartmer
• Keywords: Artificial Intelligence, Decidable Fragment, Improved Tableau Calculus, Set Theory, TABLEAUX 1998