On Program Completion, with an Application to the Sum and Product Puzzle

Abstract

This paper describes a generalization of Clark’s completion that is applicable to logic programs containing arithmetic operations and produces syntactically simple, natural looking formulas. If a set of first-order axioms is equivalent to the completion of a program, then we may be able to find standard models of these axioms by running an answer set solver. As an example, we apply this “reverse completion” procedure to the Sum and Product Puzzle.

1 Introduction

Program completion (Clark 1978; Lloyd and Topor 1984) is a transformation that converts logic programs into sets of first-order formulas. The study of completion improved our understanding of the relationship between these two knowledge representation formalisms, and it has been used in the design of answer set solvers (Lierler and Maratea 2004; Lin and Zhao 2004).

The definition of completion has been extended to programs with operations on integers (Fandinno et al. 2020). That generalized completion process produces formulas in a two-sorted first-order language (Lifschitz et al. 2019, Section 5). In addition to “general” variables, which range over both symbolic constants and (symbols for) integers, a formula in that language may include also variables ranging over integers only. The need to use a language with two sorts is explained by the fact that function symbols in a first-order language are supposed to represent total functions, and arithmetic operations are not defined on symbolic constants. In answer set programming languages, applying arithmetic operations to symbolic constants is usually handled in a different way; when a rule is instantiated, a substituition is not used unless it is “well formed” (Calimeri et al. 2020, Section 3).

In this paper, the idea of a natural translation (Lifschitz 2021) is used to define a version of generalized completion that is limited to relatively simple (“regular”) rules but produces simpler, and more natural-looking, formulas. The modified completion operator is denoted by NCOMP, for “natural completion.” For example, the natural completion of the one-rule program:

(1) \begin{equation}\verb|even(2*X) :- X = -10..10.|\label{r1}\end{equation}

in the input language of the answer set solver clingo (Gebser et al. 2019) is the sentence:

(2) \begin{equation}\forall V (\textit{even}(V) \leftrightarrow \exists I (\overline {-10}\leq I\leq \overline{10} \,\land\, V = \overline 2*I)).\label{c1}\end{equation}

Here, V is a general variable, I is an integer variable, and $\overline {-10}$ , $\overline{10}$ , $\overline 2$ are “numerals” – object constants representing integers.

Two theorems, stated in Section 3.4 and proved in Section 5, relate stable models of a regular program to standard models of its completion (standard in the sense that they interpret symbols related to integers as usual in arithmetic). These theorems extend well-known results due to (Fages 1991).

