2 Review: syntax of mini-gringo

The description of mini-gringo programs below uses “abstract syntax,” which disregards some details related to representing programs by strings of ASCII characters. We assume that three countably infinite sets of symbols are selected: numerals, symbolic constants, and variables. We assume that a 1-1 correspondence between numerals and integers is chosen; the numeral corresponding to an integer n is denoted by $\overline n$ . Precomputed terms are numerals, symbolic constants, and the symbols inf, sup. We assume that a total order on the set of precomputed terms is selected, with the least element inf and the greatest element sup, so that numerals are contiguous and ordered in the standard way.

Terms allowed in a mini-gringo program are formed from precomputed terms and variables using the binary operation symbols

\begin{equation*}+\quad-\quad\times\quad/\quad\backslash \quad..\end{equation*}

An atom is a symbolic constant optionally followed by a tuple of terms in parentheses. A literal is an atom possibly preceded by one or two occurrences of not. A comparison is an expression of the form $t_1\prec t_2$ , where $t_1$ , $t_2$ are mini-gringo terms and $\prec$ is one of the six comparison symbols

(6) \begin{equation}=\quad\neq\quad<\quad>\quad\leq\quad\geq.\end{equation}

A mini-gringo rule is an expression of the form

(7) \begin{equation}{Head}\leftarrow{Body},\end{equation}

where

• ${Body}$ is a conjunction (possibly empty) of literals and comparisons, and

• ${Head}$ is either an atom (then (7) is a basic rule), or an atom in braces (then (7) is a choice rule), or empty (then (7) is a constraint).

A mini-gringo program is a finite set of mini-gringo rules.

3 Review: Semantics of mini-gringo

The semantics of ground terms is defined by assigning to every ground term t the finite set [t] of its values (Lifschitz et al. Reference Lifschitz, Lühne and Schaub2019, Section 3). Values of a ground term are precomputed terms. For instance,

\begin{equation*}[\overline 2/\overline 2]=\{\overline 1\},\ [\overline 2/\overline 0]=\emptyset,\ [\overline 0\,..\,\overline 2]=\{\overline 0, \overline 1, \overline 2\}.\end{equation*}

If a term is interval-free (that is, does not contain $..$ ), then it has at most one value. For any ground terms $t_1, \dots, t_n$ , by $[t_1, \dots, t_n]$ , we denote the set of tuples $r_1, \dots, r_n$ such that $r_1 \in [t_1], \dots,$ $r_n \in [t_n]$ .

Stable models of a mini-gringo program are defined as stable models of the set of propositional formulas obtained from it by applying a syntactic transformation denoted by $\tau$ (Lifschitz et al. Reference Lifschitz, Lühne and Schaub2019, Section 3). These propositional formulas are built from precomputed atoms—atoms $p({\bf r})$ such that members of the tuple $\bf r$ are precomputed terms. Thus, every stable model is a set of precomputed atoms.

The transformation $\tau$ is defined as follows. For any ground atom $p({\bf t})$ ,

• $\tau(p({\bf t}))$ is $\bigvee_{{\bf r} \in [{\bf t}]} p({\bf r})$ ,

• $\tau ({not}\ p({\bf t}))$ is $\bigvee_{{\bf r} \in [{\bf t}]} \neg p({\bf r})$ , and

• $\tau ({not}\ {not}\ p({\bf t}))$ is $\bigvee_{{\bf r} \in [{\bf t}]} \neg\neg p({\bf r})$ .

For any ground comparison $t_1 \prec t_2$ , $\tau(t_1 \prec t_2)$ is $\top$ if the relation $\prec$ holds between some $r_1$ from $[t_1]$ and some $r_2$ from $[t_2]$ , and $\bot$ otherwise. The result of applying $\tau$ to a conjunction $B_1\wedge B_2\wedge \cdots$ is $\tau(B_1)\wedge \tau(B_2)\wedge\cdots$ . If R is a ground basic rule $p({\bf t}) \leftarrow {Body}$ , then $\tau(R)$ is the propositional formula

(8) \begin{equation}\tau({Body}) \to\bigwedge_{{\bf r}\in [{\bf t}]} p({\bf r}).\end{equation}

If R is a ground choice rule $\{p({\bf t})\} \leftarrow {Body}$ then $\tau(R)$ is the propositional formula

(9) \begin{equation}\tau({Body}) \to \bigwedge_{{\bf r} \in [{\bf t}]}(p({\bf r})\lor\neg p({\bf r})).\end{equation}

If R is a ground constraint $\leftarrow{Body}$ then $\tau(R)$ is

(10) \begin{equation}\neg\tau({Body}).\end{equation}

For any mini-gringo program $\Pi$ , $\tau(\Pi)$ is the set of propositional formulas $\tau(R)$ for all ground rules R that can be obtained from rules of $\Pi$ by substituting precomputed terms for variables.

For example, substituting a precomputed term r for X in the choice rule

(11) \begin{equation}\{p(\overline 2)\} \leftarrow p(X),\end{equation}

gives the ground rule $\{p(\overline 2)\} \leftarrow p(r)$ , so that $\tau$ transforms (11) into the set of all formulas of the form

\begin{equation*}p(r) \to p(\overline 2) \lor \neg p(\overline 2).\end{equation*}

4 Mini-gringo with counting: syntax

We extend the class of mini-gringo rules as follows. An aggregate element is a pair ${\bf X}:{\bf L},$ where X is a tuple of distinct variables, and $\bf L$ is a conjunction of literals and comparisons such that every member of X occurs in $\bf L$ . In mini-gringo with counting, the body of a rule is allowed to contain, besides literals and comparisons, aggregate atoms of the forms

(12) \begin{equation}{count\ /} \{E\} \geq t,\ {count\ /} \{E\} \leq t,\ \end{equation}

where E is an aggregate element, and t is an interval-free term. The conjunction of aggregate atoms (12) can be written as ${count\ /}\{E\}=t$ .

A variable that occurs in a rule R is local in R if each of its occurrences is within an aggregate element, and global otherwise. A rule is pure if, for every aggregate element ${\bf X}:{\bf L}$ in its body, all variables in the tuple X are local. For example, all rules that do not contain aggregate elements are pure. The rules

