Deductive Systems for Logic Programs with Counting

TL;DR

This paper extends deductive systems for establishing strong equivalence in answer set programming to include programs with counting aggregates, enabling more comprehensive equivalence proofs.

Contribution

It introduces an extension of existing deductive methods to handle counting aggregates in logic programs, enhancing the analysis of program equivalence.

Findings

Extended deductive system successfully proves strong equivalence with counting aggregates

Demonstrated applicability on various logic programs with counting

Improved understanding of program transformations involving aggregates

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.