Abstract: A new method of tableau with equality based on the additional tableau expansion is proposed and its sound and complete is proved. We adopt the idea of separating the tableau expansion into two stages in the method. The equality handle is independent. It r

Key words: Equality unification, Disiunctions of inequality, Equivalence classes