Minimal model generation with positive unit hyper-resolution tableaux

Abstract

Herbrand models for clausal theories are useful in several areas of computer science. In most cases, however, the conventional model generation algorithms are inappropriate because they generate nonminimal Herbrand models and can be ine cient. This article describes a novel approach for generating minimal Herbrand models of clausal theories. The approach builds upon positive unit hyper-resolution (PUHR) tableaux, that are in general smaller than conventional tableaux. To generate only minimal Herbrand models, a complement splitting expansion rule and a speci c search strategy are applied. The proposed procedure is optimal in the sense that each minimal model is generated only once, and nonminimal models are rejected before their complete construction. First measurements on an implementation point to its e ciency