We continue our investigation aimed at spotting small fragments of Set Theory (in this paper, sublanguages of Boolean Set Theory) that might be of use in automated proof-checkers based on the set-theoretic formalism. Here we propose a method that leads to a cubic-time satisfiability decision test for the language involving, besides variables intended to range over the von Neumann set-universe, the Boolean operator ∪ and the logical relators = and ≠. It can be seen that the dual language involving the Boolean operator ∩ and, again, the relators = and ≠, also admits a cubic-time satisfiability decision test; noticeably, the same algorithm can be used for both languages. Suitable pre-processing can reduce richer Boolean languages to the said two fragments, so that the same cubic satisfiability test can be used to treat the relators ⊆ and ⊈, and the predicates ‘’ and ‘’, meaning ‘the argument is empty’ and ‘the arguments are disjoint sets’, along with their opposites ‘’ and ‘’. Those richer languages are ‘polynomial maximal’, in the sense that each language strictly containing either of them and whose formulae are conjunctions of literals has an NP-hard satisfiability problem. A generalized version of the two said satisfiability tests can treat the relator ⊄, though at the price of a worsening of the algorithmic complexity (from cubic to quintic time).

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 ∈ 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 ∪ ∩ \, 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(•, •)’. 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.