A Sound Framework for delta-rule Variants in Free Variable Semantic Tableaux

We propose a generic sound delta-rule, based on a quite general method for the construction of Skolem terms, which can be used as a common framework for proving the soundness of known variants of the delta-rule, and we compare their relative effectiveness. Attempts to instantiate some of the delta-rules present in the literature within our framework allowed us to pinpoint unsoundness problems for two of them. In both cases, we propose revised versions that are proved sound by reducing them within our framework.