If a set of first-order axioms happens to be equivalent to the completion of a regular program, then we may be able to find standard models of these axioms by running an answer set solver. As an example, we apply this “reverse completion” procedure to a formalization of the Sum and Product Puzzle (https://en.wikipedia.org/wiki/Sum_and_Product_Puzzle). From the perspective of knowledge representation and automated reasoning, that puzzle presents a challenge: express it in a formal declarative language so that the answer can be found, or at least verified, by an automated reasoning tool. This has been accomplished using first-order axioms for Kripke-style possible worlds and the first-order theorem prover fol (McCarthy 1990), and also using a modal logic of public announcements and the epistemic model checker demo (van Ditmarsch et al. 2005). More recently, Jayadev Misra proposed a simple first-order formalization that does not refer to possible worlds (Misra 2022, Section 2.8.3). In Section 4, we show that the answer to the puzzle can be found by applying the reverse completion process to a variant of his axiom set and then running clingo.

2 Review: Rules and formulas

2.1 Regular rules

To simplify presentation, we do not include here some of the programming constructs that are classified as regular in the previous publication on natural translations (Lifschitz 2021). As in the Abstract Gringo article (Gebser et al. 2015), rules will be written in abstract notation, which disregards some details related to representing rules by strings of ASCII characters. For example, rule (1) will be written as:

(3) \begin{equation}\textit{even}(\overline 2\times X) \leftarrow X = \overline {-10}\,..\,\overline{10}.\label{r1a}\end{equation}

We assume that three disjoint countably infinite sets of symbols are selected: numerals, symbolic constants, and (general) 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 the set of precomputed terms is chosen so that, for all integers m and n,

• • $\overline m < \overline n$ iff $m<n$ , and

• • every precomputed term t such that $\overline m < t < \overline n$ is a numeral.

Regular terms are formed from numerals and variables using the binary function symbols $+,\ -,\ \times$ . A regular atom is an expression of the form $p({\bf t})$ , where p is a symbolic constant and $\bf t$ is a tuple of symbolic constants and regular terms, separated by commas. Regular comparisons are expressions of the forms:

• • $t_1\prec t_2$ , where each of $t_1$ and $t_2$ is a symbolic constant or a regular term, and $\prec$ is one of the comparison symbols $=,\ \neq,\ <,\ >,\ \leq,\ \geq,$ and

• • $t_1=t_2\,..\,t_3$ , where $t_1$ , $t_2$ , and $t_3$ are regular terms.

A regular rule is an expression of the form:

(4) \begin{equation}\textit{Head} \leftarrow {\textit{Body,}}\label{rule}\end{equation}

where

• • Head is either a regular atom (then (4) is a basic rule), or a regular atom in braces (then (4) is a choice rule), or empty (then (4) is a constraint), and

• • Body is a conjunction, possibly empty, of (i) regular atoms, possibly preceded by not, and (ii) regular comparisons.

For example, (3) is a regular rule.

A regular program is a finite set of regular rules. This is a special case of Abstract Gringo programs (Gebser et al. 2015), and stable models of a regular program are understood in the sense of the semantic of Abstract Gringo. Thus, stable models are sets of ground atoms that do not contain arithmetic operations.

2.2 Two-sorted formulas

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 regular program $\Pi$ if some atom of the form $p(t_1,\dots,t_n)$ occurs in one of the rules of $\Pi$ .

For any regular program $\Pi$ , by $\sigma_\Pi $ we denote the two-sorted signature with the sort general and its subsort integer, which includes

• • every numeral as an object constant of the sort integer,

• • every symbolic constant as an object constant of the sort general,

• • the symbols $+$ , $-$ , $\times$ as binary function constants with the argument sorts integer and the value sort integer,

• • every predicate symbol $p/n$ that occurs in $\Pi$ as an n-ary predicate constant with the argument sorts general,

• • the symbols $\neq$ , $<$ , $>$ , $\leq$ , $\geq$ as binary predicate constants with the argument sorts general.

A formula over $\sigma_\Pi $ that has the form $(p/n)({\bf t})$ can be abbreviated as $p({\bf t})$ . This convention allows us to view regular atoms occurring in $\Pi$ as atomic formulas over $\sigma_\Pi $ .

Conjunctions of equalities and inequalities can be abbreviated as usual in algebra; for instance, $t_1\leq t_2\leq t_3$ stands for $t_1\leq t_2\land t_2\leq t_3$ . An equality between tuples of terms $(t_1,\dots,t_k)=(t'_1,\dots,t'_k)$ is understood as the conjunction $t_1=t'_1\land\cdots\land t_k=t'_k$ .

In this paper, integer variables are denoted by capital letters from the middle of the alphabet ( $I,\dots,N$ ), and general variables by letters from the end ( $U,\dots,Z$ ).

3 Completion

3.1 Replacing variables

In the process of constructing the natural completion of a regular program $\Pi$ , the bodies of rules of $\Pi$ will be transformed into formulas over $\sigma_\Pi$ . Since general variables are not allowed in a formula in the scope of an arithmetic operation, this process has to involve replacing some of them by integer variables.

A critical variable of a regular rule R is a general variable X such that at least one occurrence of X in R is in the scope of an arithmetic operation or is part of a comparison of the form $t_1=t_2\,..\,t_3$ . For every regular rule R, choose a function $f_R$ that maps its critical variables to pairwise distinct integer variables. This function $f_R$ is extended to other subexpressions of R as follows. For a tuple $\bf t$ of symbolic constants and regular terms, $f_R({\bf t})$ is the tuple of terms over $\sigma_\Pi$ obtained from $\bf t$ by replacing all occurrences of every critical variable X with the integer variable $f_R(X)$ . Applying $f_R$ to a regular atom and to a comparison that does not contain intervals is defined in a similar way. The result of applying $f_R$ to $\textit{not}\ A$ is defined as the formula $\neg f_R(A)$ , and the result of applying $f_R$ to a comparison $t_1=t_2\,..\,t_3$ is $f_R(t_2)\leq f_R(t_1)\leq f_R(t_3)$ . Finally, applying $f_R$ to the body $B_1\land B_2\land\cdots$ of R gives the formula $f_R(B_1)\land f_R(B_2)\land\cdots$ .

For instance, if R is rule (3) then the variable X is critical, and $f_R$ maps X to some integer variable I. It transforms the term $\overline 2\times X$ in the head into $\overline 2\times I$ , and the body $X = \overline {-10}\,..\,\overline{10}$ into $\overline {-10}\leq I\leq\overline{10}$ .

3.2 Completed definitions

Consider a regular program $\Pi$ and a predicate symbol $p/n$ that occurs in $\Pi$ . The definition of $p/n$ in $\Pi$ is the set of all rules of $\Pi$ that have the form:

(5) \begin{equation} p({\bf t}) \leftarrow {\textit{Body,}}\label{def1}\end{equation}

or

(6) \begin{equation} \{p({\bf t})\} \leftarrow {\textit{Body,}}\label{def2}\end{equation}

such that the length of the tuple $\bf t$ is n. The completed definition of $p/n$ in $\Pi$ is the sentence over $\sigma_\Pi $ constructed as follows. Choose a tuple $\bf V$ of n general variables that do not occur in $\Pi$ . For every rule R in the definition D of $p/n$ in $\Pi$ , by $F_R$ we denote the formula:

$$f_R(\textit{Body}) \land {\bf V}=f_R({\bf t}),$$

if R is (5), and

$$f_R(\textit{Body}) \land {\bf V}=f_R({\bf t}) \land p({\bf V}),$$

if R is (6). The completed definition of $p/n$ in $\Pi$ is the sentence:

(7) \begin{equation}\forall {\bf V} \left(p({\bf V}) \leftrightarrow \bigvee_{R\in D} \exists {\bf U}_R F_R \right),\label{compdef}\end{equation}

where ${\bf U}_R$ is the list of all variables occurring in $f_R(\textit{Body})$ or in $f_R({\bf t})$ .

For example, if the only rule R of the program is (3), and $p/n$ is $\textit{even}/1$ , then $F_R$ is

$$\overline {-10} \leq I\leq \overline{10} \,\land\, V = \overline 2*I,$$

where I is $f_R(X)$ . The completed definition of $\textit{even}/1$ is (2).The formula obtained from the completed definition (7) by replacing the global variables $\bf V$ with fresh integer variables will be called the arithmetic completed definition of $p/n$ in $\Pi$ . For example, the arithmetic completed definition of $\textit{even}/1$ in program (3) is

(8) \begin{equation}\forall N (\textit{even}(N) \leftrightarrow \exists I (\overline {-10}\leq I\leq \overline{10} \,\land\, N = \overline 2*I)).\label{arcomp}\end{equation}

The arithmetic completed definition is entailed by the completed definition, but not the other way around. For example, from formula (2) we can derive $\neg\textit{even}(t)$ for every symbolic constant t, but this conclusion is not warranted by formula (8).

3.3 Natural completion

The natural completion NCOMP $(\Pi)$ of a regular program $\Pi$ is the set of sentences that includes

• • for every predicate symbol $p/n$ occurring in $\Pi$ , its completed definition in $\Pi$ , and

• • for every constraint $\leftarrow\textit{Body}$ in $\Pi$ , the universal closure of the formula:

  $$\neg f_{\leftarrow Body}(\textit{Body}).$$

Consider, for example, the program that consists of rule (3), the choice rule:

(9) \begin{equation}\{\textit{foo}(X)\} \leftarrow \textit{even}(X),\label{r2}\end{equation}

and the constraint:

(10) \begin{equation}\leftarrow \textit{not}\ \textit{foo}(\overline 0).\label{r3}\end{equation}

Its natural completion consists of the completed definition (2) of $\textit{even}/2$ , the completed definition of $\textit{foo}/1$ :

$$\forall V(\textit{foo}(V) \leftrightarrow \exists X(\textit{even}(X) \land X=V \land \textit{foo}(V))),$$

which can be rewritten ¹ as:

$$\forall V(\textit{foo}(V) \to \textit{even}(V)),$$

and the sentence $\neg\neg \textit{foo}(\overline 0)$ , which is equivalent to $\textit{foo}(\overline 0)$ .

3.4 Relation to stable models

The Herbrand base of a regular program $\Pi$ is the set of all regular atoms $p(t_1,\dots,t_n)$ such that $p/n$ occurs in $\Pi$ and $t_1,\dots,t_n$ are precomputed terms. If S is a subset of the Herbrand base of $\Pi$ then $S^\uparrow$ is the interpretation of the signature $\sigma_\Pi$ defined as follows:

1. (i) the universe of the sort general in $S^\uparrow$ is the set of all precomputed terms;

2. (ii) the universe of the sort integer in $S^\uparrow$ is the set of all numerals;

3. (iii) for every precomputed term t, $S^\uparrow(t)=t$ ;

4. (iv) for every pair m, n of integers, $S^\uparrow(\overline m+\overline n)=\overline{m+n}$ , and similarly for subtraction and multiplication;

5. (v) for every pair $t_1,~t_2$ of precomputed terms, $S^\uparrow$ satisfies $t_1<t_2$ iff the relation $<$ holds for the pair $t_1$ , $t_2$ , and similarly for the other comparison symbols.

Theorem 1 For any regular program $\Pi$ and any subset S of its Herbrand base, if S is a stable model of $\Pi$ then $S^\uparrow$ satisfies NCOMP $(\Pi)$ .

The positive predicate dependency graph of a regular program $\Pi$ is the directed graph defined as follows. Its vertices are the predicate symbols $p/n$ occurring in $\Pi$ . It has an edge from $p/n$ to $q/m$ if $\Pi$ has a rule (4) such that

• • Head has the form $p(t_1,\dots,t_n)$ or $\{p(t_1,\dots,t_n)\}$ , and

• • one of the conjunctive terms of Body has the form $q(t_1,\dots,t_m)$ .

A regular program $\Pi$ is tight if its positive predicate dependency graph is acyclic.

For example, the positive predicate dependency graph of program (3), (9), and (10) has one edge, from $\textit{foo}/1$ to $\textit{even}/1$ . This program is tight.

Theorem 2 For any tight regular program $\Pi$ and any subset S of its Herbrand base, S is a stable model of $\Pi$ iff $S^\uparrow$ satisfies NCOMP $(\Pi)$ .

4 The puzzle

Two mathematicians, S and P, talk about two integers, M and N. S knows the sum $M+N$ , and P knows the product $M\times N$ . Both S and P know also that the integers are greater than 1; that their sum is not greater than 100; and that N is greater than M. The following conversation occurs:

1. 1. S says: P does not know M and N.

2. 2. P says: Now I know M and N.

3. 3. S says: Now I also know M and N.

What are M and N?

4.1 First-order axioms

Jayadev Misra’s approach to translating this puzzle into a first-order language (Misra 2022, Section 2.8.3) involves the use of binary predicates $b_0,\dots,b_3$ . The formula $b_0(M,N)$ expresses that before the beginning of the conversation, the pair M, N was considered a possible solution. This can be expressed by the formula:

(11) \begin{equation}b_0(M,N) \leftrightarrow 1 < M < N \land M+N \leq 100.\label{ax1}\end{equation}

The formula $b_1(M,N)$ expresses that M, N was considered a possible solution at step 1, that is, after hearing the words “P does not know M and N,” and so forth.

There are several ways to write axioms for $b_1$ , $b_2$ , and $b_3$ . One possibility is described below.

We say that an integer I is puzzling at time 0 if is there is more than one way to represent it as the product of two numbers J, K satisfying $b_0(J,K)$ :

(12) \begin{equation}\begin{array} r\!\!\textit{puzzling}_0(I)\leftrightarrow \exists J_1K_1J_2K_2(b_0(J_1,K_1)\land b_0(J_2,K_2)\hskip 2.25cm \\\land\, I=J_1\times K_1 =J_2\times K_2\land J_1\neq J_2).\end{array}\label{ax2}\end{equation}

We say that an integer I is possibly easy if it can be represented as the sum of two numbers J and K satisfying $b_0(J,K)$ such that $J\times K$ is not puzzling at time 0:

(13) \begin{equation}\textit{possibly_easy}(I) \leftrightarrow \exists JK(b_0(J,K)\land I = J+K\land\neg\textit{puzzling}_0(J\times K)).\label{ax3}\end{equation}

Then the assumption:

can be expressed by the axiom:

(14) \begin{equation}b_1(M,N) \leftrightarrow b_0(M,N)\land\neg\textit{possibly_easy}(M+N).\label{ax4}\end{equation}

We say that an integer I is puzzling at time 1 is there is more than one way to represent it as the product of two numbers J, K satisfying $b_1(J,K)$ :

(15) \begin{equation}\begin{array} r\!\!\textit{puzzling}_1(I)\leftrightarrow \exists J_1K_1J_2K_2(b_1(J_1,K_1)\land b_1(J_2,K_2)\hskip 2.25cm \\\land\, I=J_1\times K_1 =J_2\times K_2\land J_1\neq J_2).\end{array}\label{ax5}\end{equation}

The assumption

can be expressed by the axiom

(16) \begin{equation}b_2(M,N) \leftrightarrow b_1(M,N)\land\neg\textit{puzzling}_1(M\times N).\label{ax6}\end{equation}

We say that an integer I is puzzling at time 2 is there is more than one way to represent it as the sum of two numbers J, K satisfying $b_2(J,K)$ :

(17) \begin{equation}\begin{array} r\!\!\textit{puzzling}_2(I)\leftrightarrow \exists J_1K_1J_2K_2(b_2(J_1,K_1)\land b_2(J_2,K_2)\hskip 2.25cm \\\land\, I=J_1+K_1 =J_2+K_2\land J_1\neq J_2).\end{array}\label{ax7}\end{equation}

Finally, the assumption

can be expressed by the axiom:

(18) \begin{equation}b_3(M,N) \leftrightarrow b_2(M,N)\land\neg\textit{puzzling}_2(M+N).\label{ax8}\end{equation}

Since axioms (11)–(18) form a chain of explicit definitions, the predicates represented by the symbols:

(19)

are uniquely defined, assuming that variables range over the integers and that the symbols:

$$+\quad\times\quad<\quad\leq,$$

are interpreted in the standard way. To solve the Sum and Product Puzzle, we will calculate the extents of these predicates.

This will be accomplished by running clingo on the “reverse completion” of axioms (11)–(18).

4.2 Reverse completion

Consider the regular program

(20) \begin{equation}\begin{array}{rcl}b_0(\textit{XM},\textit{XN}) &\leftarrow& \overline 1 < \textit{XM}\,\land\, \textit{XM} < \textit{XN}\,\land\, \textit{XM}+\textit{XN} \leq \overline{100},\\\textit{puzzling}_0(\textit{XI}) &\leftarrow& b_0(\textit{XJ}_1,\textit{XK}_1)\,\land\, b_0(\textit{XJ}_2,\textit{XK}_2)\,\land\, \textit{XI} = \textit{XJ}_1 \times \textit{XK}_1\\&&\hskip 1cm \land\; \textit{XJ}_1 \times \textit{XK}_1=\textit{XJ}_2 \times \textit{XK}_2\,\land\, \textit{XJ}_1 \neq \textit{XJ}_2,\\\textit{possibly_easy}(\textit{XI}) &\leftarrow& b_0(\textit{XJ},\textit{XK})\,\land\, \textit{XI} = \textit{XJ}+\textit{XK}\\&&\land\; \textit{not}\ \textit{puzzling}_0(\textit{XJ} \times \textit{XK}),\\b_1(\textit{XM},\textit{XN})&\leftarrow& b_0(\textit{XM},\textit{XN})\,\land\, \textit{not}\ \textit{possibly_easy}(\textit{XM}+\textit{XN}),\\\textit{puzzling}_1(\textit{XI}) &\leftarrow& b_1(\textit{XJ}_1,\textit{XK}_1)\,\land\, b_1(\textit{XJ}_2,\textit{XK}_2)\,\land\, \textit{XI} = \textit{XJ}_1 \times \textit{XK}_1\\&&\hskip 1cm\land\; \textit{XJ}_1 \times \textit{XK}_1=\textit{XJ}_2 \times \textit{XK}_2\,\land\, \textit{XJ}_1 \neq \textit{XJ}_2,\\b_2(\textit{XM},\textit{XN}) &\leftarrow& b_1(\textit{XM},\textit{XN})\,\land\, \textit{not}\ \textit{puzzling}_1(\textit{XM} \times \textit{XN}),\\\textit{puzzling}_2(\textit{XI}) &\leftarrow& b_2(\textit{XJ}_1,\textit{XK}_1)\,\land\, b_2(\textit{XJ}_2,\textit{XK}_2)\,\land\, \textit{XI} = \textit{XJ}_1+\textit{XK}_1\\&&\hskip 1cm\land\; \textit{XJ}_1+\textit{XK}_1=\textit{XJ}_2+\textit{XK}_2\,\land\,\ \textit{XJ}_1 \neq \textit{XJ}_2,\\b_3(\textit{XM},\textit{XN}) &\leftarrow& b_2(\textit{XM},\textit{XN})\,\land\,\textit{not}\ \textit{puzzling}_2(\textit{XM}+\textit{XN}).\end{array}\label{sp}\end{equation}

These rules are obtained from equivalences (11)–(18) by:

• • replacing the equivalence signs $\leftrightarrow$ by left arrows,

• • dropping existential quantifiers,

• • replacing integer variables by general variables, and

• • replacing $\neg$ by not.

The natural completion of program (20) looks very similar to axiom set (11)–(18). There is a difference though: the former consists of formulas over the two-sorted signature described in Section 2.2, and the axioms formalizing the Sum and Product puzzle are one-sorted; there are no general variables in them. Consider then the arithmetic completed definitions of predicate symbols (19) (see Section 3.2). Those are one-sorted formulas, and they are equivalent to the universal closures of the corresponding axioms. For example, the completed definition of the predicate symbol $b_0/2$ in program (20) is

$$\begin{array} l\forall \textit{XM}\,\textit{XN}(b_0(\textit{XM},\textit{XN}) \leftrightarrow\\\hskip 1.8cm\exists M N(\overline 1 < M\land M < N\land M+N \leq \overline{100}\land \textit{XM}=M\land \textit{XN}=N)),\end{array}$$

and the arithmetic completed definition of this symbol is the one-sorted formula:

$$\begin{array} l\forall M_1N_1(b_0(M_1,N_1) \leftrightarrow\\\hskip 1.8cm\exists M N(\overline 1 < M\land M < N\land M+N \leq \overline{100}\land M_1=M\land N_1=N)).\end{array}$$

This formula is equivalent to the universal closure of axiom (11). Similarly, the arithmetic completed definition of $\textit{puzzling}_0/2$ is equivalent to the universal closure of axiom (12), and so forth.

4.3 Calculating the answer

By running clingo, we can determine that program (20) has a unique stable model S. By Theorem 1, the interpretation $S^\uparrow$ satisfies the completed definitions of symbols (19). It follows that $S^\uparrow$ satisfies the arithmetic completed definitions of these symbols, which are equivalent to axioms (11)–(18). In other words, S describes the extents of the predicates that we want to calculate. Since the only atom in S that begins with $b_3$ is $b_3(\overline 4,\overline{13})$ , the answer to the puzzle is

$$M=4,\ N=13.$$

To perform this calculation, we used version 5.6.0 of clingo. Earlier versions do not accept the first rule of the program as safe unless the expression:

$$\overline 1 < M\land M < N,$$

in the body is rewritten in the interval notation: $M=\overline 2\,..\,N-\overline 1$ .

5 Proofs

Proofs of Theorems 1 and 2 are based on similar results from an earlier publication (Fandinno et al. 2020), and we begin by reviewing them for the special case of regular programs.

5.1 Review: Completion according to Fandinno et al.

For any regular term t, the formula ${\textit{val}_{t}(Z)}$ , where Z is a general variable that does not occur in t, is defined recursively:

• • if t is a numeral or a variable then ${\textit{val}_{t}(Z)}$ is $Z=t$ ;

• • if t is $t_1 + t_2$ then ${\textit{val}_{t}(Z)}$ is

  $$\exists I J (Z=I + J \land {\textit{val}_{t_1}(I)} \land {\textit{val}_{t_2}(J)}),$$
  and similarly for $t_1-t_2$ and $t_1\times t_2$ .

If t is a symbolic constant then ${\textit{val}_{t}(Z)}$ stands for $Z=t$ . If $t_1,\dots,t_k$ is a tuple of symbolic constants and regular terms, and $Z_1,\dots,Z_k$ are pairwise distinct general variables that do not occur in $t_1,\dots,t_k$ , then ${\textit{val}_{t_1,\dots,t_k}({Z_1,\dots,Z_k})}$ stands for ${\textit{val}_{t_1}(Z_1)} \land \cdots \land {\textit{val}_{t_k}(Z_k)}$ . If t is $t_1\,..\,t_2$ then ${\textit{val}_{t}(Z)}$ stands for

$$\exists I J K ({\textit{val}_{t_1}(I)} \land {\textit{val}_{t_2}(J)} \land I\leq K \leq J \land Z=K).$$

The translation $\tau^B$ transforms expressions in the body of a regular rule into formulas as follows:

• • $\tau^B(p({\bf t}))$ is $\exists {\bf Z}{\textit{val}_{\bf t}({\bf Z})} \land p({\bf Z}))$ , where $\bf Z$ is a tuple of distinct program variables that do not occur in $\bf t$ ;

