# Strong Equivalence and Program Structure in Arguing Essential Equivalence between Logic Programs

## TL;DR

This paper explores formal relationships between different answer set programs, providing theoretical results and a system for automatic program rewriting to improve efficiency in logic programming.

## Contribution

It introduces formal results relating program rewritings and proves the correctness of an automatic rewriting system for answer set programs.

## Key findings

- Formal links between answer set program rewritings
- Proof of correctness for the Projector system
- Enhanced understanding of program equivalence and structure

## Abstract

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