An improved method for adding equality to free variable semantic tableaux

Tableau-Based theorem provers can be extended to cover many of the nonclassical logics currently used in AI research. For both, classical and nonclassical first-order logic, equality is a crucial feature to increase ex- pressivity of the object language. Unfortunately, all so far existing attempts of adding equality to semantic tableaux have been more or less experimental and turn out to be useless in practice. In the present work we introduce an approach that leads much further and sets the stage for more advanced developments. We identify the problems that stem specifically from choosing semantic tableaux as a framework and state soundness and completeness results for our method.