• • $\tau^B(\textit{not}\ p({\bf t}))$ is $\exists {\bf Z}({\textit{val}_{\bf_t}({\bf Z})} \land \neg p({\bf Z}))$ ;

• • $\tau^B(t_1\prec t_2)$ is $\exists Z_1 Z_2 ({\textit{val}_{t_1,t_2}({Z_1,Z_2})} \land Z_1\prec Z_2)$ ;

• • $\tau^B(t_1=t_2\,..\,t_3)$ is $\exists Z_1 Z_2 ({\textit{val}_{t_1}(Z_1)}\land {\textit{val}_{t_2\,..\,t_3}(Z_2)}\land Z_1=Z_2)$ ;

• • $\tau^B(B_1\land B_2\land\cdots)$ is $\tau^B(B_1)\land\tau^B(B_2)\land\cdots$ .

The completed definition of $p/n$ in $\Pi$ in the sense of Fandinno et al. is the sentence over $\sigma_\Pi$ constructed as follows. Choose a tuple $\bf V$ of n general variables that do not occur in $\Pi$ . For every rule R in the definition D of $p/n$ in $\Pi$ , by $F'_R$ we denote the formula:

$$\tau^B(\textit{Body}) \land {\textit{val}_{\bf t}({\bf V})}$$

if R is (5), and

