Sciweavers

Share
TABLEAUX
1998
Springer

A Tableau Calculus for Quantifier-Free Set Theoretic Formulae

11 years 5 months ago
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).
Bernhard Beckert, Ulrike Hartmer
Added 06 Aug 2010
Updated 06 Aug 2010
Type Conference
Year 1998
Where TABLEAUX
Authors Bernhard Beckert, Ulrike Hartmer
Comments (0)
books