Semantic tableaux with equality
Bernhard Beckert · Journal of Logic and Computation · 1997
This paper tries to identify the basic problems encountered in handling equality in the semantic tableau framework, and to describe the state of the art in solving these problems. The two main paradigms for handling equality are compared: adding new tableau expansion rules and using E-unification algorithms.