(13) \begin{equation}q \leftarrow {count\ /}\{X:p(X,Y)\} \leq \overline 2,\end{equation}

and

(14) \begin{equation}q \leftarrow {count\ /}\{X:p(X,Y)\} \leq \overline 2\wedge Y=\overline 1\,..\,\overline {10},\end{equation}

are pure, because X is local in each of them. The rule

(15) \begin{equation}q \leftarrow {count\ /}\{X:p(X,Y)\} \leq \overline 2\wedge X=\overline 1\,..\,\overline {10,}\end{equation}

is not pure, because X is global. ^{Footnote 2}

A program in mini-gringo with counting, or an mgc program, is a finite set of pure rules. Allowing nonpure rules in a program would necessitate making the semantics more complicated; see Footnote 5.

An expression of the form

\begin{equation*}\overline m\,\{{\bf X}:A\}\,\overline n \leftarrow{Body},\end{equation*}

where $\bf X$ is a tuple of distinct variables, A is an atom, and ${Body}$ is a conjunction of literals, comparisons and aggregate atoms, can be used as shorthand for the group of three rules:

\begin{equation*}\begin{array} l\{A\} \leftarrow{Body},\\\leftarrow {Body}, {count\ /}\{{\bf X}:A\} \leq \overline{m-1},\\\leftarrow {Body}, {count\ /}\{{\bf X}:A\} \geq \overline{n+1}.\end{array}\end{equation*}

5 Mini-gringo with counting: Semantics

To define the semantics of mgc programs, we will extend the definition of $\tau$ (Section 3) to aggregate atoms (12) such that t is a ground term. Since t is interval-free, [t] is either a singleton or empty. If [t] is a singleton $\{c\}$ , then $\tau({count\ /}\{{\bf X}:{\bf L}\} \geq t)$ is defined as the infinite disjunction

(16) \begin{equation}\bigvee_{\Delta\,:\,\overline{|\Delta|} \geq c}\;\bigwedge_{{\bf x}\in\Delta}\;\bigvee_{\bf w} \tau\!\left({\bf L}^{{\bf X},{\bf W}}_{\,{\bf x},\;{\bf w}}\right),\end{equation}

and $\tau({count\ /}\{{\bf X}:{\bf L}\} \leq t)$ as the infinite conjunction

(17) \begin{equation}\bigwedge_{\Delta\,:\,\overline{|\Delta|}>c}\;\neg\bigwedge_{{\bf x}\in\Delta}\;\bigvee_{\bf w} \tau\!\left({\bf L}^{{\bf X},{\bf W}}_{\,{\bf x},\;{\bf w}}\right),\end{equation}

where

• $\Delta$ ranges over finite sets of tuples of precomputed terms of the same length as X;

• W is the list of variables that occur in $\bf L$ but do not belong to X;

• $\bf w$ ranges over tuples of precomputed terms of the same length as W;

• the expression ${\bf L}^{{\bf X},{\bf W}}_{\,{\bf x},\;{\bf w}}$ denotes the result of substituting $\bf x$ , $\bf w$ for all occurrences of X, W in L.

(If c is a numeral $\overline n$ then the inequalities $\overline{|\Delta|}\geq c$ , $\overline{|\Delta|}> c$ in these formulas can be written as $|\Delta|\geq n$ , $|\Delta|>n$ .) If [t] is empty, then we define

\begin{equation*}\tau({count\ /}\{{\bf X}:{\bf L}\} \geq t)=\tau({count\ /}\{{\bf X}:{\bf L}\} \leq t)=\bot.\end{equation*}

For example, the result of applying $\tau$ to the body of rule (13) is

\begin{equation*}\bigwedge_{\Delta\,:\,|\Delta| > \overline 2}\neg\bigwedge_{x\in\Delta}\;\bigvee_w p(x,w).\end{equation*}

(In this case, X is X; W is Y; $\Delta$ ranges over sets of precomputed terms; w ranges over precomputed terms.) In application to the aggregate expression

\begin{equation*}{count\ /}\{X:p(X,r)\} \leq \overline 2,\end{equation*}

where r is a precomputed term, $\tau$ gives

\begin{equation*}\bigwedge_{\Delta\,:\,|\Delta|>\overline 2}\neg\bigwedge_{x\in\Delta}p(x,r),\end{equation*}

(W is empty).

A rule is closed if it has no global variables. It is clear that substituting precomputed terms for all global variables in a pure rule is a closed pure rule. ^{Footnote 3} For any mini-gringo program $\Pi$ , $\tau(\Pi)$ stands for the conjunction of the formulas $\tau(R)$ over all closed rules R that can be obtained from rules of $\Pi$ by such substitutions. Thus, $\tau(\Pi)$ is an infinitary propositional formula over the signature consisting of all precomputed atoms.

For example, $\tau$ transforms rule (13) into

\begin{equation*}\bigwedge_{\Delta\,:\,|\Delta| > \overline 2}\neg\bigwedge_{x\in\Delta}\;\bigvee_w p(x,w) \to q,\end{equation*}

where $\Delta$ ranges over sets of precomputed terms, and w ranges over precomputed terms. Rule (14) becomes

\begin{equation*}\bigwedge_r\left(\left(\bigwedge_{\Delta\,:\,|\Delta|>\overline 2} \neg\bigwedge_{x\in\Delta}p(x,r)\right) \wedge \tau(r=\overline 1..\overline{10})\to q\right),\end{equation*}

where r ranges over precomputed terms, and $\Delta$ ranges over sets of precomputed terms. The subformula $\tau(r=\overline 1..\overline{10})$ is $\top$ if r is one of the numerals $\overline 1,\dots,\overline{10}$ , and $\bot$ otherwise.

The semantics of mgc described in this section, like the semantics of aggregates proposed by Gebser et al. (Reference Gebser, Harrison, Kaminski, Lifschitz and Schaub2015), aims at modeling the behavior of the answer set solver clingo. The definition in this paper is simpler than the 2015 version, but more limited in scope, because it is does not cover aggregates other than #count. The two versions of the semantics of #count are not completely equivalent, however, because they handle infinite sets in slightly different ways. This difference does not affect safe programs and is in this sense inessential.

