L. Georgieva, U. Hustadt, R. A. Schmidt (2002b): ``A new clausal class decidable by hyperresolution.'' In A. Voronkov, editor, Proceedings of the 18th International Conference on Automated Deduction CADE-18 [Copenhagen, Denmark, 27-30 July 2002], pp. 258-272. LNAI 2392, Springer.
Abstract, BibTeX, PDF (© Springer), Abstract + PDF (Springer)

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. [an error occurred while processing this directive]