$$\tau^B(\textit{Body}) \land {\textit{val}_{\bf t}({\bf V})} \land p({\bf V}),$$

if R is (6). The completed definition of $p/n$ in $\Pi$ according to Fandinno et al. is the sentence:

$$\forall {\bf V} \left(p({\bf V}) \leftrightarrow \bigvee_{R\in D} \exists {\bf U}'_R F'_R \right),$$

where ${\bf U}'_R$ is the list of all variables occurring in R.

For example, the completed definition of one-rule program (3) is

(21) \begin{equation}\forall V \left(\textit{even}(V) \leftrightarrow \exists X \left(\exists Z_1Z_2\left(Z_1=X\land \textit{val}_{\overline {-10}\,..\,\overline{10}}({Z_2}) \land Z_1=Z_2\right) \land \textit{val}_{\overline 2\times X}(V)\right)\right),\label{longcd}\end{equation}

where $\textit{val}_{\overline {-10}\,..\,\overline{10}}({Z_2})$ stands for

$$\exists I J K (I=\overline{-10} \land J=\overline{10} \land I\leq K \leq J \land Z_2=K),$$

and $\textit{val}_{\overline 2\times X}(V)$ stands for

$$\exists I J (V=I \times J \land I =\overline 2 \land J = X).$$

By COMP $(\Pi)$ , we denote the set of sentences that includes

