We recently undertook an investigation aimed at identifying
small fragments of set theory (which in most cases are 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 ∈ for the time being, in
this note 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 ∪, ∩, , the
Boolean relators ⊆, /⊆, =, /=, and the predicates ‘· = ∅’ and ‘Disj(·, ·)’,
meaning ‘the argument set is empty’ and ‘the arguments are disjoint
sets’, along with their opposites ‘· /= ∅’ and ‘¬Disj(·, ·)’.
