Semantic tableaux with equality (Q2785839)

This article is a very good survey of deduction methods based on semantic tableaux, and the approaches to enrich semantic tableaux with equality reasoning. It covers ground semantic tableaux, semantic tableaux with free variables, and semantic tableaux with universal variables. For equality reasoning in the context of semantic tableaux it considers methods based on adding expansion rules for equality and methods based on \(E\)-unification. Depending on the type of tableaux, the latter can be universal \(E\)-unification, rigid \(E\)-unification, or mixed universal and rigid \(E\)-unification. The paper can be recommended as introductory reading for starting research in equality reasoning in the context of semantic tableaux. On the other hand, somebody interested in equality reasoning should also consult other sources, e.g.:NEWLINENEWLINENEWLINE\textit{N. Dershowitz} and \textit{J.-P. Jouannaud}, ``Rewrite systems'' [in: J. van Leeuwen (ed.), Handbook of Theoretical Computer Science, Vol. B, 243-320 (1990; Zbl 0714.68001)],NEWLINENEWLINENEWLINE\textit{D. A. Plaisted}, ``Equational reasoning and term rewriting systems'' [in: D. M. Gabbay et al. (eds.), Handbook of Logic in Artificial Intelligence and Logic Programming, Vol. 1, 273-364 (1993; Zbl 0808.68027)],NEWLINENEWLINENEWLINE\textit{M. P. Bonacina} and \textit{J. Hsiang}, ``Towards a foundation of completion procedures as semidecision procedures'' [Theor. Comput. Sci. 146, 199-242 (1995; Zbl 0873.68102)].