Volume 7: January - December 1997

Issue 1: 1997


Semantic tableaux with equality

  • Semantic tableaux with equality
  • B. Beckert Institute for Logic, Complexity and Deduction Systems, University of Karlsruhe, Am Fasanengarten 5, 76128 Karlsruhe, Germany. Email: beckert@ira.uka.de and 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.

    Keywords: Theorem proving, automated deduction, semantic tableaux, equality, E-unification

    Pages: 39 - 58

    Part of the OUP Journal of Logic and Computation WWW service

    General Information

    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