6 Review: Representing mini-gringo rules by formulas

The target language of the translation $\tau^*$ is a first-order language with two sorts: the sort general and its subsort integer. General variables are meant to range over arbitrary precomputed terms, and we identify them with variables used in mini-gringo rules. Integer of the second sort is meant to range over numerals (or, equivalently, integers). The signature $\sigma_0$ of the language includes

• all precomputed terms as object constants; an object constant is assigned the sort integer iff it is a numeral;

• the symbols $+$ , $-$ and $\times$ as binary function constants; their arguments and values have the sort integer;

• symbols $p/n$ , where p is a symbolic constant, as n-ary predicate constants;

• comparison symbols (6) as binary predicate constants.

An atomic formula $(p/n)({\bf t})$ can be abbreviated as $p({\bf t})$ . An atomic formula $\prec\!\!(t_1,t_2)$ , where $\prec$ is a comparison symbol, can be written as $t_1\prec t_2$ .

Lifschitz et al. (Reference Lifschitz, Lühne and Schaub2019) defined, for every mini-gringo term t, a formula ${val\,}_{t}({Z})$ that expresses, informally speaking, that Z is one of the values of t. For example, ${val\,}_{\overline 2}({Z})$ is $Z=\overline 2$ . If $\bf t$ is a tuple $t_1,\dots,t_n$ of mini-gringo terms, and $\bf Z$ is a tuple $Z_1,\dots,Z_n$ of distinct general variables, then ${val\,}_{\bf t}({\bf Z})$ stands for ${val\,}_{t_1}({Z_1}) \wedge \cdots \wedge {val\,}_{t_n}({Z_n})$ .

The translation $\tau^B$ , which transforms literals and comparisons into formulas over the signature $\sigma_0$ , is defined in that paper as follows: ^{Footnote 4}

• $\tau^B(p({\bf t}))= \exists {\bf Z}({val\,}_{\bf t}({\bf Z}) \wedge p({\bf Z}))$ ;

• $\tau^B({not}\ p({\bf t})) = \exists {\bf Z}({val\,}_{\bf t}({\bf Z}) \wedge \neg p({\bf Z}))$ ;

• $\tau^B({not}\ {not}\ p({\bf t})) = \exists {\bf Z}({val\,}_{\bf t}({\bf Z}) \wedge \neg\neg p({\bf Z}))$ ;

• $\tau^B(t_1\prec t_2) =\exists Z_1 Z_2 ({val\,}_{t_1}({Z_1}) \wedge {val\,}_{t_2}({Z_2}) \wedge Z_1\prec Z_2)$ .

Here $Z_1$ , $Z_2$ , and members of the tuple Z are fresh general variables.

The result of applying $\tau^*$ to a mini-gringo rule $H \leftarrow B_1\wedge\cdots\wedge B_n$ can be defined as the universal closure of the formula

(18) \begin{equation}\begin{array}{ll}B^*_1\wedge\cdots\wedge B^*_n\wedge{val\,}_{\bf t}({\bf Z})\to p({\bf Z})&\hbox{ if }H\hbox{ is }p({\bf t}),\\B^*_1\wedge\cdots\wedge B^*_n\wedge{val\,}_{\bf t}({\bf Z}) \to p({\bf Z}) \lor \neg p({\bf Z})&\hbox{ if }H\hbox{ is }p\{({\bf t})\},\\\neg(B^*_1\wedge\cdots\wedge B^*_n)&\hbox{ if }H\hbox{ is empty},\end{array}\end{equation}

where $B^*_i$ stands for $\tau^B(B_i)$ , and $\bf Z$ is a tuple of fresh general variables.

For example, the result of applying $\tau^*$ to choice rule (11) is

\begin{equation*}\forall XZ(\tau^B(p(X))\wedge Z=\overline 2 \to p(Z)\lor \neg p(Z));\end{equation*}

$\tau^B(p(X))$ can be further expanded into $\exists Z(Z=X \wedge p(Z))$ .

7 Extending the target language

In this section, we extend the translation $\tau^*$ to arbitrary pure rules. This more general translation produces first-order formulas over the signature $\sigma_1$ that is obtained from $\sigma_0$ by adding infinitely many predicate constants

(19) \begin{equation}{Atleast\ /}^{{\bf X};{\bf V}}_F\hbox{ and }{Atmost\ /}^{{\bf X};{\bf V}}_F,\end{equation}

where X and V are disjoint lists of distinct general variables, and F is a formula over $\sigma_0$ such that each of its free variables belongs to X or to V. ^{Footnote 5} The number of arguments of each of constants (19) is greater by 1 than the length of V; all arguments are of the sort general.

If n is a positive integer, then the formula ${Atleast\ /}^{{\bf X},{\bf V}}_F({\bf V},\overline n)$ is meant to express that F holds for at least n values of X; symbolically,

(20) \begin{equation}\exists{\bf X}_1\cdots{\bf X}_n\left(\,\bigwedge_{i=1}^n F^{\bf X}_{\,{\bf X}_i} \wedge \bigwedge_{i<j}\neg({\bf X}_i={\bf X}_j) \right),\end{equation}

where ${\bf X}_1,\dots,{\bf X}_n$ are tuples of fresh general variables. ^{Footnote 6} For any precomputed term r, the expression $\exists_{\geq r}{\bf X} F$ will stand for

The formula ${Atmost\ /}^{{\bf X},{\bf V}}_F({\bf V},\overline n)$ is meant to express that F holds for at most n values of X; symbolically,

(21) \begin{equation}\forall{\bf X}_1\cdots{\bf X}_{n+1}\left(\bigwedge_{i=1}^{n+1} F^{\bf X}_{\,{\bf X}_i}\to \,\bigvee_{i<j}{\bf X}_i={\bf X}_j\right).\end{equation}

For any precomputed term r, the expression $\exists_{\leq r}{\bf X} F$ will stand for

The set of all sentences of the forms

