Le Matematiche (Nov 1988)
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.