Deductive Systems for Logic Programs with Counting

TL;DR

This work extends the notion of strong equivalence in answer set programming to programs with counting aggregates by developing the HT# deductive framework. It translates mgc rules into first-order sentences via $\tau^*$ and proves that equivalence in HT# implies strong equivalence of the original programs, with a classical FO bridge provided by the $HT#'$ transformation using $\gamma$. To achieve completeness, the authors introduce $HT#^\omega$, an omega-rule based system, showing that two mgc programs are strongly equivalent iff their $\tau^*$ translations are interchangeable under this system. The paper also demonstrates how $HT#$ relates to earlier mgc formalisms through $Defs$ and provides a concrete example, while outlining prospects for automation via classical theorem provers and extensions to other aggregates. Overall, the framework offers a principled, logic-based approach to verifying strong equivalence for counting-enabled logic programs, with potential practical impact on program optimization and verification tools.

Abstract

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.

Theorems & Definitions (37)

• Theorem 1
• Proposition 1
• Proposition 2
• Proposition 3
• Theorem 2
• Theorem 3
• Corollary 1
• proof
• Theorem 4
• Theorem 5