Decision procedures for elementary sublanguages of set theory. XV: Multilevel syllogistic extended by the predicate Finite and the operators singleton and \(pred_ <\) (Q912082)

[Part XVI is reviewed below (see Zbl 0698.03004).] From the authors' introduction: ``This paper gives a decision procedure for an unquantified fragment of set theory involving the constant \(\emptyset\), the Boolean set operators \(\cap\), \(\cup\), \(\setminus\), \(\{\) \(\}\) (singleton), the rank predicate, and the predicates \(=\), \(\in\), \(\subseteq\), Finite.''