(22) \begin{equation}\forall {\bf V} \left({Atleast\ /}^{{\bf X};{\bf V}}_F({\bf V},r)\leftrightarrow \exists_{\geq r} {\bf X} F\right),\end{equation}

(23) \begin{equation}\forall {\bf V} \left({Atmost\ /}^{{\bf X};{\bf V}}_F({\bf V},r)\leftrightarrow \exists_{\leq r}{\bf X} F\right)\end{equation}

will be denoted by Defs.

8 Representing pure rules by formulas

To extend the definition of $\tau^*$ reproduced in Section 6 to arbitrary pure rules, we need to say how to choose $B^*_i$ in (18) when $B_i$ includes an aggregate element ${\bf X}:{\bf L}$ . Let V be the list of global variables that occur in $\bf L$ , and let W be the list of local variables that occur in $\bf L$ but are not included in X. Then, $B^*_i$ is defined as

\begin{equation*}\exists C\left({val\,}_{t}({C})\wedge {Atleast\ /}^{{\bf X};{\bf V}}_{\exists {\bf W}\tau^B({\bf L})}({\bf V},C)\right),\end{equation*}

if $B_i$ is ${count\ /}\{{\bf X}:{\bf L}\} \geq t$ , and as

\begin{equation*}\exists C\left({val\,}_{t}({C})\wedge {Atmost\ /}^{{\bf X};{\bf V}}_{\exists {\bf W}\tau^B({\bf L})}({\bf V},C)\right),\end{equation*}

if $B_i$ is ${count\ /}\{{\bf X}:{\bf L}\} \leq t$ , where C is a fresh general variable.

For example, the result of applying $\tau^*$ to rule (13) is

\begin{equation*}\exists C\left({val\,}_{\overline 2}({C}) \wedge {Atmost\ /}^{X;}_{\exists Y\tau^B(p(X,Y))}(C)\right)\to q,\end{equation*}

(V is empty, W is Y). The result of applying $\tau^*$ to rule (14) is

\begin{equation*}\forall Y\left(\exists C\left({val\,}_{\overline 2}({C}) \wedge{Atmost\ /}^{X;Y}_{\tau^B(p(X,Y))}(Y,C)\right)\wedge\tau^B(Y=\overline 1\,..\,\overline {10}) \to q\right),\end{equation*}

(V is Y, W is empty).

For any mgc program $\Pi$ , $\tau^*(\Pi)$ stands for the conjunction of the formulas $\tau^*(R)$ for all rules R of $\Pi$ . Thus, $\tau^*(\Pi)$ is a sentence over the signature $\sigma_1$ .

9 Review: infinitary logic of here-and-there

Some of the properties of the translation $\tau^*$ discussed below refer to the deductive system of infinitary propositional logic of here-and-there (Harrison et al. Reference Harrison, Lifschitz, Pearce and Valverde2017), denoted by ${HT\ /}^\infty$ . In this section, we reproduce the definition of that system.

The derivable objects of ${HT\ /}^{\infty}$ are sequents—expressions of the form $\Gamma\Rightarrow F$ , where F is an infinitary propositional formula, and $\Gamma$ is a finite set of infinitary propositional formulas (“F under assumptions $\Gamma$ ”). To simplify notation, we write $\Gamma$ as a list. We identify a sequent of the form $\Rightarrow F$ with the formula F.

The axiom schemas of ${HT\ /}^\infty$ are

\begin{equation*}F \Rightarrow F,\end{equation*}

\begin{equation*}F\lor(F\to G)\lor\neg G,\end{equation*}

and

(24) \begin{equation}\bigwedge_{\alpha \in A}\ \ \bigvee_{F \in \mathcal{H}_\alpha} F \to\bigvee_{(F_\alpha)_{\alpha \in A}}\ \ \bigwedge_{\alpha \in A} F_\alpha,\end{equation}

where $(\mathcal{H}_\alpha)_{\alpha \in A}$ is a nonempty family of sets of formulas; the disjunction in the consequent of (24) extends over all elements $(F_\alpha)_{\alpha \in A}$ of the Cartesian product of the family $(\mathcal{H}_\alpha)_{\alpha \in A}$ . The inference rules of ${HT\ /}^\infty$ are the introduction and elimination rules for the propositional connectives shown in the Table 1 above and the weakening rule

\begin{equation*}(W)\;{\frac{\textstyle {\Gamma\Rightarrow F}}{\textstyle {\Gamma,\Delta\Rightarrow F}}} .\end{equation*}

Falsity and negation are not mentioned in the axiom schemas and inference rules of ${HT\ /}^\infty$ because $\bot$ is considered shorthand for $\emptyset^\lor$ , and $\neg F$ is shorthand for $F\to\bot$ .

Table 1.

Introduction and elimination rules of infinitary propositional logic. By $\mathcal H^\wedge$ and $\mathcal H^\lor$ , we denote the conjunction and disjunction of all formulas in $\mathcal H$ .

The set of theorems of HT $^\infty$ is the smallest set of sequents that includes the axioms of the system and is closed under the application of its inference rules. We say that formulas F and G are equivalent in HT $^\infty$ if $F\leftrightarrow G$ is a theorem of HT $^\infty$ .

The role of this deductive system is determined by the fact that two infinitary propositional formulas are strongly equivalent to each other if and only if they are equivalent in ${HT\ /}^\infty$ (Harrison et al. Reference Harrison, Lifschitz, Pearce and Valverde2017, Corollary 2).

10 Properties of the generalized translation

Informally speaking, a pure rule R has the same meaning as the sentence $\tau^*(R)$ . This claim is made precise in Theorem 1 below. The statement of the theorem refers to the infinitary propositional formulas obtained from sentences over $\sigma_1$ by applying the grounding operator gr, which is defined recursively:

• $gr(\bot)$ is $\bot$ ;

• if F is $\prec(t_1,t_2)$ , where $\prec$ is a comparison symbol, then gr(F) is $\top$ if the relation $\prec$ holds for the values of $t_1$ and $t_2$ , and $\bot$ otherwise;

