Decidability results for classes of purely universal formulae and quantifiers elimination in set theory

Abstract

A general mechanism to extend decision algorithms to deal with additional predicates is described. The only conditions imposed on the predicates is stability with respect to some transitive relations.