We study how to preserve universal termination besides computed answer substitutions while transforming definite programs. We consider the unfold operation both alone and combined with the introduction of a new definition and fold operations. We prove that unfold always preserves universal termination. Moreover we define a restricted version of the Tamaki-Sato's transformation sequence and show that it preserves universal termination as well.
I documenti in ARCA sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.