We continue our investigation aimed at spotting small frag- ments of Set Theory (in this paper, sublanguages of Boolean Set The- ory) 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 vari- ables 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 decidable cubic-time satisfiability 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 the predicates ‘ = ∅’ and ‘Disj( , )’, meaning ‘the argument is empty’ and ‘the arguments are disjoint sets’, along with their opposites ‘ ̸= ∅’ and ‘¬Disj( , )’. Those richer languages are ‘polynomial maximal’, in the sense that all languages strictly containing them have an NP-hard satisfiability problem.