• • for every predicate symbol $p/n$ occurring in $\Pi$ , its completed definition in $\Pi$ in the sense of Fandinno et al., and

• • for every constraint $\leftarrow\textit{Body}$ in $\Pi$ , the universal closure of the formula $\neg \tau^B(\textit{Body})$ .

Lemma 1 For any regular program $\Pi$ and any subset S of its Herbrand base, if S is a stable model of $\Pi$ then $S^\uparrow$ satisfies COMP $(\Pi)$ (Fandinno et al. 2020, Theorem 1).

Lemma 2 For any tight regular program $\Pi$ and any subset S of its Herbrand base, S is a stable model of $\Pi$ iff $S^\uparrow$ satisfies COMP $(\Pi)$ (Fandinno et al. 2020, Theorem 2).

5.2 Main Lemma

Theorems 1 and 2 follow from Lemmas 1 and 2 in view of the following fact proved below:

Main Lemma

For any regular program $\Pi$ , the formula NCOMP $(\Pi)$ is equivalent to COMP $(\Pi)$ in classical predicate calculus with equality.

In the statements of Lemmas 3–7, R is a regular rule, $\bf X$ is the list of its critical variables, and $\bf I$ is $f_R({\bf X})$ .

Lemma 3 If $\bf t$ is a list of symbolic constants and regular terms that occur in R, and $\bf Z$ is a list of pairwise distinct general variables that do not occur in R, then the formula

