Some methods to decrease the number of clauses obtained by Non-Horn magic sets transformation and their evaluation

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.