Volume 6: January - December 1996

Issue 2: April 1996


Hyperresolution and automated model building

  • Hyperresolution and automated model building
  • C. Fermuller and A. Leitsch Technische Universitat Wien, 1040 Vienna, Austria


    Building on previous results that show that hyperresolution refinements may usefully be employed as decision procedures for a wide range of decidable classes of clause sets we present methods for constructing models for such sets of clauses. We show how to generate finite sets of atoms that represent Herbrand models using hyperresolution. We demonstrate that these atomic representations of models enjoy features that provide a basis for various applications in automated theorem proving. In particular, we show that the equivalence of atomic representations is decidable and that arbitrary clauses can be evaluated effectively w.r.t to the represented models. For the investigated classes we may focus on atoms with a linear term structure and show that, for this important subcase, finite models can be extracted from the sets of atoms generated by hyperresolution. We emphasize that, in contrast to model theoretic approaches, no backtracking is needed in our proof theoretic model constructing algorithm.

    Pages: 173 - 203

    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 15 Jul 96

    Part of the OUP Journals World Wide Web service.

    Copyright Oxford University Press, 1996