Please use this identifier to cite or link to this item: http://hdl.handle.net/20.500.11889/2100
Title: Positive unit hyperresolution tableaux and their application to minimal model generation
Authors: Bry, Francois
Yahya, Adnan
Issue Date: Jul-2000
Publisher: ResearchGate
Abstract: Minimal Herbrand models of sets of rst-order clauses are useful in several areas of computer science, e.g. automated theorem proving, program veri cation, logic programming, databases, and arti cial intelligence. In most cases, the conventional model generation algorithms are inappropriate because they generate nonminimal Herbrand models and can be ine cient. This article describes an approach for generating the minimal Herbrand models of sets of rst-order clauses. The approach builds upon positive unit hyperresolution (PUHR) tableaux, that are in general smaller than conventional tableaux. PUHR tableaux formalize the approach initially introduced with the theorem prover SATCHMO. Two minimal model generation procedures are described. The rst one expands PUHR tableaux depth- rst relying on a complement splitting expansion rule and on a form of backtracking involving constraints. A Prolog implementation, named MM-SATCHMO, of this procedure is given and its performance on benchmark suites is reported. The second minimal model generation procedure performs a breadth- rst, constrained expansion of PUHR (complement) tableaux. Both procedures are optimal in the sense that each minimal model is constructed only once, and the construction of nonminimal models is interrupted as soon as possible. They are complete in the following sense: The depth- rst minimal model generation procedure computes all minimal Herbrand models of the considered clauses provided these models are all nite. The breadth- rst minimal model generation procedure computes all nite minimal Herbrand models of the set of clauses under consideration. The proposed procedures are compared with related work in terms of both principles and performance on benchmark problems.
URI: http://hdl.handle.net/20.500.11889/2100
Appears in Collections:Fulltext Publications

Files in This Item:
File Description SizeFormat
Positive_Unit_Hyperresolution_Tableaux_and_Their_A.pdf500.6 kBAdobe PDFView/Open
Show full item record

Google ScholarTM

Check


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