Various commonly occurring decidable extensions of multi-level syllogistic

Engaging formal proofs, such as those founding the field of mathematical analysis, very often rely on routine forms of set-theoretical reasoning which a human expert exploits almost unconsciously and a computerized proof-checker must encompass as basic inferential services. This paper focuses on situations when such reasoning services are implemented as decision algorithms for fragments of set theory. We will start with a specific satisfiability test which, despite being rather limited in the constructs it can deal with, has demonstrated very useful in practice (whereas decision algorithms for more expressive sub-languages of set theory tend to be utterly unmanageable due to their high complexity). We will address the issue: how can we extend the realm of applicability of this decision algorithm without substantial reworking of its internals, but rather via systematic reprocessing techniques? The method which we will propose as an answer is already at work in a proof-verification system which we are currently developing.