# Verifying Tight Logic Programs with anthem and Vampire

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

## Key facts

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

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

- [Constraint Answer Set Programming: Integrational and Translational (or SMT-based) Approaches](https://mlsanity.com/paper/2107.08252/) (2021)
- [Verification of Locally Tight Programs](https://mlsanity.com/paper/2204.10789/) (2022)
- [Unit Testing in ASP Revisited: Language and Test-Driven Development Environment](https://mlsanity.com/paper/2401.02153/) (2024)
- [Rethinking Answer Set Programming Templates](https://mlsanity.com/paper/2307.06382/) (2023)
- [Recursive Aggregates as Intensional Functions in Answer Set Programming: Semantics and Strong Equivalence](https://mlsanity.com/paper/2412.10975/) (2024)
- [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)
- [Automated Verification of Equivalence Properties in Advanced Logic Programs -- Bachelor Thesis](https://mlsanity.com/paper/2310.19806/) (2023)
- [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)
- [Implementing the First-Order Logic of Here and There](https://mlsanity.com/paper/2601.03848/) (2026)
- [Parametric Modular Answer Set Programs Made Declarative](https://mlsanity.com/paper/2605.22716/) (2026)

## Abstract (arXiv)

This paper continues the line of research aimed at investigating the relationship between logic programs and first-order theories. We extend the definition of program completion to programs with input and output in a subset of the input language of the ASP grounder gringo, study the relationship between stable models and completion in this context, and describe preliminary experiments with the use of two software tools, anthem and vampire, for verifying the correctness of programs with input and output. Proofs of theorems are based on a lemma that relates the semantics of programs studied in this paper to stable models of first-order formulas. Under consideration for acceptance in TPLP.