In answer set programming, two groups of rules are considered strongly equivalent if they havethe same meaning in any context. In some cases, strong equivalence of programs in the inputlanguage of the grounder gringo can be established by deriving rules of each program from rulesof the other. The possibility of such proofs has been demonstrated for a subset of that languagethat includes comparisons, arithmetic operations, and simple choice rules, but not aggregates.This method is extended here to a class of programs in which some uses of the #count aggregateare allowed.
展开▼
