# Relating Answer Set Programming and Many-sorted Logics for Formal Verification

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 11 of its 48 references that are in the map.
- First posted on arXiv 13 Feb 2025.

## Builds on (most cited first, 11 of 11)

- [ASP-Core-2 Input Language Format](https://mlsanity.com/paper/1911.04326/) (2019)
- [Verifying Tight Logic Programs with anthem and Vampire](https://mlsanity.com/paper/2008.02025/) (2020)
- [Experimenting with robotic intra-logistics domains](https://mlsanity.com/paper/1804.10247/) (2018)
- [Modularity Aspects of Disjunctive Stable Models](https://mlsanity.com/paper/1401.3484/) (2014)
- [Modular Answer Set Programming as a Formal Specification Language](https://mlsanity.com/paper/2008.02015/) (2020)
- [First-Order Stable Model Semantics and First-Order Loop Formulas](https://mlsanity.com/paper/1401.3898/) (2014)
- [Semantics of templates in a compositional framework for building logics](https://mlsanity.com/paper/1507.06778/) (2015)
- [Verification of Locally Tight Programs](https://mlsanity.com/paper/2204.10789/) (2022)
- [External Behavior of a Logic Program and Verification of Refactoring](https://mlsanity.com/paper/2305.17485/) (2023)
- [First-Order Stable Model Semantics with Intensional Functions](https://mlsanity.com/paper/2307.10225/) (2023)
- [Rethinking Answer Set Programming Templates](https://mlsanity.com/paper/2307.06382/) (2023)

## Abstract (arXiv)

Answer Set Programming (ASP) is an important logic programming paradigm within the field of Knowledge Representation and Reasoning. As a concise, human-readable, declarative language, ASP is an excellent tool for developing trustworthy (especially, artificially intelligent) software systems. However, formally verifying ASP programs offers some unique challenges, such as 1. a lack of modularity (the meanings of rules are difficult to define in isolation from the enclosing program), 2. the ground-and-solve semantics (the meanings of rules are dependent on the input data with which the program is grounded), and 3. limitations of existing tools. My research agenda has been focused on addressing these three issues with the intention of making ASP verification an accessible, routine task that is regularly performed alongside program development. In this vein, I have investigated alternative semantics for ASP based on translations into the logic of here-and-there and many-sorted first-order logic. These semantics promote a modular understanding of logic programs, bypass grounding, and enable us to use automated theorem provers to automatically verify properties of programs.