Deductive Systems for Logic Programs with Counting
arXiv:2511.19565v1
Originality Synthesis-oriented
AI Analysis
This work addresses a specific technical challenge in answer set programming, representing an incremental advancement in formal methods for logic programs.
The paper tackles the problem of proving strong equivalence for logic programs with counting aggregates, extending deductive systems to handle such programs.
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.