Hyper Tableau with Equality
Feng Sha-sha, Jigui Sun, Xia Wu · Journal of Jilin University · 2005
The hyper tableau calculus is capable of solving first-order logic problems with equality by introducing superposition to it, which is competent in equality reasoning. The new tableau calculus is backtrack-free as well as complete. It is an attempt at completing the machine proving of the first-order logic theorem with (equality) via the tableau calculus.