• if F is $p({\bf t})$ , where p is not a comparison symbol, then gr(F) is obtained from F by replacing each member of the tuple t by its value;

• $gr(F\odot G)$ is $gr(F)\odot gr(G)$ for every binary connective $\odot$ ;

• $gr(\forall X\,F)$ is the conjunction of the formulas $gr\left(F^X_r\right)$ over all precomputed terms r if X is a general variable, and over all numerals r if X is an integer variable;

• $gr(\exists X\,F)$ is the disjunction of the formulas $gr\left(F^X_r\right)$ over all precomputed terms r if X is a general variable, and over all numerals r if X is an integer variable.

Thus, gr(F) is an infinitary propositional formula over the signature consisting of all atomic formulas of the form $p({\bf r})$ , where p is different from comparison symbols and $\bf r$ is a tuple of precomputed terms. Such atomic formulas will be called extended precomputed atoms. Unlike precomputed atoms, they may contain predicate symbols (19). If $\Gamma$ is a set of sentences over $\sigma_1$ , then $gr(\Gamma)$ stands for the set of formulas gr(F) for all F in $\Gamma$ .

The statement of the theorem refers also to the system ${HT\ /}^\infty$ (Section 9) extended by the axioms $gr({Defs})$ . These axioms express the meaning of predicate symbols (19).

About mgc programs $\Pi_1$ , $\Pi_2$ we say that they are strongly equivalent to each other if $\tau(\Pi_1)$ is strongly equivalent to $\tau(\Pi_2)$ . This condition guarantees that for any mgc program $\Pi$ (and, more generally, for any logic program $\Pi$ in a similar language), $\Pi_1\cup\Pi$ has the same stable models as $\Pi_2\cup\Pi$ .

Theorem 2 mgc programs $\Pi_1$ , $\Pi_2$ are strongly equivalent to each other iff

(25) \begin{equation} gr(\tau^*(\Pi_1))\hbox{ is equivalent to }gr(\tau^*(\Pi_2)) \hbox{ in }{HT\ /}^\infty\!+\!gr({Defs\ /}). \end{equation}

Thus, the claim that MGC programs $\Pi_1$ , $\Pi_2$ are strongly equivalent to each other can be always established, in principle, by deriving each of the infinitary propositional formulas $gr(\tau^*(\Pi_1))$ , $gr(\tau^*(\Pi_2))$ from the other in ${HT\ /}^\infty\!+\!gr({Defs\ /})$ . Theorem 3 below shows that in some cases such a claim can be justified by operating with finite formulas—with first-order formulas of the signature $\sigma_1$ . Instead of ${HT\ /}^\infty\!+\!gr({Defs\ /})$ , we can use the logic of here-and-there with arithmetic (Lifschitz Reference Lifschitz2021) extended by the axiom schemas Defs:

As an example, we will use ${HT\ /}^\infty\!+\!gr({Defs\ /})$ to verify that rules (1), (2), (3) are strongly equivalent to each other. The translation $\tau^*$ transforms these rules into the formulas

(26) \begin{equation}\forall Y\left( \exists C\left(C=Y\wedge{Atleast\ /}^{X;}_{\tau^B(p(X))}(C)\right) \wedge\tau^B(Y=\overline 1),\to q\right),\end{equation}

(27) \begin{equation} \exists C\left(C=\overline 1\wedge{Atleast\ /}^{X;}_{\tau^B(p(X))}(C)\right)\to q,\end{equation}

(28) \begin{equation}\forall X(\tau^B(p(X))\to q).\end{equation}

The first two formulas are equivalent to each other in intuitionistic predicate calculus with equality, which is a subsystem of ${HTA\ /}$ ; this is clear from the fact that $\tau^B(Y=\overline 1)$ stands for the formula $\exists Z_1Z_2(Z_1=Y\wedge Z_2=\overline 1\wedge Z_1=Z_2)$ , which is intuitionistically equivalent to $Y=\overline 1$ . Furthermore, (27) is intuitionistically equivalent to

(29) \begin{equation}{Atleast\ /}^{X;}_{\tau^B(p(X))}(\overline 1)\to q.\end{equation}

Using the axiom

\begin{equation*}{Atleast\ /}^{X;}_{\tau^B(p(X))}(\overline 1)\leftrightarrow \exists X \tau^B(p(X)),\end{equation*}

of ${HTA}\!+\!{Defs}$ , (29) can be transformed into the formula $\exists X\,\tau^B(p(X))\to q$ , which is intuitionistically equivalent to (28).

11 Proofs

In this section, the word “equivalent” in application to infinitary propositional formulas refers to equivalence in ${HT\ /}^\infty$ whenever the deductive system is not specified.

The following fact is Proposition 2 by Lifschitz et al. (Reference Lifschitz, Lühne and Schaub2019).

Lemma 3 Let X, V, W be disjoint lists of distinct general variables, and let A be an aggregate atom $count\{{\bf X}:{\bf L}\} \prec t$ such that every variable occurring in $\bf L$ belongs to one of these three lists, and every variable occurring in t belongs to V. For any list $\bf v$ of precomputed terms of the same length as V, the formula $\tau\left(A^{\bf V}_{\bf v}\right)$ is equivalent in ${HT\ /}^\infty\!+\!gr({Defs\ /})$ to

(30) \begin{equation}gr\left(\exists C\left(val_{t^{\bf V}_{\bf v}}(C) \wedge Atleast^{{\bf X};{\bf V}}_{\exists{\bf W}\tau^B({\bf L})}({\bf v},C)\right)\right),\end{equation}

if $\prec$ is $\geq$ , and to

(31) \begin{equation}gr\left(\exists C\left(val_{t^{\bf V}_{\bf v}}(C) \wedge Atmost^{{\bf X};{\bf V}}_{\exists{\bf W}\tau^B({\bf L})}({\bf v},C)\right)\right),\end{equation}

if $\prec$ is $\leq$ .

Proof. Case 1: $\prec$ is $\geq$ . Formula (30) can be written as

\begin{equation*}\bigvee_c \left(gr({val\,}_{t^{\bf V}_{\bf v}}({c})) \wedge {Atleast\ /}^{{\bf X};{\bf V}}_{\exists{\bf W}\tau^B({\bf L})}({\bf v},c)\right),\end{equation*}