(22) \begin{equation}{\bf I}={\bf X} \to\forall {\bf Z}(val_{\bf t}({\bf Z}) \leftrightarrow {\bf Z}=f_R({\bf t})),\label{lem3f}\end{equation}

is logically valid (Lifschitz 2021, Lemma 1(i)).

Lemma 4 For any regular atom $p({\bf t})$ occurring in R, the formulas

$$\begin{array} l{\bf I}={\bf X} \to (f_R(p({\bf t})) \leftrightarrow \tau^B(p({\bf t}))),\\{\bf I}={\bf X} \to (f_R(not\ p({\bf t})) \leftrightarrow \tau^B(not\ p({\bf t}))),\end{array}$$

are logically valid (Lifschitz 2021, Lemma 1(iii,iv)).

Lemma 5 For any comparison $t_1\prec t_2$ occurring in R, the formula

$${\bf I}={\bf X} \to (f_R(t_1\prec t_2) \leftrightarrow \tau^B(t_1\prec t_2)),$$

is logically valid (Lifschitz 2021, Lemma 2).

Lemma 6 For any comparison $t_1 = t_2\,..\,t_3$ occurring in R, the formula

$${\bf I}={\bf X} \to (f_R(t_1 = t_2\,..\,t_3)\leftrightarrow \tau^B(t_1 = t_2\,..\,t_3)),$$

