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).

翻译：答案集编程是一个突出的宣示性编程模式,用于制定组合搜索问题和实施不同的知识代表形式主义。对于一个特定问题,通常存在若干相关但又大相径庭的解答成套程序。这些编码有时可能表现出显著的不同性能。这些编程之间没有准确的正式联系往往很重要,但远非微不足道。本文提出了与一些令人感兴趣的程序重写有关的正式结果。本文还提供了系统投影员为提高效率而进行自动程序重写的真实性的证据。在逻辑编程的理论和实践(TPLP)中正在考虑。