where c ranges over precomputed terms. From Lemma 1, we see that it is equivalent to

\begin{equation*}\bigvee_{c\in\left[t^{\bf V}_{\bf v}\right]} {Atleast\ /}^{{\bf X};{\bf V}}_{\exists{\bf W}\tau^B({\bf L})}({\bf v},c).\end{equation*}

Consider the infinitary formula obtained by grounding (22) with $\exists{\bf W}\tau^B({\bf L})$ as F. One of its conjunctive terms is

\begin{equation*}{Atleast\ /}^{{\bf X};{\bf V}}_{\exists{\bf W}\tau^B({\bf L})}({\bf v},c)\leftrightarrow gr\left(\left(\exists_{\geq c} {\bf X} \exists{\bf W}\tau^B({\bf L})\right)^{\bf V}_{\bf v}\right).\end{equation*}

Consequently (30) is equivalent in ${HT\ /}^\infty\!+\!gr({Defs\ /})$ to

(32) \begin{equation}\bigvee_{c\in\left[t^{\bf V}_{\bf v}\right]}gr\left(\left(\exists_{\geq c} {\bf X} \exists{\bf W}\tau^B({\bf L})\right)^{\bf V}_{\bf v}\right).\end{equation}

Case 1.1: The set $\left[t^{\bf V}_{\bf v}\right]$ is empty. Then (32) is the empty disjunction $\bot$ ; $\tau\left(A^{\bf V}_{\bf v}\right)$ is $\bot$ as well. Case 1.2: The set $\left[t^{\bf V}_{\bf v}\right]$ is nonempty. Since t is interval-free, this set is a singleton $\{c\}$ , so that (32) is

(33) \begin{equation}gr\left(\left(\exists_{\geq c} {\bf X} \exists{\bf W}\tau^B({\bf L})\right)^{\bf V}_{\bf v}\right),\end{equation}

and $\tau\left(A^{\bf V}_{\bf v}\right)$ is

(34) \begin{equation}\bigvee_{\Delta\,:\,\overline{|\Delta|} \geq c}\;\bigwedge_{{\bf x}\in\Delta}\;\bigvee_{\bf w} \tau\!\left({\bf L}^{{\bf X},{\bf V},{\bf W}}_{\,{\bf x},\;{\bf v},\;{\bf w}}\right).\end{equation}

Case 1.2.1: $c\leq\overline 0$ . Then (33) is $\top$ . The disjunctive term of (34) with $\Delta=\emptyset$ is the empty conjunction $\top$ , so that (34) is equivalent to $\top$ . Case 1.2.2: for all n, $c>\overline n$ . Then (33) is $\bot$ . Formula (34) is the empty disjunction $\bot$ as well. Case 1.2.3: c is a numeral $\overline n$ , $n>0$ . Then (33) is

\begin{equation*}gr\left(\exists{\bf X}_1\cdots{\bf X}_n\left(\bigwedge_{i=1}^n \exists{\bf W}\left(\tau^B({\bf L})^{{\bf X},{\bf V}}_{{\bf X}_i,{\bf v}}\right) \wedge\bigwedge_{i<j}\neg({\bf X}_i={\bf X}_j)\right)\right),\end{equation*}

This formula can be rewritten as

\begin{equation*}\bigvee_{{\bf x}_1,\dots,{\bf x}_n}\left(\bigwedge_{i=1}^n \bigvee_{\bf w}gr\left((\tau^B{\bf L})^{{\bf X},{\bf V},{\bf W}}_{{\bf x}_i,{\bf v},{\bf w}}\right) \wedge\bigwedge_{i<j}\neg gr({\bf x}_i={\bf x}_j)\right)\end{equation*}

( ${\bf x}_1,\dots{\bf x}_n,{\bf w}$ range over tuples of precomputed terms). The part $\bigwedge_{i<j}\neg(gr({\bf x}_i={\bf x}_j))$ is equivalent to $\top$ if the tuples ${\bf x}_1,\dots{\bf x}_n$ are pairwise distinct, that is to say, if the cardinality of the set $\{{\bf x}_1,\dots{\bf x}_n\}$ is n; otherwise, this conjunction is equivalent to $\bot$ . Consequently (33) is equivalent to

\begin{equation*}\bigvee_{\Delta\,:\,|\Delta|=n}\,\bigwedge_{{\bf x}\in\Delta}\bigvee_{\bf w}gr\left((\tau^B{\bf L})^{{\bf X},{\bf V},{\bf W}}_{{\bf x},\;{\bf v},\;{\bf w}}\right).\end{equation*}

The formula $gr\!\left((\tau^B{\bf L})^{{\bf X},{\bf V},{\bf W}}_{{\bf x},\;{\bf v},\;{\bf w}}\right)$ can be rewritten as $gr\!\left(\tau^B\left({\bf L}^{{\bf X},{\bf V},{\bf W}} _{{\bf x},\;{\bf v},\;{\bf w}}\right)\right)$ . By Lemma 2, it is equivalent to $\tau\left({\bf L}^{{\bf X},{\bf V},{\bf W}}_{{\bf x},\;{\bf v},\;{\bf w}}\right)$ , so that (33) is equivalent to

(35) \begin{equation}\bigvee_{\Delta\,:\,|\Delta| = n}\;\bigwedge_{{\bf x}\in\Delta}\;\bigvee_{\bf w} \tau\!\left({\bf L}^{{\bf X},{\bf V},{\bf W}}_{\,{\bf x},\;{\bf v},\;{\bf w}}\right). \end{equation}

Disjunction (34) can be obtained from this disjunction by adding similar disjunctive terms with sets $\Delta$ containing more than n tuples. Since each of these disjunctive terms is stronger than some of the disjunctive terms in (35), the two disjunctions are equivalent.

Case 2: $\prec$ is $\leq$ . Formula (31) is equivalent in ${HT\ /}^\infty\!+\!gr({Defs\ /})$ to

