1 Introduction

In answer set programming (ASP), two groups of rules are considered strongly equivalent if replacing one group by the other within any program does not affect the set of stable models [21]. This equivalence relation has been extensively studied in the literature because of its interesting theoretical properties and its usefulness for the practice of answer set programming [1,2,3,4,5,6, 8, 10, 11, 15, 16, 19, 20, 22,23,24, 27]. Jan Heuer designed and implemented a system that verifies strong equivalence of programs in the ASP language mini-gringo. The system is described in his Bachelor Thesis [12], presented to the University of Potsdam.

The design of the system is based on the syntactic transformation \(\tau ^*\) [20], which converts mini-gringo rules and programs into first-order formulas. Mini-gringo programs \(\varPi _1\), \(\varPi _2\) are strongly equivalent whenever the formulas \(\tau ^*\varPi _1\) and \(\tau ^*\varPi _2\) can be derived from each other in the deductive system HTA (“here-and-there with arithmetic”) [17].

To use a resolution theorem prover as a proof engine for HTA, Heuer needed an additional translation that would relate HTA to a classical first-order theory. The translation that he implemented is a straightforward generalization of the process proposed by Pearce et al. [25] for propositional formulas.

Unfortunately, the claim that is supposed to justify this additional translation [12, Theorem 3] is incorrect as stated, because it disregards the existence of interpretations that treat arithmetical symbols in nonstandard ways.Footnote 1 For example, the facts \(p(2+3)\) and p(5) are strongly equivalent, but we cannot assert that they get the same truth value under any interpretation. Indeed, the expressions \(2+3\) and 5 can have different values if the symbols 2, 3, 5 and \(+\) are not interpreted as usual in arithmetic.

In this paper we show that, in spite of this difficulty, Heuer’s procedure is in fact correct. Second, we show that the procedure will produce correct results if we modify it by replacing \(\tau ^*R\) with the simpler translation \(\nu R\) when the rule R is regular [18]. The paper begins with a review of the mini-gringo language and of the target language of the translations \(\tau ^*\) and \(\nu \) (Sects. 2 and 3). The main results of this paper are stated in Sect. 4. In Sect. 5 we give examples of their use. In Sect. 6 we describe an extension HTA\(^\omega \) of the deductive system HTA, which plays an important role in our proofs of the main results.

2 Review: Programs

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 and symbolic constants. We assume that a total order on precomputed terms is chosen such that for all integers m and n, \(\overline{m} < \overline{n}\) iff \(m<n\).

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

$$+\quad -\quad \times \quad /\quad \backslash \quad ..$$

(the last three serve to represent integer division, remainder and intervals). 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 terms and \(\prec \) is \(=\) or one of the comparison symbols

$$\begin{aligned} \ne \quad <\quad >\quad \le \quad \ge \end{aligned}$$
(1)

A rule is an expression of the form \(Head \leftarrow Body \), where

  • \(Body \) is a conjunction (possibly empty) of literals and comparisons, and

  • \(Head \) is either an atom (then the rule is basic), or an atom in braces (then this is a choice rule), or empty (then this is a constraint).

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

The semantics of ground terms is defined by assigning to every ground term t the finite set [t] of its values [20, Section 3]. Values of a ground term are precomputed terms. For instance,

$$ [\overline{2}/\overline{3}]=\{\overline{0}\},\ [\overline{2}/\overline{0}]=\emptyset ,\ [\overline{0}\,..\,\overline{2}]=\{\overline{0}, \overline{1}, \overline{2}\}. $$

A predicate symbol is a pair p/n, where p is a symbolic constant, and n is a nonnegative integer. About a predicate symbol p/n we say that it occurs in a program \(\varPi \) if a rule of \(\varPi \) contains an atom of the form \(p(t_1,\dots ,t_n)\).

Stable models of a program are defined as stable models of the set of propositional formulas obtained from it by the syntactic transformation \(\tau \) [20, Section 3]. Atomic parts of these formulas are precomputed atoms—atoms \(p(\textbf{t})\) such that the members of \(\textbf{t}\) are precomputed terms. For example, \(\tau \) transforms the rule

$$\begin{aligned} \{q(X)\} \leftarrow p(X) \end{aligned}$$
(2)

into the set of formulas \(p(t)\rightarrow (q(t)\vee \lnot q(t))\) for all precomputed terms t. The rule

