Semantics hold transformation for prolog

The application of program transformation method to logic program is mainly based on such theory, namely, Fold/Unfold transformation holds the least Herbrand model semantics and the semantics of answer substitution set of logic program. However, when the leftmost computing rule and depth-first searching rule of standard Prolog systems are adopted for implementing logic programs, the semantics of original program cannot necessarily be held by transformed program. Moreover, the proof of semantic equivalence of the program is often difficult to understand and to read. By the style of algorithm for computing answer substitution sequence relating to the node of leaves in SLD-tree, the author puts forward a semantics definition of Prolog which is not difficult to understand; and then, gives the rules for semantics hold transformation and offers proof.