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. I n addition, we investigate the relationship of BU to other solvable classes.
CITATION STYLE
Georgieva, L., Hustadt, U., & Schmidt, R. A. (2002). A new clausal class decidable by hyperresolution. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2392, pp. 260–274). Springer Verlag. https://doi.org/10.1007/3-540-45620-1_21
Mendeley helps you to discover research relevant for your work.