is logically valid (Lifschitz 2021, Lemma 4).

From Lemmas 4–6, we conclude:

Lemma 7 The formula

(23) \begin{equation}{\bf I}={\bf X} \to (f_R(Body)\leftrightarrow \tau^B(Body)),\label{l7}\end{equation}

where Body is the body of R, is logically valid.

Lemma 8 Let R be a regular rule with the body $B_1\land B_2\land \cdots$ .

• (a) For every variable X that occurs in $B_i$ in the scope of an arithmetic operation, the formula

  (24) \begin{equation} \tau^B(B_i)\to\exists I(I=X), \label{l8} \end{equation}
  is logically valid.

• (b) If $B_i$ is a comparison of the form $t_1=t_2\,..\,t_3$ then formula (24) is logically valid for every variable X that occurs in $B_i$ .

(Lifschitz 2021, Lemmas 7 and 9).

From Lemma 8, we conclude:

Lemma 9 Let R be a regular rule, and let $\bf X$ be the list of its critical variables. The formula

(25) \begin{equation} \tau^B(Body) \to \exists {\bf I}({\bf I}={\bf X}), \label{l9} \end{equation}

where Body is the body of R and $\bf I$ is $f_R({\bf X})$ , is logically valid.

In the following lemma, R is a regular rule of form (5) or (6), $F_R$ and ${\bf U}_R$ are as defined in Section 3.2, and $F'_R$ and ${\bf U}'_R$ are as defined in Section 5.1.

Lemma 10 The formula $\exists {\bf U}'_R F'_R$ is equivalent to $\exists {\bf U}_R F_R$ .

Proof Let $\bf X$ be the list of all critical variables of R, and let $\bf I$ be $f_R({\bf X})$ . It is sufficient to prove the equivalence:

$$\exists {\bf I}\, F'_R\leftrightarrow \exists {\bf X}\, F_R.$$

We consider the case when R is (5), so that $F_R$ is

$$\tau^B(\textit{Body}) \land {\textit{val}_{\bf t}({\bf V}),}$$

and $F'_R$ is

$$f_R(\textit{Body}) \land {\bf V}=f_R({\bf t}).$$

The case of rule (6) is similar.

Left-to-right: assume $\exists {\bf I}(f_R(\textit{Body}) \land {\bf V}=f_R({\bf t}))$ . Since $\forall{\bf I}\exists{\bf X}({\bf I}={\bf X})$ , we can conclude that

$$\exists {\bf I}(\exists {\bf X}({\bf I}={\bf X}) \land f_R(\textit{Body})\land {\bf V}=f_R({\bf t})).$$

It follows that

$$\exists {\bf IX}({\bf I}={\bf X} \land f_R(\textit{Body})\land {\bf V}=f_R({\bf t})),$$

