  Answer set programming is a prominent declarative programming paradigm used
in formulating combinatorial search problems and implementing different
knowledge representation formalisms. Frequently, several related and yet
substantially different answer set programs exist for a given problem.
Sometimes these encodings may display significantly different performance.
Uncovering precise formal links between these programs is often important and
yet far from trivial. This paper presents formal results carefully relating a
number of interesting program rewritings. It also provides the proof of
correctness of system Projector concerned with automatic program rewritings for
the sake of efficiency. Under consideration in Theory and Practice of Logic
Programming (TPLP).
