Please use this identifier to cite or link to this item: http://hdl.handle.net/20.500.11889/2096
Title: Minimal model generation with positive unit hyper-resolution tableaux
Authors: Bry, Francois
Yahya, Adnan
Issue Date: May-1996
Publisher: ResearchGate
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
URI: http://hdl.handle.net/20.500.11889/2096
Appears in Collections:Fulltext Publications

Files in This Item:
File Description SizeFormat 
Minimal_Model_Generation_with_Positive_Unit_Hyper-.pdf343.49 kBAdobe PDFView/Open


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.