(36) \begin{equation}\bigvee_{c\in\left[t^{\bf V}_{\bf v}\right]}gr\left(\left(\exists_{\leq c} {\bf X} \exists{\bf W}\tau^B({\bf L})\right)^{\bf V}_{\bf v}\right);\end{equation}

this is parallel to the argument in Case 1.

Case 2.1: The set $\left[t^{\bf V}_{\bf v}\right]$ is empty. Then (36) is the empty disjunction $\bot$ ; $\tau\left(A^{\bf V}_{\bf v}\right)$ is $\bot$ as well. Case 2.2: The set $\left[t^{\bf V}_{\bf v}\right]$ is nonempty. Since t is interval-free, this set is a singleton $\{c\}$ , so that (36) is

(37) \begin{equation}gr\left(\left(\exists_{\leq c} {\bf X} \exists{\bf W}\tau^B({\bf L})\right)^{\bf V}_{\bf v}\right),\end{equation}

and $\tau\left(A^{\bf V}_{\bf v}\right)$ is

(38) \begin{equation}\bigwedge_{\Delta\,:\,\overline{|\Delta|}>c}\;\neg\bigwedge_{{\bf x}\in\Delta}\;\bigvee_{\bf w} \tau\!\left({\bf L}^{{\bf X},{\bf V},{\bf W}}_{\,{\bf x},\;{\bf v},\;{\bf w}}\right).\end{equation}

Case 2.2.1: $c<\overline 0$ . Then (37) is $\bot$ . The conjunctive term of (38) with $\Delta=\emptyset$ is $\neg\top$ , so that (38) is equivalent to $\bot$ . Case 2.2.2: for all n, $c>\overline n$ . Then (37) is $\top$ . Formula (38) is the empty conjunction $\top$ as well. Case 2.2.3: c is a numeral $\overline n$ , $n>0$ . Then (37) is

\begin{equation*}gr\left(\forall{\bf X}_1\cdots{\bf X}_{n+1}\left(\bigwedge_{i=1}^{n+1} \exists{\bf W}\left(\tau^B({\bf L})^{{\bf X},{\bf V}}_{{\bf X}_i,{\bf v}}\right) \to\bigvee_{i<j}{\bf X}_i={\bf X}_j\right)\right).\end{equation*}

This formula can be rewritten as

\begin{equation*}\bigwedge_{{\bf x}_1,\dots,{\bf x}_{n+1}}\left(\bigwedge_{i=1}^{n+1} \bigvee_{\bf w}gr\left((\tau^B{\bf L})^{{\bf X},{\bf V},{\bf W}}_{{\bf x}_i,{\bf v},{\bf w}}\right) \to\bigvee_{i<j} gr({\bf x}_i={\bf x}_j)\right).\end{equation*}

The consequent $\bigvee_{i<j}gr({\bf x}_i={\bf x}_j))$ is equivalent to $\bot$ if the tuples ${\bf x}_1,\dots{\bf x}_{n+1}$ are pairwise distinct, that is to say, if the cardinality of the set $\{{\bf x}_1,\dots{\bf x}_{n+1}\}$ is $n+1$ ; otherwise this conjunction is equivalent to $\top$ . Consequently, (37) is equivalent to

\begin{equation*}\bigwedge_{\Delta\,:\,|\Delta|=n+1}\neg\bigwedge_{{\bf x}\in\Delta}\bigvee_{\bf w}gr\left((\tau^B{\bf L})^{{\bf X},{\bf V},{\bf W}}_{{\bf x},\;{\bf v},\;{\bf w}}\right),\end{equation*}

and furthermore to

(39) \begin{equation}\bigwedge_{\Delta\,:\,|\Delta| = n+1}\neg\bigwedge_{{\bf x}\in\Delta}\;\bigvee_{\bf w} \tau\!\left({\bf L}^{{\bf X},{\bf V},{\bf W}}_{\,{\bf x},\;{\bf v},\;{\bf w}}\right); \end{equation}

this is parallel to the argument in Case 1.2.3. Conjunction (38) can be obtained from this conjunction by adding similar conjunctive terms with finite sets $\Delta$ containing more than $n+1$ tuples. Since each of these conjunctive terms is weaker than some of the conjunctive terms in (39), the two conjunctions are equivalent to each other.

Proof of Theorem 1 Assume, for instance, that R is a basic rule $p({\bf t}) \leftarrow B_1\wedge\cdots\wedge B_n$ ; for choice rules and constraints the proof is similar. Then $\tau^*(R)$ is

\begin{equation*}\forall{\bf V}{\bf Z}(B^*_1\wedge\cdots\wedge B^*_n\wedge{val\,}_{\bf t}({\bf Z})\to p({\bf Z})),\end{equation*}

where V is the list of global variables of R, and $B_i^*$ are the formulas defined in Section 8. It follows that $gr(\tau^*(R))$ is the conjunction of the formulas

\begin{equation*}gr\left((B^*_1)^{\bf V}_{\bf v}\right)\wedge\cdots\wedge gr\left((B^*_n)^{\bf V}_{\bf v}\right)\wedge gr\left({val\,}_{\bf t^{\bf V}_{\bf v}}({\bf r})\right)\to p({\bf r}),\end{equation*}

over all tuples $\bf v$ of precomputed terms of the same length as V and all tuples $\bf r$ of precomputed terms of the same length as Z. By Lemma 1, we can conclude that $gr(\tau^*(R))$ is equivalent to the formula

\begin{equation*}\bigwedge_{\bf v}\left(\left(gr\left((B^*_1)^{\bf V}_{\bf v}\right)\wedge\cdots\wedge gr\left((B^*_n)^{\bf V}_{\bf v}\right)\right)\to \bigwedge_{{\bf r}\in \left[{\bf t}^{\bf V}_{\bf v}\right]} p({\bf r})\right).\end{equation*}

Each of the formulas

(40) \begin{equation}gr\left((B^*_i)^{\bf V}_{\bf v}\right),\end{equation}