$$\begin{aligned} q(\overline{0}\,..\,\overline{2}) \leftarrow p \end{aligned}$$
(3)

is transformed into \(p\rightarrow (q(\overline{0})\wedge q(\overline{1})\wedge q(\overline{2}))\). Thus stable models of mini-gringo programs are sets of precomputed atoms.

Mini-gringo programs \(\varPi _1\) and \(\varPi _2\) are strongly equivalent to each other if, for every set \(\varOmega \) of propositional combinations of precomputed atoms, \(\tau \varPi _1\cup \varOmega \) has the same stable models as \(\tau \varPi _2\cup \varOmega \).

3 Review: Two-Sorted Formulas

The target language of the translations \(\tau ^*\) [20, Section 6] and \(\nu \) [18, Sections 4, 5] is a first-order language with the sort general and its subsort integer.Footnote 2 Variables of the first sort are meant to range over arbitrary precomputed terms, and we identify them with variables used in mini-gringo rules. Variables of the second sort are meant to range over numerals (or, equivalently, integers). This is made precise in the definition of a standard interpretation at the end of this section.

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;Footnote 3

  • predicate symbols p/n as n-ary predicate constants; their arguments have the sort general;

  • comparison symbols (1) as binary predicate constants; their arguments have the sort general.

An atomic formula \((p/n)(t_1,\dots ,t_n)\) can be abbreviated as \(p(t_1,\dots ,t_n)\). An atomic formula of the form \(\prec \!\!(t_1,t_2)\), where \(\prec \) is a comparison symbol, can be written as \(t_1\prec t_2\). A conjunction of the form \(t_1\le t_2 \wedge t_2\le t_3\) can be written as \(t_1\le t_2 \le t_3\), and similarly for other chains of inequalities.

For example, the translation \(\nu \) converts rule (2) into

$$\begin{aligned} \forall X(p(X)\rightarrow (q(X)\vee \lnot q(X))). \end{aligned}$$
(4)

Rule (3) is transformed into

$$p\rightarrow \forall N(\overline{0}\le N\le \overline{2} \rightarrow q(N)),$$

where N is an integer variable. The result of applying \(\nu \) to the rule

$$\begin{aligned} q(X,Y+\overline{1}) \leftarrow p(X,Y) \end{aligned}$$
(5)

is

$$\begin{aligned} \forall XN(p(X,N)\rightarrow q(X,N+\overline{1})). \end{aligned}$$
(6)

An interpretation of the signature \(\sigma _0\) is standard if

  • its domain of the sort general is the set of all precomputed terms;

  • its domain of the sort integer is the set of all numerals;

  • it interprets every precomputed term t as t;

  • it interprets \(\overline{m}+\overline{n}\) as \(\overline{m+n}\), and similarly for subtraction and multiplication;

  • it interprets every atomic sentence \({t_1 \prec t_2}\), where \(t_1\) and \(t_2\) are precomputed terms, as true iff the relation \(\prec \) holds for the pair \({(t_1,t_2)}\).

4 Translation \(\gamma \) and Its Properties

