The liberalized δ-rule in free variable semantic tableaux
In this paper we have a closer look at one of the rules of the tableau calculus presented by Fitting , 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 . 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.