Please use this identifier to cite or link to this item:
|Title:||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|
|Appears in Collections:||Fulltext Publications|
Files in This Item:
|Minimal_Model_Generation_with_Positive_Unit_Hyper-.pdf||343.49 kB||Adobe PDF||View/Open|
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.