because the critical variables $\bf X$ do not occur in the formula $f_R(\textit{Body})\land {\bf V}=f_R({\bf t})$ . Then $\exists {\bf IX}(\tau^B(\textit{Body})\land {\textit{val}_{\bf t}({\bf V})})$ follows using the iniversal closures of (22) and (23). Since the integer variables $\bf I$ do not occur in $\tau^B(\textit{Body})\land {\textit{val}_{\bf t}({\bf V})}$ , the quantifiers binding $\bf I$ can be dropped.

Right-to-left: assume $\exists {\bf X} (\tau^B(\textit{Body})\land {\textit{val}_{\bf t}({\bf V})})$ . We can conclude, using the universal closure of (25), that

$$\exists {\bf X}(\exists {\bf I}({\bf I}={\bf X})\land \tau^B(\textit{Body})\land {\textit{val}_{\bf t}({\bf V})}).$$

It follows that

$$\exists {\bf IX}({\bf I}={\bf X}\land \tau^B(\textit{Body})\land {\textit{val}_{\bf t}({\bf V})}),$$

because the integer variables $\bf I$ do not occur in the formula $\tau^B(\textit{Body})\land {\textit{val}_{\bf t}({\bf V})})$ . Then $\exists {\bf IX}(f_R(\textit{Body})\land {\bf V}=f_R({\bf t}))$ follows using the universal closures of (22) and (23). Since the critical variables $\bf X$ do not occur in $f_R(\textit{Body})\land {\bf V}=f_R({\bf t})$ , the quantifiers binding $\bf X$ can be dropped.

Lemma 11 If R is a regular constraint $\leftarrow Body$ then the universal closures of the formulas $\neg f_R(Body)$ and $\neg \tau^B(Body)$ are equivalent to each other.

Proof Let $\bf X$ be the list of all critical variables of R, and let $\bf I$ be $f_R({\bf X})$ . It is sufficient to prove the equivalence:

$$\exists {\bf I}\, f_R(\textit{Body}) \leftrightarrow \exists {\bf X}\, \tau^B(\textit{Body}),$$

because it entails

$$\forall {\bf I}\neg f_R(\textit{Body}) \leftrightarrow \forall {\bf X}\neg \tau^B(\textit{Body}),$$

and consequently entails also the equivalence between the universal closures of $\neg f_R(Body)$ and $\neg \tau^B(Body)$ .

Left-to-right: assume $\exists {\bf I}\, f_R(\textit{Body})$ . Since $\forall{\bf I}\exists{\bf X}({\bf I}={\bf X})$ , we can conclude that

$$\exists {\bf IX}({\bf I}={\bf X} \land f_R(\textit{Body})),$$

because the critical variables $\bf X$ do not occur in $f_R(\textit{Body})$ . Then $\exists {\bf IX}\, \tau^B(\textit{Body})$ follows using the iniversal closure of (23). Since the integer variables $\bf I$ do not occur in $\tau^B(\textit{Body})$ , the quantifiers binding $\bf I$ can be dropped.

Right-to-left: assume $\exists {\bf X}\, \tau^B(\textit{Body})$ . We can conclude, using the universal closure of (25), that

$$\exists {\bf IX}({\bf I}={\bf X}\land \tau^B(\textit{Body})),$$

because the integer variables $\bf I$ do not occur in $\tau^B(\textit{Body})$ . Then $\exists {\bf IX}\, f_R(\textit{Body})$ follows using the universal closure of (23). Since the critical variables $\bf X$ do not occur in $f_R(\textit{Body})$ , the quantifiers binding $\bf X$ can be dropped.

Main Lemma follows from Lemmas 10 and 11.

6 Discussion

In the presence of arithmetic operations, the completed definition in the sense of Fandinno et al. is often longer and syntactically more complex than the “natural” completed definition introduced in Section 3.2; compare, for instance, formula (21) with (2). On the other hand, the approach of Fandinno et al. is applicable to some types of rules that are accepted by clingo but are not regular, such as

These two rules can be easily rewritten as regular rules:

Regularizing the rule

in a similar way gives the rule:

that the current version of clingo considers unsafe.

The translation COMP is used in the design of the proof assistant anthem (Fandinno et al. 2020), and our Main Lemma shows that NCOMP can be employed in the same way. In the process of interacting with anthem, the user often has to read and modify completion formulas. A version of anthem that implements natural completion would make this work easier.

It would be interesting to extend the definition of NCOMP to programs containing conditional literals (Gebser et al. 2019, Section 3.1.11). Such an extension would make the reverse completion process applicable to some formulas that are more complex syntactically than the current version. For instance, it may be able to handle the formula:

\begin{align*}&b_1(M,N)\, \leftrightarrow\\&\qquad b_0(M,N)\land\neg\exists JK(b_0(J,K)\land M+N = J+K\land\neg\textit{puzzling}_0(J\times K)),\end{align*}

which can replace axioms (13), (14) in the first-order formalization of the Sum and Product Puzzle.