$(i=1,\dots,n)$ is equivalent in ${HT\ /}^\infty\!+\!gr({Defs\ /})$ to $\tau\left((B_i)^{\bf V}_{\bf v}\right)$ . Indeed, if $B_i$ is a literal or a comparison, then (40) is $gr\left(\left(\tau^B(B_i)\right)^{\bf V}_{\bf v}\right)$ , which can be also written as $gr\left(\tau^B\left((B_i)^{\bf V}_{\bf v}\right)\right)$ ; this formula is equivalent in ${HT\ /}^\infty\!+\!gr({Defs\ /})$ to $\tau\left((B_i)^{\bf V}_{\bf v}\right)$ by Lemma 2. If $B_i$ is an aggregate atom then (40) is equivalent in ${HT\ /}^\infty\!+\!gr({Defs\ /})$ to $\tau\left((B_i)^{\bf V}_{\bf v}\right)$ by Lemma 3. Consequently $gr(\tau^*(R))$ is equivalent in ${HT\ /}^\infty\!+\!gr({Defs\ /})$ to

(41) \begin{equation}\bigwedge_{\bf v}\left(\tau\left((B_1)^{\bf V}_{\bf v}\right)\wedge\cdots\wedge \tau\left((B_n)^{\bf V}_{\bf v}\right)\to \bigwedge_{{\bf r}\in \left[{\bf t}^{\bf V}_{\bf v}\right]} p({\bf r})\right).\end{equation}

It remains to observe that instances of R are rules of the form

\begin{equation*}p({\bf t}^{\bf V}_{\bf v}) \leftarrow (B_1)^{\bf V}_{\bf v}\wedge\cdots\wedge (B_n)^{\bf V}_{\bf v},\end{equation*}

so that (41) is $\tau(R)$ .

Proof (sketch) The set $gr({Defs})$ consists of infinitary propositional formulas of the forms

(42) \begin{equation}\bigwedge_{\bf v}\left({Atleast\ /}^{{\bf X};{\bf V}}_F({\bf v},r)\leftrightarrow gr\left(\exists_{\geq r} {\bf X} F^{\bf V}_{\bf v}\right)\right),\end{equation}

and

(43) \begin{equation}\bigwedge_{\bf v}\left({Atmost\ /}^{{\bf X};{\bf V}}_F({\bf v},r)\leftrightarrow gr\left(\exists_{\leq r} {\bf X} F^{\bf V}_{\bf v}\right)\right).\end{equation}

A derivation from $gr({Defs})$ can be visualized as a tree with axioms of ${HT\ /}^\infty$ and formulas (42), (43), attached to leaves. In such a tree, modify all formulas by replacing

• atoms ${Atleast\ /}^{{\bf X};{\bf V}}_F({\bf v},r)$ by $gr\left(\exists_{\leq r}{\bf X} F^{{\bf V}}_{\bf v}\right)$ , and

• atoms ${Atmost\ /}^{{\bf X};{\bf V}}_F({\bf v},r)$ by $gr\left(\exists_{\geq r}{\bf X} F^{{\bf V}}_{\bf v}\right)$ .

The result is a derivation from formulas that are provable in ${HT\ /}^\infty$ . If the formula attached to the root does not contain ${Atleast\ /}^{{\bf X};{\bf V}}_F$ , ${Atmost\ /}^{{\bf X};{\bf V}}_F$ , then it is not affected by this transformation.

Proof of Theorem 2 By Theorem 1, each of the equivalences

\begin{equation*}gr(\tau^*(\Pi_1)) \leftrightarrow \tau(\Pi_1),\ gr(\tau^*(\Pi_2)) \leftrightarrow \tau(\Pi_2),\end{equation*}

is provable in ${HT\ /}^\infty\!+\!gr({Defs\ /})$ . Consequently condition (25) is equivalent to the condition

(44) \begin{equation} \tau(\Pi_1)\hbox{ is equivalent to }\tau(\Pi_2)\hbox{ in }{HT\ /}^\infty\!+\!gr({Defs\ /}).\end{equation}

By Lemma 4, (44) is equivalent to the condition

\begin{equation*}\tau(\Pi_1)\leftrightarrow\tau(\Pi_2)\hbox{ is provable in }{HT\ /}^\infty,\end{equation*}

which holds if and only if $\Pi_1$ is strongly equivalent to $\Pi_2$ .

Proof (sketch) For any axiom S of ${HTA\ /}$ , the formula gr(S) is provable in ${HT\ /}^\infty$ . (To be precise, axioms of ${HTA\ /}$ are sequents, and the transformation gr needs to be applied to the universal closure of the formula corresponding to S.) For any instance

\begin{equation*}\frac{S_1\ \cdots\ S_k}{S},\end{equation*}

of an inference rule of ${HTA\ /}$ , the formula gr(S) is derivable from $gr(S_1),\dots,gr(S_k)$ in ${HT\ /}^\infty$ . It follows that for any formula F that is derivable from Defs in ${HTA\ /}$ , the formula gr(F) is derivable from $gr({Defs})$ in ${HT\ /}^\infty$ .

12 Related Work

Fandinno et al. (Reference Fandinno, Nansen and Lierler2022) defined a translation similar to $\tau^*$ for an answer set programming language that is in some ways less expressive than mini-gringo with counting (no arithmetic operations), and in some ways more expressive (the #sum aggregate is allowed, besides #count). The main difference between that approach to transforming aggregate expressions into formulas and the one described above is that the former employs function symbols in the role that predicate symbols (19) play here. As discussed in Footnote 1, thinking of #count as a function may be misleading. This is apparently the reason why the adequacy of the translation due to Fandinno et al. is only guaranteed for programs without positive recursion through aggregates (Fandinno et al. Reference Fandinno, Nansen and Lierler2022, Theorem 3). This assumption is not satisfied, for instance, for program (4), (5).

The technical problems discussed in this paper are specific for the approach to aggregates implemented in the answer set solver clingo and do not appear in the same form, for instance, in the theory of the solver dlv (Faber et al. Reference Faber, Pfeifer and Leone2011). The semantics of aggregates based on the vicious circle principle (Gelfond and Zhang Reference Gelfond and Zhang2019), unlike the clingo semantics, makes rule (4) strongly equivalent to each of the rules (1)–(3).