The liberalized δ-rule in free variable semantic tableaux
(Citations: 9)
In this paper we have a closer look at one of the rules of the tableau calculus presented by Fitting [4], called the d-rule. We prove that a modification of this rule, called the d+-rule, which uses fewer free variables, is also sound and complete. We examine the relationship between the d+-rule and variations of the d-rule presented by Smullyan [9]. This leads to a second proof of the soundness of the d+-rule. An example shows the relevance of this modification for building tableau-based theorem provers.