Please use this identifier to cite or link to this item:
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
Appears in Collections:Fulltext Publications

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

Page view(s)

Last Week
Last month
checked on Jun 27, 2024


checked on Jun 27, 2024

Google ScholarTM


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