# External Behavior of a Logic Program and Verification of Refactoring

arXiv: https://arxiv.org/abs/2305.17485 · HTML: https://mlsanity.com/paper/2305.17485/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 27 May 2023.

## Built on by (most cited first, 3 of 3)

- [SM-based Semantics for Answer Set Programs Containing Conditional Literals and Arithmetic](https://mlsanity.com/paper/2511.01753/) (2025)
- [Relating Answer Set Programming and Many-sorted Logics for Formal Verification](https://mlsanity.com/paper/2502.09230/) (2025)
- [Deductive Systems for Logic Programs with Counting](https://mlsanity.com/paper/2511.19565/) (2025)

## Abstract (arXiv)

Refactoring is modifying a program without changing its external behavior. In this paper, we make the concept of external behavior precise for a simple answer set programming language. Then we describe a proof assistant for the task of verifying that refactoring a program in that language is performed correctly.