Non-Horn magic sets(NHM) method transforms a given clause set into a set of clauses simulating backward reasoning and those for controlling forward reasoning so as to prune the search space. To preserve the range-restricted condition, the transformation needs to attach an adornment to a predicate to show binding information of its arguments. However, introducing adornments causes combinatorial explosion of the number of transformed clauses because the number of adornments may increase exponentially. This paper presents four methods to decrease the number of transformed clauses: (1) obtaining necessary adornments by statical analysis, (2) extracting minimal adornments from necessary adornments, (3) calculating necessary adornments dynamically, and (4) transformation without adornments. These methods have been implemented on a UNIX workstation. We evaluated their effects by proving some problems in the TPTP problem library.
|Number of pages||6|
|Journal||Research Reports on Information Science and Electrical Engineering of Kyushu University|
|Publication status||Published - Sept 1 1997|
All Science Journal Classification (ASJC) codes
- Computer Science(all)
- Electrical and Electronic Engineering