3. Tableau Model Elimination

Abstract

Model elimination [Loveland, 1968] is a calculus, which is the base of numerous proof procedures for first order deduction. There are high speed theorem provers, like METEOR [Astrachan and Stickel, 1992] or SETHEO [Letz et al., 1992]. The implementation of model elimination provers can take advantage of techniques developed for Prolog. For instance, SETHEO compiles the input clause set into a generalized WAM architecture. Stickel’s Prolog technology theorem proving system (PTTP, [Stickel, 1988]) uses Horn clauses as an intermediate language, which can even be processed by conventional Prolog systems [Stickel, 1989].