Correct transformations of logic programs

This paper describes a system of transformations that preserves the semantics of logic programs with respect to a fixed goal. We formalise some standard transformations and introduce two new transformation rules: Copying/Merge of Copies and Contextual Replacement by Equal Term. Correctness of all schemes of the transformation rules is proven. The applicability conditions of the schemes of rules are effectively decidable, that makes it useful for application in practice. Since some transformations simplify programs, the transformation system can be used for automated program transforming.