A New Clausal Class Decidable by Hyperresolution

Georgieva, L. and Hustadt, U. and Schmidt, R. A. (Jul. 2002)

Preprint CSPP-18, Department of Computer Science, University of Manchester. Also to appear in Proc. CADE'2002, LNAI, Springer. BiBTeX, Postscript.

In this paper we define a new clausal class, called BU, which can be decided by hyperresolution with splitting. We also consider the model generation problem for BU and show that hyperresolution plus splitting can also be used as a Herbrand model generation procedure for BU and, furthermore, that the addition of a local minimality test allows us to generate only minimal Herbrand models for clause sets in BU. In addition, we investigate the relationship of BU to other solvable classes.


Renate A. Schmidt
Home | Publications | Tools | FM Group | School | Man Univ

Last modified: 10 Jul 2002
Copyright © 2002 Renate A. Schmidt, School of Computer Science, Man Univ, schmidt@cs.man.ac.uk