B. Beckert Institute for Logic, Complexity and Deduction Systems, University of Karlsruhe, Am Fasanengarten 5, 76128and Karlsruhe, Germany. Email: firstname.lastname@example.org WWW: http://i12.www.ira.uka.de/beckert
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.
: Theorem proving, automated deduction, semantic tableaux, equality, E-unification
Part of the OUP Journal of Logic and Computation WWW service
Click here to register with OUP.
This page is maintained by OUP admin
Last updated 25 Jan 97
Part of the OUP Journals World Wide Web service.
Copyright Oxford University Press, 1997