By \(\sigma '_0\) we denote the extension of the signature \(\sigma _0\) obtained by adding, for every predicate symbol p/n, a new n-ary predicate constant \((p/n)'\). An atomic formula \((p/n)'(\textbf{t})\) can be abbreviated as \(p'(\textbf{t})\). For the signature \(\sigma '_0\), the definition of a standard interpretation is the same as for the signature \(\sigma _0\) above.

For any formula F over the signature \(\sigma _0\), by \(F'\) we denote the formula over \(\sigma '_0\) obtained from F by replacing every occurrence of every predicate symbol p/n by \((p/n)'\).

The translation \(\gamma \), which relates logic of here-and-there with arithmetic to classical logic, maps formulas over \(\sigma _0\) to formulas over \(\sigma '_0\).Footnote 4 It is defined recursively:

  • \(\gamma F=F\) if F is atomic,

  • \(\gamma (\lnot F)=\lnot F'\),

  • \(\gamma (F\wedge G)=\gamma F \wedge \gamma G\),

  • \(\gamma (F\vee G)=\gamma F \vee \gamma G\),

  • \(\gamma (F\rightarrow G)=(\gamma F \rightarrow \gamma G)\wedge (F'\rightarrow G')\),

  • \(\gamma (\forall X\,F)=\forall X\,\gamma F\),

  • \(\gamma (\exists X\,F)=\exists X\,\gamma F\).

Our justification of Heuer’s procedure is given by Theorem 1 below. In the statement of the theorem, \(\mathcal {A}(p/n)\) stands for the formula \(\forall \textbf{X}(p(\textbf{X})\rightarrow p'(\textbf{X}))\), where \(\textbf{X}\) is an n-tuple of distinct general variables.

Theorem 1

Mini-gringo programs \(\varPi _1\), \(\varPi _2\) are strongly equivalent iff all standard interpretations of \(\sigma '_0\) satisfy the formula

$$\begin{aligned} \left( \bigwedge _{p/n}\mathcal {A}(p/n)\right) \rightarrow (\gamma \tau ^*\varPi _1\leftrightarrow \gamma \tau ^*\varPi _2), \end{aligned}$$
(7)

where the conjunction extends over all predicate symbols p/n that occur in \(\varPi _1\) or in \(\varPi _2\).

This theorem differs from the incorrect assertion mentioned in the introduction [12, Theorem 3] by requiring the interpretations to be standard. It shows that strong equivalence between \(\varPi _1\) and \(\varPi _2\) can be established by proving formula (7) in a first-order theory such that its axioms are satisfied by all standard interpretations. This is how Heuer’s procedure operates. It translates formula (7) into the TPTP language [26] using the algorithm implemented earlier as part of the proof assistant anthem [7]. Then the theorem prover vampire [14] is invoked to find a proof.

Results similar to the theorem above are due to Lin [23] (his Theorem 1 is about strong equivalence of propositional programs), to Pearce et al. [25] (their Theorem 6(iii) is about strong equivalence of propositional formulas), and to Ferraris et al. [9] (their Theorem 9 is about strong equivalence of first-order formulas without arithmetic).

Theorem 2 below shows that the assertion of Theorem 1 will remain true if we replace \(\tau ^*\) by the simpler and more natural translation \(\nu \) when a “regular” rule [18, Section 2] is translated. (The two main distinctive features of regular rules are that they do not use function symbols / and \(\backslash \), and do not apply arithmetical operations to intervals, as in \(X\times (Y\,..\,Z)\).)

For any mini-gringo program \(\varPi \), by \(\mu \varPi \) we denote the set consisting of

  • the formulas \(\nu R\) for all rules R of \(\varPi \) that are regular [18, Section 2], and

  • the formulas \(\tau ^* R\) for all rules R of \(\varPi \) that are not regular.

The assertion of Theorem 1 will remain true if we replace \(\tau ^*\) in its statement by \(\mu \):

Theorem 2

Mini-gringo programs \(\varPi _1\), \(\varPi _2\) are strongly equivalent iff all standard interpretations of \(\sigma '_0\) satisfy the formula

$$\begin{aligned} \left( \bigwedge _{p/n}\mathcal {A}(p/n)\right) \rightarrow (\gamma \mu \varPi _1\leftrightarrow \gamma \mu \varPi _2), \end{aligned}$$
(8)

where the conjunction extends over all predicate symbols p/n that occur in \(\varPi _1\) or in \(\varPi _2\).

5 Examples

Example 1

Let \(\varPi _1\) be rule (2), and let \(\varPi _2\) be the rule

$$\begin{aligned} q(X) \leftarrow p(X) \wedge not \ not \ q(X). \end{aligned}$$
(9)

Both rules are regular, so that \(\mu \varPi _1\) is (4), and \(\mu \varPi _2\) is

$$ \forall X(p(X) \wedge \lnot \lnot q(X) \rightarrow q(X)). $$

Then \(\gamma \mu \varPi _1\) is

$$ \forall X((p(X) \rightarrow (q(X) \vee \lnot q'(X))) \wedge (p'(X) \rightarrow (q'(X) \vee \lnot q'(X)))), $$

which is (classically) equivalent to

$$\begin{aligned} \forall X(p(X) \rightarrow (q(X) \vee \lnot q'(X))); \end{aligned}$$
(10)

\(\gamma \mu \varPi _2\) is

$$ \forall X((p(X) \wedge \lnot \lnot q'(X) \rightarrow q(X)) \wedge (p'(X) \wedge \lnot \lnot q'(X) \rightarrow q'(X))), $$

which is equivalent to

$$\forall X(p(X) \wedge q'(X) \rightarrow q(X)))$$

and furthermore to (10). Thus the consequent of (8) is in this case logically valid, and the programs are strongly equivalent by Theorem 2.

Example 2

Let \(\varPi _1\) be rule (5), and let \(\varPi _2\) be the rule

$$\begin{aligned} q(X,Y) \leftarrow p(X,Y-\overline{1}). \end{aligned}$$
(11)

Both rules are regular, so that \(\mu \varPi _1\) is (6), and \(\mu \varPi _2\) is

$$ \forall XN(p(X,N-\overline{1})\rightarrow q(X,N)). $$

Then \(\gamma \mu \varPi _1\) is

$$\forall XN( (p(X,N)\rightarrow q(X,N+\overline{1})) \wedge (p'(X,N)\rightarrow q'(X,N+\overline{1}))),$$

and \(\gamma \mu \varPi _2\) is

$$\forall XN( (p(X,N-\overline{1})\rightarrow q(X,N)) \wedge (p'(X,N-\overline{1})\rightarrow q'(X,N))).$$

The equivalence \(\gamma \mu \varPi _1\leftrightarrow \gamma \mu \varPi _2\) is a logical consequence of the formulas

$$ \forall N((N-\overline{1})+\overline{1}=N)\hbox { and }\forall N((N+\overline{1})-\overline{1}=N), $$

which are satisfied by all standard interpretations. The programs are strongly equivalent by Theorem 2.

In both examples above, we did not refer to the antecedent of implication (8); in each case, all standard interpretations satisfy the consequent. Strong equivalence between the program

$$\begin{array}{l} q\leftarrow p,\\ \leftarrow p \wedge \lnot q \end{array}$$

and its first rule is a case when the presence of the antecedents in implications (7) and (8) is essential. This example is due to Lin [23, Section 2].

6 Logic of Here-and-there with Arithmetic

Proofs of Theorems 1 and 2 are derived from a lemma that refers to an extension of the deductive system HTA. This extension, denoted by HTA\(^\omega \), can be described as the result of adding a few axiom schemas and inference rules to intuitionistic logic with equality for the signature \(\sigma _0\).

The list of additional axioms includes the Hosoi axiom schema [13]

$$F\vee (F\rightarrow G) \vee \lnot G$$

and the schema SQHT [22]

$$\exists X(F(X) \rightarrow \forall X\,F(X)).$$

It includes also the formulas

$$t_1\prec t_2$$

where \(\prec \) is one of comparison symbols (1), and \(t_1\), \(t_2\) are precomputed terms that satisfy the condition \(t_1\prec t_2\);

$$\lnot (t_1\prec t_2)$$

where \(\prec \) is \(=\) or one of comparison symbols (1), and \(t_1\), \(t_2\) are precomputed terms that do not satisfy the condition \(t_1\prec t_2\); and

$$ \overline{m+n}=\overline{m} + \overline{n},\qquad \overline{m-n}=\overline{m} - \overline{n},\qquad \overline{m \cdot n}=\overline{m} \times \overline{n} $$

for all integers m, n.

The additional inference rules are “omega-rules” with infinitely many premises:

$$\frac{F(t) \hbox { for all precomputed terms}~t}{\forall X\, F(X)}$$

where X is a general variable, and

$$\begin{aligned} \frac{F(\overline{n}) \hbox { for all integers}~n}{\forall N\, F(N)} \end{aligned}$$
(12)

where N is an integer variable [6, Section 5.3].

Main Lemma. Let \(\varPi _1\), \(\varPi _2\) be mini-gringo programs, and let \(F_i\) (\(i=1,2\)) be a sentence over \(\sigma _0\) that is equivalent to \(\tau ^*\varPi _i\) in HTA\(^\omega \). Programs \(\varPi _1\), \(\varPi _2\) are strongly equivalent iff every standard model of \(\mathcal {A}\) satisfies \(\gamma F_1\leftrightarrow \gamma F_2\), where \(\mathcal {A}\) denotes the set of formulas \(\mathcal {A}(p/n)\) for all predicate symbols p/n.

Conclusion

Theorem 2 shows that Heuer’s procedure can be modified by replacing \(\tau ^*R\) with the simpler translation \(\nu R\) when the rule R is regular. We expect that this modification will make the system easier to use, and we plan to verify this conjecture in collaboration with researchers at the University of Potsdam.