Decision procedures for elementary sublanguages of set theory. V. Multilevel syllogistic extended by the general union operator (Q1096608)

[For Part IV see Commun. Pure Appl. Math. 40, 37-77 (1987; Zbl 0595.03007).] Quantifier free formulas are Boolean combinations of the following atomic expressions: \(x=y\cup z\), \(x=y\setminus z\), \(x\in y\), \(x=\emptyset\), \(u=Un(y)\) (here \(u=Un(y)\) is intended to mean the set u is the union of the set y). A standard interpretation for a quantifier free formula is a function which assigns to every variable x a set Mx. A set of quantifier free formulas is satisfiable if there is some (standard) interpretation which makes all the formulas in the set true. In this paper an algorithm is presented for deciding the satisfiability of quantifier free formulas.