Improving example-guided unfolding

Abstract

It has been observed that the addition of clauses learned by explanation-based generalization may degrade, rather than improve, the efficiency of a logic program. There are three reasons for the degradation: i) increased unification cost ii) increased inter-clause repetition of goal calls iii) increased redundancy. There have been several approaches to solve (or reduce) these problems. However, previous techniques that solve the redundancy problem do in fact increase the two first problems. Hence, the benefit of avoiding redundancy might be outweighed by the cost associated with these techniques. A solution to this problem is presented: the algorithm EGU II, which is a reformulation of one of the previous techniques (Example-Guided Unfolding). The algorithm is based upon the application of program transformation rules (definition, unfolding and folding) and is shown to preserve the equivalence of the domain theory. Experimental results are presented showing that the cost of avoiding redundancy is significantly reduced by EGU II, and that even when the redundancy problem is not present, the technique can be superior to adding clauses redundantly.