# Modular Answer Set Programming as a Formal Specification Language

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

## Key facts

- Cited by 7 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 5 Aug 2020.

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

- [Constraint Answer Set Programming: Integrational and Translational (or SMT-based) Approaches](https://mlsanity.com/paper/2107.08252/) (2021)
- [Rethinking Answer Set Programming Templates](https://mlsanity.com/paper/2307.06382/) (2023)
- [Splitting Answer Set Programs with respect to Intensionality Statements (Extended Version)](https://mlsanity.com/paper/2503.19762/) (2025)
- [SM-based Semantics for Answer Set Programs Containing Conditional Literals and Arithmetic](https://mlsanity.com/paper/2511.01753/) (2025)
- [Tools and Methodologies for Verifying Answer Set Programs](https://mlsanity.com/paper/2208.03096/) (2022)
- [Relating Answer Set Programming and Many-sorted Logics for Formal Verification](https://mlsanity.com/paper/2502.09230/) (2025)
- [Parametric Modular Answer Set Programs Made Declarative](https://mlsanity.com/paper/2605.22716/) (2026)

## Abstract (arXiv)

In this paper, we study the problem of formal verification for Answer Set Programming (ASP), namely, obtaining a formal proof showing that the answer sets of a given (non-ground) logic program P correctly correspond to the solutions to the problem encoded by P, regardless of the problem instance. To this aim, we use a formal specification language based on ASP modules, so that each module can be proved to capture some informal aspect of the problem in an isolated way. This specification language relies on a novel definition of (possibly nested, first order) program modules that may incorporate local hidden atoms at different levels. Then, verifying the logic program P amounts to prove some kind of equivalence between P and its modular specification. Under consideration for acceptance in TPLP.