# Deductive Systems for Logic Programs with Counting

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 5 of its 30 references that are in the map.
- First posted on arXiv 24 Nov 2025.

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

- [Verifying Tight Logic Programs with anthem and Vampire](https://mlsanity.com/paper/2008.02025/) (2020)
- [External Behavior of a Logic Program and Verification of Refactoring](https://mlsanity.com/paper/2305.17485/) (2023)
- [Here and There with Arithmetic](https://mlsanity.com/paper/2108.03187/) (2021)
- [Strong Equivalence of Logic Programs with Counting](https://mlsanity.com/paper/2205.07783/) (2022)
- [Recursive Aggregates as Intensional Functions in Answer Set Programming: Semantics and Strong Equivalence](https://mlsanity.com/paper/2412.10975/) (2024)

## Abstract (arXiv)

In answer set programming, two groups of rules are considered strongly equivalent if they have the same meaning in any context. Strong equivalence of two programs can be sometimes established by deriving rules of each program from rules of the other in an appropriate deductive system. This paper shows how to extend this method of proving strong equivalence to programs containing the counting aggregate.