and C. Fermuller 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.
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 15 Jul 96
Part of the OUP Journals World Wide Web service.
Copyright Oxford University Press, 1996