Complexity Assessments For Decidable Fragments Of Set Theory. I: A Taxonomy For The Boolean Case

We report on an investigation aimed at identifying small fragments of set theory (typically, sublanguages of Multi-Level Syllogistic) endowed with polynomial-time satisfiability decision tests, potentially useful for automated proof verification. Leaving out of consideration the membership relator is an element of for the time being, in this paper we provide a complete taxonomy of the polynomial and the NP-complete fragments involving, besides variables intended to range over the von Neumann set-universe, the Boolean operators boolean OR,boolean AND,\, the Boolean relators subset of, not subset of, = not equal, and the predicates '. = circle divide' and 'Disj(.,.)', meaning 'the argument set is empty' and 'the arguments are disjoint sets', along with their opposites '. not equal circle divide'and '(sic)Disj(.,.)'. We also examine in detail how to test for satisfiability the formulae of six sample fragments: three sample problems are shown to be NP-complete, two to admit quadratic-time decision algorithms, and one to be solvable in linear time.