AUTOMATIC FINITE UNFOLDING USING WELL-FOUNDED MEASURES

We elaborate on earlier work proposing general criteria to control unf olding during partial deduction of logic programs. We study several te chniques relying on more general and more powerful well-founded orderi ngs. In particular, we extend our framework to incorporate lexicograph ical priorities between argument positions in, a goal. We show that th is handles some remaining deficiencies in previous methods. We emphasi ze the development of fully automatic algorithms for finite unfolding, avoiding the use of ad hoc techniques. Through an extensive formaliza tion, we convey an understanding of the common principles underlying t he various algorithms. Finally, we exhibit how our structure-based unf olding framework can be adapted to cope with datalog-like constant man ipulating predicates in a satisfactory way.