# Verification of Locally Tight Programs

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

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- Builds on 2 of its 30 references that are in the map.
- First posted on arXiv 18 Apr 2022.

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

- [Verifying Tight Logic Programs with anthem and Vampire](https://mlsanity.com/paper/2008.02025/) (2020)
- [First-Order Stable Model Semantics and First-Order Loop Formulas](https://mlsanity.com/paper/1401.3898/) (2014)

## 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)
- [Parametric Modular Answer Set Programs Made Declarative](https://mlsanity.com/paper/2605.22716/) (2026)

## Abstract (arXiv)

Program completion is a translation from the language of logic programs into the language of first-order theories. Its original definition has been extended to programs that include integer arithmetic, accept input, and distinguish between output predicates and auxiliary predicates. For tight programs, that generalization of completion is known to match the stable model semantics, which is the basis of answer set programming. We show that the tightness condition in this theorem can be replaced by a less restrictive "local tightness" requirement. From this fact we conclude that the proof assistant anthem-p2p can be used to verify equivalence between locally tight programs. Under consideration for publication in Theory and Practice of Logic Programming