Strong Equivalence and Program Structure in Arguing Essential Equivalence between Logic Programs

TL;DR

This paper explores formal relationships between different answer set programs, providing theoretical results and a system for automatic program rewriting to improve efficiency in logic programming.

Contribution

It introduces formal results relating program rewritings and proves the correctness of an automatic rewriting system for answer set programs.

Findings

Formal links between answer set program rewritings

Proof of correctness for the Projector system

Enhanced understanding of program equivalence and structure

Abstract

Answer set programming is a prominent declarative programming paradigm used in formulating combinatorial search problems and implementing different knowledge representation formalisms. Frequently, several related and yet substantially different answer set programs exist for a given problem. Sometimes these encodings may display significantly different performance. Uncovering precise formal links between these programs is often important and yet far from trivial. This paper presents formal results carefully relating a number of interesting program rewritings. It also provides the proof of correctness of system Projector concerned with automatic program rewritings for the sake of efficiency. Under consideration in Theory and Practice of Logic Programming (TPLP).

Equations

$$\begin{array}[]{l}a_{0}\leftarrow a_{1},\dots,a_{l},not\ a_{l+1},\dots,not\ a_{m},not\ not\ a_{m+1},\dots,not\ not\ a_{n},\end{array}$$

$$a_0\leftarrow a_1,\dots ,a_l,$$

$$a_1\wedge \cdots \wedge a_l\to a_0.$$

$$p\leftarrow q,notnotp.$$

$$\begin{array}[]{r}a_{1}\wedge\dots\wedge a_{l}\wedge\neg a_{l+1}\wedge\dots\wedge\neg a_{m}\wedge\neg\neg a_{m+1}\wedge\dots\wedge\neg\neg a_{n}\rightarrow a_{0}.\end{array}$$

$$\begin{array}[]{l}\neg q\rightarrow p\\ \neg p\rightarrow q\end{array}$$

$$\{p\}.$$

$$a_1\wedge \cdots \wedge a_l\wedge \neg a_{l+1}\wedge \cdots \wedge \neg a_m\wedge \neg \neg a_{m+1}\wedge \cdots \wedge \neg \neg a_n,$$

$$def(q)\to q$$

$$\neg q\to p$$

$$\begin{array}[]{l}r\rightarrow p\\ \neg q\rightarrow r\end{array}$$

$$\mathbf{caused}{l}_0\mathbf{if}{l}_1\wedge \cdots \wedge l_m$$

$$\mathbf{caused}{l}_0\mathbf{if}{l}_1\wedge \cdots \wedge l_m\mathbf{after}{l}_{m+1}\wedge \cdots \wedge l_n$$

$$l_1\wedge \cdots \wedge l_m\to l_0$$

$$l_1\wedge \cdots \wedge l_m$$

$$l_{m+1}\wedge \cdots \wedge l_n.$$

$$\begin{array}[]{l}\hbox{$\mathbf{caused}\ $}wet\hbox{$\ \mathbf{if}\ $}inWater\\ putInWater\ \hbox{\bf causes}\ inWater\\ \hbox{\bf inertial}\ inWater,\neg inWater,wet,\neg wet\end{array}$$

$$\begin{array}[]{l}\hbox{$\mathbf{caused}\ $}wet\hbox{$\ \mathbf{if}\ $}inWater\\ \hbox{$\mathbf{caused}\ $}inWater\hbox{$\ \mathbf{if}\ $}\top\ \hbox{\bf after}\ putInWater\\ \hbox{$\mathbf{caused}\ $}inWater\hbox{$\ \mathbf{if}\ $}inWater\ \hbox{\bf after}\ inWater\\ \hbox{$\mathbf{caused}\ $}\neg inWater\hbox{$\ \mathbf{if}\ $}\neg inWater\ \hbox{\bf after}\ \neg inWater\\ \hbox{$\mathbf{caused}\ $}wet\hbox{$\ \mathbf{if}\ $}wet\ \hbox{\bf after}\ wet\\ \hbox{$\mathbf{caused}\ $}\neg wet\hbox{$\ \mathbf{if}\ $}\neg wet\ \hbox{\bf after}\ \neg wet\\ \end{array}$$

$$\neg inWater\text{leavevmode}\neg wet,\text{leavevmode}\neg inWater\text{leavevmode}wet,\text{leavevmode}inWater\text{leavevmode}wet$$

$$\small\begin{array}[]{ll}\langle\neg inWater\leavevmode\nobreak\ \neg wet,\neg putInWater,\neg inWater\leavevmode\nobreak\ \neg wet\rangle,&\langle\neg inWater\leavevmode\nobreak\ \neg wet,putInWater,inWater\leavevmode\nobreak\ wet\rangle,\\ \langle\neg inWater\leavevmode\nobreak\ wet,\neg putInWater,\neg inWater\leavevmode\nobreak\ wet\rangle,&\langle\neg inWater\leavevmode\nobreak\ wet,putInWater,inWater\leavevmode\nobreak\ wet\rangle,\\ \langle inWater\leavevmode\nobreak\ wet,\neg putInWater,inWater\leavevmode\nobreak\ wet\rangle,&\langle inWater\leavevmode\nobreak\ wet,putInWater,inWater\leavevmode\nobreak\ wet\rangle.\\ \end{array}\normalsize$$

$$-{\sigma }^{fl}=\{-a\mid a\in {\sigma }^{fl}\}$$

$$-{\sigma }^{act}=\{-a\mid a\in {\sigma }^{act}\}.$$

$$\hat{l}=\{\begin{array}{l}aiflis\; an\; atoma\\ -aiflis\; a\; literal\; of\; the\; form\; \neg a\end{array}$$

$$\overline{l}=\{\begin{array}{l}-aiflis\; an\; atoma\\ aiflis\; a\; literal\; of\; the\; form\; \neg a\end{array}$$

$$\perp \leftarrow a,-a$$

$$\perp \leftarrow nota,not-a$$

$$\widehat{l_0}(t)\leftarrow not\overline{l_1}(t),\dots ,not\overline{l_m}(t)$$

$$\begin{array}[]{r}\hbox{$\widehat{l_{0}}$}(t+1)\leftarrow\ not\ \hbox{$\overline{l_{1}}$}(t+1),\dots,\ not\ \hbox{$\overline{l_{m}}$}(t+1),\hbox{$\widehat{l_{m+1}}$}(t),\dots,\ \hbox{$\widehat{l_{n}}$}(t),\end{array}$$

$$\begin{array}[]{l}\hbox{$\hbox{-}{a}$}(0)\leftarrow\ not\ a(0)\\ a(0)\leftarrow\ not\ \hbox{$\hbox{-}{a}$}(0),\\ \end{array}$$

$$\begin{array}[]{l}\hbox{$\hbox{-}{a}$}\leftarrow\ not\ a\\ a\leftarrow\ not\ \hbox{$\hbox{-}{a}$}.\\ \end{array}$$

Full text

1 Introduction

Answer set programming (ASP) is a prominent knowledge representation paradigm with roots in logic programming [Brewka et al. (2011)]. It is frequently used for addressing combinatorial search problems. It has also been used to provide implementations and/or translational semantics to other knowledge representation formalisms such as action languages including languages $\mathcal{B}$ [Gelfond and Lifschitz (1998), Section 5], $\mathcal{C}$ [Lifschitz and Turner (1999)], $\mathcal{BC}$ [Lee et al. (2013)], \hbox{\mathcal{C}}+ [Giunchiglia et al. (2004), Babb and Lee (2013)], and $\mathcal{AL}$ [Gelfond and Kahl (2014), Section 8].

In answer set programming, a given computational problem is represented by a declarative program, also called a problem encoding, that describes the properties of a solution to the problem. Then, an answer set solver is used to generate answer sets for the program. These answer sets correspond to solutions to the original problem. As answer set programming evolves, new language features come to life providing means to reformulations of original problem encodings. Such new formulations often prove to be more intuitive and/or more concise and/or more efficient. Similarly, when a software engineer tackles a problem domain by means of answer set programming it is a common practice to first develop a/some solution to a problem and then rewrite this solution iteratively using such techniques, for example, as projection to gain a better performing encoding [Buddenhagen and Lierler (2015)]. These common processes bring a scientific question to light: what are the formal means to argue the correctness of renewed formulations of the original encodings to problems? In other words, under the assumption that the original encoding to a problem is correct, how can we argue that a related and yet different encoding is also correct? In addition, automated ASP program rewriting systems come to life. Systems lpopt [Bichler et al. (2016)] and  projector [Hippen and Lierler (2019)] exemplify such a trend. These tools rewrite an original program into a new one with the goal of improving an ASP solver’s performance. Once again, formal means are necessary to claim the correctness of such systems. We note that the last section of this work is devoted to the claim of correctness of system projector.

It has been long recognized that studying various notions of equivalence between programs under the answer set semantics is of crucial importance. Researchers proposed and studied strong equivalence [Lifschitz et al. (2001), Lifschitz et al. (2007)], uniform equivalence [Eiter and Fink (2003)], relativized strong and uniform equivalences [Woltran (2004)]. Another related approach is the study of forgetting [Leite (2017)]. Also, equivalences relative to specified signatures were considered [Erdoğan and Lifschitz (2004), Eiter et al. (2005), Woltran (2008), Harrison and Lierler (2016)]. In most of the cases the programs considered for studying the distinct forms of equivalence are propositional. Works by \citeNeit06, \citeNeit06a, \citeNlif07a, \citeNoet08, \citeNpea12, and \citeNhar16 are exceptions. These authors consider programs with variables (or, first-order programs). It is first-order programs that ASP knowledge engineers develop. Thus, theories on equivalence between programs with variables are especially important as they can lead to more direct arguments about properties of programs used in practice.

In this paper we show how concepts of strong equivalence and so called conservative extension are of use in illustrating that two programs over different signatures and with significantly different structure are “essentially the same” or “essentially equivalent” in a sense that they capture solutions to the same problem. Let us make the concept of an essential equivalence between problem’s encodings precise. We use the same notion of the search problem as Brewka et al. \shortcitebre11. Quoting from their work, a search problem $P$ consists of a set of instances with each instance $I$ assigned a finite set $S_{P}(I)$ of solutions. We say that logic program $\Pi_{P}(\cdot)$ is an encoding of $P$ when for any instance $I$ of this problem, the solutions to $I$ – the elements of set $S_{P}(I)$ – can be reconstructed from the answer sets of program $\Pi_{P}(I)$. We say that encodings $\Pi_{P}(\cdot)$ and $\Pi^{\prime}_{P}(\cdot)$ are essentially equivalent, when given any instance $I$ of problem $P$ the answer sets of programs $\Pi_{P}(I)$ and $\Pi^{\prime}_{P}(I)$ are in one-to-one correspondence. The paper has two parts. In the first part we consider propositional programs. In the second part, we move to the programs with variables. These parts can be studied separately. The first one is appropriate for researchers who are not yet deeply familiar with answer set programming theory and are interested in learning formal details. The second part111This part of the paper is a substantially extended version of the paper presented at PADL 2019 [Lierler (2019)]. is geared towards answer set programming practitioners providing them with theoretical grounds and tools to assist them in program analysis and formal claims about the developed encodings and their relations. In both of these parts we utilize running examples stemming from the literature. For instance, for the case of propositional programs we study two distinct ASP formalizations of action language $\mathcal{C}$. In the case of first-order programs, we study two distinct formalizations of planning modules for action language $\mathcal{AL}$ given in [Gelfond and Kahl (2014), Section 9]. Namely,

a Plan-choice formalization that utilizes choice rules and aggregate expressions, 2. 2.

a Plan-disj formalization that utilizes disjunctive rules.

In both cases we identify interesting results.

Paper Outline.

The paper is structured as follows. Section 2.1 presents the concepts of (i) a propositional logic program, (ii) strong equivalence between propositional logic programs, and (iii) a propositional logic program being a conservative extension of another one. Section 2.2 introduces a rewriting technique frequently used by ASP developers when a new auxiliary proposition is introduced in order to denote a conjunction of other propositions. Then these conjunctions are safely renamed by the auxiliary atom. We refer to this process as explicit definition rewriting and illustrate its correctness. We continue by reviewing action language $\mathcal{C}$ in Section 2.3, which serves a role of a running example in the first part of the paper. In Section 2.4.1, we present an original, or gold standard, translation of language $\mathcal{C}$ to a logic program. Section 2.4.2 states a modern formalization stemming from the translation of a syntactically restricted fragment of \hbox{\mathcal{C}}+. At last, in Section 2.4.3 we showcase how we can argue on the correctness of a modern formalization by stating the formal relation between the original and modern translations of language $\mathcal{C}$. An interested reader may proceed to the Appendix to find the details of the proof of the claim. There, we utilize reasoning by ”weak” natural deduction and a formal result on explicit definition rewriting. (A weak natural deduction system is reviewed in the Appendix.) We also note that there is an interesting by product of our analysis: we establish that \hbox{\mathcal{C}}+ can be viewed as a true generalization of the language $\mathcal{C}$ to the case of multi-valued fluents.

We start the second part of the paper by presenting the Plan-choice and Plan-disj programs at the onset of Section 3. We then introduce the logic program language called RASPL-1 in Section 3.2. The semantics of this language is given in terms of the SM operator reviewed in Section 3.2.2. In Section 3.2.3, we review the concept of strong equivalence for first order programs. Section 3.3 is devoted to a sequence of formal results on program rewritings. One of the findings of this work is lifting the results by \citeNben94 to the first order case. Earlier work claimed that propositional head-cycle-free disjunctive programs can be rewritten to nondisjunctive programs by means of simple syntactic transformation. Here we not only generalize this result to the case of first-order programs, but also illustrate that at times we can remove disjunction from parts of a program even though the program is not head-cycle-free. Another important contribution of the work is lifting the Completion Lemma and the Lemma on Explicit Definitions stated in [Ferraris (2005), Ferraris and Lifschitz (2005)] from the case of propositional theories and propositional logic programs to first-order programs. In conclusion, in Section 3.4 we review a frequently used rewriting technique called projection that often produces better performing encodings. We illustrate the utility of the presented theoretical results as they can be used to argue the correctness of distinct versions of projection that also include rules with aggregates. In particular, the last formal result stated in the paper provides a proof of correctness of system projector. The Lemma on Explicit Definitions presented here is essential in this argument.

The Appendix provides the proofs for the formal results presented in the paper.

2 Propositional Programs

2.1 Traditional Logic Programs and their Equivalences

A (traditional logic) program is a finite set of rules of the form

[TABLE]

$(0\leq l\leq m\leq n)$, where each $a_{0}$ is an atom or $\bot$ and each $a_{i}$ ($1\leq i\leq n$) is an atom, $\top$, or $\bot$ . The expression containing atoms $a_{1}$ through $a_{n}$ is called the body of the rule. Atom $a_{0}$ is called a head.

We define the answer sets of a traditional program $\Pi$ following [Lifschitz et al. (1999)]. We say that a program is basic, when it does not contain connective $not$. In other words a basic program consists of rules

[TABLE]

where each $a_{0}$ is an atom or $\bot$ and each $a_{i}$ ($1\leq i\leq l$) is an atom, $\top$, or $\bot$. We say that a set $X$ of atoms satisfies rule (2) if it satisfies the implication

[TABLE]

We say that a set $X$ of atoms is an answer set of a basic program $\Pi$ if $X$ is a minimal set among sets satisfying all rules of $\Pi$.

A reduct of a program $\Pi$ with respect to a set $X$ of atoms, denoted by $\Pi^{X}$, is constructed as follows. For each rule (1) in $\Pi$

when $not\ not\ a_{i}$ ($m+1\leq i\leq n$) is such that $a_{i}\in X$, replace this expression with $\top$, otherwise replace it with $\bot$, 2. 2.

when $not\ a_{i}$ ($l+1\leq i\leq m$) is such that $a_{i}\in X$, replace this expression with $\bot$, otherwise replace it with $\top$.

It is easy to see that a reduct of a program forms a basic program. We say that a set $X$ of atoms is an answer set of a traditional program if it is an answer set for the reduct $\Pi^{X}$.

In the later part of the paper we present the definition of an answer set for programs with variables by means of operator SM [Ferraris et al. (2011)]. \citeNfer09 show in which sense SM operator captures the semantics of answer sets presented here.

According to [Ferraris and Lifschitz (2005)] and [Ferraris (2005)], rules of the form (1) are sufficient to capture the meaning of the choice rule construct commonly used in answer set programming. For instance, the choice rule ${\{p\}\leftarrow q}$ is understood as the rule

[TABLE]

We intuitively read this rule as given $q$ atom $p$ may be true. We use choice rule notation in the sequel.

Strong Equivalence

Traditional programs $\Pi_{1}$ and $\Pi_{2}$ are strongly equivalent [Lifschitz et al. (2001)] when for every program $\Pi$, programs $\Pi_{1}\cup\Pi$ and $\Pi_{2}\cup\Pi$ have the same answer sets. In addition to introducing strong equivalence, \citeNlif01 also illustrated that traditional programs can be associated with the propositional formulas and a question whether the programs are strongly equivalent can be turned into a question whether the respective propositional formulas are equivalent in the logic of here-and-there (HT-logic) [Lukasiewicz (1941)], an intermediate logic between classical and intuitionistic logics.

We follow the steps of [Lifschitz et al. (2001)] and identify a rule (1) with the propositional formula

[TABLE]

Conservative Extensions

\citeN

har16 defined the notion of a conservative extension for the case of logic programs. Similarly to strong equivalence, it attempts to capture the conditions under which we can rewrite parts of the program and yet guarantee that the resulting program is not different in an essential way from the original one. Conservative extensions allow us to reason about rewritings even when the rules in question have different signatures.

For a program $\Pi$, by $atoms(\Pi)$ we denote the set of atoms occurring in $\Pi$. Let $\Pi$ and $\Pi^{\prime}$ be programs such that $atoms(\Pi)\subseteq atoms(\Pi^{\prime})$. We say that program $\Pi^{\prime}$ is a conservative extension of $\Pi$ if $X\mapsto X\cap atoms(\Pi)$ is a 1-1 correspondence between the answer sets of $\Pi^{\prime}$ and the answer sets of $\Pi$. For instance, program

[TABLE]

is a conservative extension of the program containing the single choice rule

[TABLE]

Furthermore, given program $\Pi$ such that (i) it contains rule $\{p\}$ and (ii) $q\not\in atoms(\Pi)$, a program constructed from $\Pi$ by replacing $\{p\}$ with (4) is a conservative extension of $\Pi$.

2.2 On Explicit Definition Rewriting

We now turn our attention to a common rewriting technique based on explicit definitions and illustrate its correctness. This technique introduces an auxiliary proposition in order to denote a conjunction of other propositions. Then these conjunctions are safely renamed by the auxiliary atom in the remainder of the program.

We call a formula basic conjunction when it is of the form

[TABLE]

where each $a_{i}$ ($1\leq i\leq n$) is an atom, $\top$, or $\bot$. For example, the body of any rule in a traditional program is a basic conjunction.

Let $\Pi$ be a program, $Q$ be a set of atoms that do not occur in $\Pi$. For an atom $q\in Q$, let $def(q)$ denote a basic conjunction (5), where $a_{i}$ ($1\leq i\leq n$) in $atoms(\Pi)$. We say that $def(q)$ is an explicit definition of $q$ in terms of $\Pi$. By $def(Q)$ we denote a set of formulas $def(q)$ for each atom $q\in Q$. We assume that all these formulas are distinct. Program $\Pi[Q,def(Q)]$ is constructed from $\Pi$ as follows:

• •

all occurrences of all formulas $def(q)$ from $def(Q)$ in some body of $\Pi$ are replaced by respective $q$,

• •

for every atom $q\in Q$ a rule of the form

[TABLE]

is added to the program.

For instance,let $\Pi$ be a program

[TABLE]

and $def(r)$ be a formula $\neg q$, then $\Pi[\{r\},\{def(r)\}]$ follows

[TABLE]

The proposition below supports the fact that the latter program is a conservative extension of the former. It is an important claim as although this kind of rewriting is very frequently used in practice to the best of our knowledge this is the first time it has been formally claimed.

Proposition 1

Let $\Pi$ be a program, $Q$ be a set of atoms that do not occur in $\Pi$, and $def(Q)$ be a set composed of explicit definitions for each element in $Q$ in terms of $\Pi$. Program $\Pi[Q,def(Q)]$ is a conservative extension of $\Pi$.

2.3 Review of Action Language C

This review of action language $\mathcal{C}$ follows [Lifschitz and Turner (1999)].

We consider a set $\sigma$ of propositional symbols partitioned into the fluent names $\sigma^{fl}$ and the elementary action names $\sigma^{act}$. An action is an interpretation of $\sigma^{act}$. Here we only consider what \citeNlif99b call definite action descriptions so that we only define this special class of $\mathcal{C}$ action descriptions.

Syntactically, a $\mathcal{C}$  action description is a set of static and dynamic laws. Static laws are of the form

[TABLE]

and dynamic laws are of the form

[TABLE]

where

• •

$l_{0}$ is either a literal over $\sigma^{fl}$ or the symbol $\bot$,

• •

$l_{i}$ ($1\leq i\leq m$) is a literal in $\sigma^{fl}$,

• •

$l_{i}$ ($m+1\leq i\leq n$) is a literal in $\sigma$ , and

• •

conjunctions $l_{1}\wedge\cdots\wedge l_{m}$ and $l_{m+1}\wedge\cdots\wedge l_{n}$ are possibly empty and understood as $\top$ in this case.

In both laws, the literal $l_{0}$ is called the head.

Semantically, an action description defines a graph or a transition system. We call nodes of this graph states and directed edges transitions. We now define these concepts precisely. Consider an action description $D$. A state is an interpretation of $\sigma^{fl}$ that satisfies implication

[TABLE]

for every static law (6) in $D$. A transition is any triple $\langle s,a,s^{\prime}\rangle$, where $s$, $s^{\prime}$ are states and $a$ is an action; $s$ is the initial state of the transition, and $s^{\prime}$ is its resulting state. A literal $l$ is caused in a transition $\langle s,a,s^{\prime}\rangle$ if it is

• •

the head of a static law (6) from $D$ such that $s^{\prime}$ satisfies $l_{1}\wedge\cdots\wedge l_{m}$, or

• •

the head of a dynamic law (7) from $D$ such that $s^{\prime}$ satisfies

[TABLE]

and $s\cup a$ satisfies

[TABLE]

A transition $\langle s,a,s^{\prime}\rangle$ is causally explained by $D$ if its resulting state $s^{\prime}$ is the set of literals caused in this transition.

The transition system described by an action description $D$ is the directed graph, which has the states of $D$ as nodes, and which includes an edge from state $s$ to state $s^{\prime}$ labeled $a$ for every transition $\langle s,a,s^{\prime}\rangle$ that is causally explained by $D$.

We now present an example by \citeNlif99b that formalizes the effects of putting an object in water. We use this domain as a running example. It uses the fluent names $inWater$ and $wet$ and the elementary action name $putInnWater$. We follow the convention by \citeNlif99b and present states (interpretations) as lists of literals. In the notation introduced by \citeN[Section 6]gel98, the action description for water domain follows222We remark on the keyword inertial. It intuitively suggests that a fluent declared to be inertial is such that its value can be changed by actions only. If no actions, which directly or indirectly affect such a fluent, occur then the value of the inertial fluent remains unchanged.

[TABLE]

Written in full this action description contains six laws:

[TABLE]

The corresponding transition system has 3 states:

[TABLE]

and 6 causally explained transitions

[TABLE]

We depict this transition system in Figure 1.

2.4 On Relation between the Original and Modern Formalizations of $\mathcal{C}$

We start this section by reviewing the original formalization of action language $\mathcal{C}$ in the language of logic programs under answer set semantics [Lifschitz and Turner (1999)]. Specifically, \citeNlif99b proposed a translation from an action description $D$ in $\mathcal{C}$ to a logic program $lp_{T}(D)$ so that the answer sets of this program capture all the ”histories” of length $T$ in the transition system specified by $D$.

Since that original work, languages of answer set programming have incorporated new features such as, for instance, choice rules. At present, these are commonly used by the practitioners of ASP. It is easy to imagine that in a modern formalization of action language $\mathcal{C}$, given a system description $D$ a resulting program will be different from the original $lp_{T}(D)$. In fact, \citeNbab13 present a translation of an action language \mathcal{C}$$+ (according to \citeN[Section 7.3]giu04 $\mathcal{C}$ is the immediate predecessor of \hbox{\mathcal{C}}+) that utilizes modern language features such as choice rules. In Section 2.4.2, we present this translation for the case of $\mathcal{C}$. In particular, we restrict the language of \hbox{\mathcal{C}}+ to Boolean, or two-valued, fluents (in general, \hbox{\mathcal{C}}+ permits multivalued fluents). We call this translation $simp_{T}(D)$. Although, $lp_{T}(D)$ and $simp_{T}(D)$ share a lot in common they are substantially different. To begin with, the signatures of these programs are not identical. Also, $simp_{T}(D)$ utilizes choice rules. The programs $lp_{T}(D)$ and $simp_{T}(D)$ are different enough that it is not immediately obvious that their answer sets capture the same entities. There are two ways to argue that the program $simp_{T}(D)$ is “essentially the same” as program $lp_{T}(D)$: to illustrate that the answer sets of $simp_{T}(D)$ capture all the ”histories” of length $T$ in the transition system specified by $D$ by relying

on the definitions of action language $\mathcal{C}$; 2. 2.

on the properties of programs $lp_{T}(D)$ and $simp_{T}(D)$ that establish a one-to-one correspondence between their answer sets.

Here we take the second way into consideration. We illustrate how the concepts of strong equivalence and conservative extension together with formal results previously discovered about these prove to be of essence in this argument. The details of this argument are given in the Appendix. Thus, we showcase a proof technique for arguing on the correctness of a logic program. This proof technique assumes the existence of a ”gold standard” logic program formalizing a problem at hand, in a sense that this gold standard is trusted to produce correct results. It is a common practice in development of answer set programming solutions to obtain a final formalization of a problem by first producing such a gold standard program and then applying a number of rewriting procedures to that program to enhance its performance. The benefits of the proposed method are twofold. First, this methodology can be used by software engineers during a formal analysis of their solutions. Second, we trust that this methodology paves a way for a general framework for arguing correctness of common program rewritings so that they can be automated for the gain of performance. This is a question for investigation in the future.

2.4.1 Review of Basic Translation

Let $D$ be an action description. \citeNlif99b defined a translation from action description $D$ to a logic program $lp_{T}(D)$ parametrized with a positive integer $T$ that intuitively represents a time horizon. The remarkable property of logic program $lp_{T}(D)$ that its answer sets correspond to ”histories” – path/trajectories of length $T$ in the transition system described by $D$.

Recall that by $\sigma^{fl}$ we denote fluent names of $D$ and by $\sigma^{act}$ we denote elementary action names of $D$. Let us construct ”complementary” vocabularies to $\sigma^{fl}$ and $\sigma^{act}$ as follows

[TABLE]

and

[TABLE]

For a literal $l$, we define

[TABLE]

and

[TABLE]

The language of $lp_{T}(D)$ has atoms of four kinds:

fluent atoms–the fluent names of $\sigma^{fl}$ followed by $(t)$ where $t=0,\dots,T$, 2. 2.

action atoms–the action names of $\sigma^{act}$ followed by $(t)$ where $t=0,\dots,T-1$, 3. 3.

complement fluent atoms–the elements of $\hbox{-}{\sigma^{fl}}$ followed by $(t)$ where $t=0,\dots,T$, 4. 4.

complement action atoms–the elements of $\hbox{-}{\sigma^{act}}$ followed by $(t)$ where $t=0,\dots,T-1$.

Program $lp_{T}(D)$ consists of the following rules:

for every atom $a$ that is a fluent or action atom of the language of $lp_{T}(D)$

[TABLE]

and

[TABLE] 2. 2.

for every static law (6) in $D$, the rules

[TABLE]

for all $t=0,\dots,T$ (we understand \hbox{\widehat{l_{0}}}(t) as $\bot$ if $l_{0}$ is $\bot$), 3. 3.

for every dynamic law (7) in $D$, the rules

[TABLE]

for all $t=0,\dots,T-1$, 4. 4.

the rules

[TABLE]

for all fluent names $a$ in $\sigma^{fl}$ and 5. 5.

for every atom $a$ that is an action atom of the language of $lp_{T}(D)$ the rules

[TABLE]

Proposition 2** (Proposition 1 in [[Lifschitz and

Turner (1999)](#bib.bib33)])**

For a set $X$ of atoms, $X$ is an answer set for $lp_{T}(D)$ if and only if it has the form

[TABLE]

for some path $\langle s_{0},a_{0},s_{1},\dots,s_{T-1},a_{T-1},s_{T}\rangle$ in the transition system described by $D$.

We note that \citeNlif99b presented $lp_{T}$ translation and Proposition 1 using both default negation $not$ and classical negation $\neg$ in the program. Yet, classical negation can always be eliminated from a program by means of auxiliary atoms and additional constraints as it is done here. In particular, auxiliary atoms have the form \hbox{\hbox{-}{a}}(i) (where \hbox{\hbox{-}{a}}(i) intuitively stands for literal $\neg a(i)$), while the additional constraints have the form (9).

To exemplify this translation, consider $\mathcal{C}$ action description (8). Its translation consists of all rules of the form

[TABLE]

[TABLE]

2.4.2 Simplified Modern Translation

As in the previous section, let $D$ be an action description and $T$ a positive integer. In this section we define a translation from action description $D$ to a logic program $simp_{T}(D)$ inspired by $lp_{T}(D)$ and the advances in answer set programming languages. The main property of logic program $simp_{T}(D)$ is as in case of $lp_{T}(D)$ that its answer sets correspond to histories captured by the transition system described by $D$. This translation is a special case of a translation by \citeNbab13 for an action language \mathcal{C}$$+ that is limited to two-valued fluents.

The language of $simp_{T}(D)$ has atoms of three kinds that coincide with the three first groups (1-3) of atoms identified in the language of $lp_{T}(D)$.

For a literal $l$, we define

[TABLE]

Program $simp_{T}(D)$ consists of the following rules:

for every fluent atom $a$ the rules of the form (9) and (10), 2. 2.

for every static law (6) in $D$, $simp_{T}(D)$ contains the rules of the form

[TABLE]

for all $t=0,\dots,T$333\citeNbab13 allow rules with arbitrary formulas in their bodies so that in place of (14) they consider rule \hbox{\widehat{l_{0}}}(t)\leftarrow\ not\ not\ (\hbox{\widehat{l_{1}}}(t)\wedge\dots\wedge\hbox{\widehat{l_{m}}}(t)). Yet, it is well known that such a rule is strongly equivalent to (14). Furthermore, more answer set solvers allow rules of the form (14) than more general rules considered in [Babb and Lee (2013)]., 3. 3.

for every dynamic law (7) in $D$, the rules

[TABLE]

for all $t=0,\dots,T-1$, 4. 4.

the rules

[TABLE]

for all fluent names $a$ in $\sigma^{fl}$ and 5. 5.

for every atom $a$ that is an action atom of the language of $lp_{T}(D)$, the choice rules $\{a\}.$ Here we note that the language $\mathcal{C}$ assumes every action to be exogenous, whereas this is not the case in \hbox{\mathcal{C}}+, where it has to be explicitly stated whether an action has this property. Thus, in [Babb and Lee (2013)] rules of this group only appear for the case of actions that have been stated exogenous.

The $simp_{T}$ translation of $\mathcal{C}$ action description (8) consists of all rules of the form

[TABLE]

2.4.3 On the Relation Between Programs $lp_{T}$ and $simp_{T}$

Proposition 3 stated in this section is the key result of this part of the paper. Its proof outlines the essential steps that we take in arguing that two logic programs $lp_{T}$ and $simp_{T}$ formalizing the action language $\mathcal{C}$ are essentially the same. The key claim of the proof is that logic program $lp_{T}(D)$ is a conservative extension of $simp_{T}(D)$. Here we only outline the proof whereas the Appendix of the paper provides a complete proof.

The argument of this claim requires some close attention to groups of rules in the $lp_{T}(D)$ program. In particular, we establish by means of weak natural deduction that

• •

the rules in group 1 and 2 of $lp_{T}(D)$ are strongly equivalent to the rules in group 1 and 2 of $simp_{T}(D)$ and

• •

the rules in group 1 and 4 of $lp_{T}(D)$ are strongly equivalent to the rules in group 1 and 4 of $simp_{T}(D)$.

Similarly, we show that

• •

the rules in group 1 and 3 of $lp_{T}(D)$ are strongly equivalent to the rules in group 1 of $simp_{T}(D)$ and the rules structurally similar to rules in group 3 of $simp_{T}(D)$ and yet not the same.

These arguments allow us to construct a program $lp^{\prime}_{T}(D)$, whose answer sets are the same as those of $lp_{T}(D)$. Program $lp^{\prime}_{T}(D)$ is a conservative extension of $simp_{T}(D)$ due to explicit definition rewriting. Proposition 1 helps us to uncover this fact.

Recall that the language of $simp_{T}(D)$ includes the action atoms — the action names of $\sigma^{act}$ followed by $(t)$ where $t=0,\dots T-1$. We denote the action atoms by $\sigma_{T}^{act}$.

Proposition 3

For a set $X$ of atoms, $X$ is an answer set for $simp_{T}(D)$ if and only if the set X\cup\{\hbox{\hbox{-}{a}}\mid a\in\sigma_{T}^{act}\setminus X\} has the form

[TABLE]

for some path $\langle s_{0},a_{0},s_{1},\dots,s_{T-1},a_{T-1},s_{T}\rangle$ in the transition system described by $D$.

2.4.4 Additional Concluding Remarks: An Interesting Byproduct

Our work, which illustrates that logic programs $lp_{T}(D)$ and $simp_{T}(D)$ are essentially the same, also uncovers a precise formal link between the action description languages $\mathcal{C}$ and \hbox{\mathcal{C}}+. The authors of \hbox{\mathcal{C}}+ claimed that $\mathcal{C}$ is an immediate predecessor of \hbox{\mathcal{C}}+. Yet, to the best of our knowledge the exact formal link between the two languages has not been stated. Thus, earlier one could view \hbox{\mathcal{C}}+ as a generalization of $\mathcal{C}$ only informally alluding to the fact that \hbox{\mathcal{C}}+ allows the same intuitive interpretation of syntactic expressions of $\mathcal{C}$, while generalizing these to allow multivalued fluents in place of Boolean ones. These languages share the same syntactic constructs such as, for example, a dynamic law of the form

[TABLE]

that we intuitively read as after the concurrent execution of actions $a_{1}\dots a_{n}$ the fluent expression $f_{0}$ holds in case if fluents expressions $f_{1}\dots f_{m}$ were the case at the time when aforementioned actions took place. Both languages provide interpretations for such expressions that meet our intuitions of this informal reading. Yet, if one studies the semantics of these languages it is not trivial to establish a specific formal link between them. For example, the semantics of \hbox{\mathcal{C}}+ relies on the concepts of causal theories [Giunchiglia et al. (2004)]. The semantics of $\mathcal{C}$ makes no reference to these theories. Here we recall the translations of $\mathcal{C}$ and \hbox{\mathcal{C}}+ to logic programs, whose answer sets correspond to their key semantic objects. We then state the precise relation between the two by means of relating the relevant translations. In conclusion, \hbox{\mathcal{C}}+ can be viewed as a true generalization of the language $\mathcal{C}$ to the case of multi-valued fluents.

3 Programs with Variables

We now proceed towards the second part of the paper devoted to programs with variables. We start by presenting its detailed outline, a new running example and then stating the preliminaries. We conclude with the formal statements on a number of rewriting techniques.

On the one hand, this part of the paper can be seen as a continuation of work by \citeNeit06, where we consider common program rewritings using a more complex dialect of logic programs. On the other hand, this part of the paper grounds the concept of program synonymity studied by \citeNpea12 in a number of practical examples. Namely, we illustrate how formal results on strong equivalence developed earlier and in this work help us to construct precise claims about programs in practice.

In this part of the paper, we systematically study some common rewritings on first-order programs utilized by ASP practitioners. We use a running example to ground general theoretical presentation of this work into specific context. In particular, we consider two formalizations of a planning module given in [Gelfond and Kahl (2014), Section 9]:

a Plan-choice formalization that utilizes choice rules and aggregate expressions, 2. 2.

a Plan-disj formalization that utilizes disjunctive rules.

Such a planning module is meant to be augmented with an ASP representation of a dynamic system description expressed in action language $\mathcal{AL}$ 444It is due to remark that although \citeNgel14 use the word “module” when encoding a planning domain, they utilize this term only informally to refer to a collection of rules responsible for formalizing “planning”. . \citeNgel14 formally state in Proposition 9.1.1 that the answer sets of program Plan-disj augmented with a given system description encode all the “histories/plans” of a specified length in the transition system captured by the system description. We note that no formal claim is provided for the Plan-choice program. Although both Plan-choice and Plan-disj programs intuitively encode the same knowledge the exact connection between them is not immediate. In fact, these programs

• •

do not share the same signature, and

• •

use distinct syntactic constructs such as choice, disjunction, aggregates in the specification of a problem.

Here, we establish a one-to-one correspondence between the answer sets of these programs using their properties. Thus, the aforementioned formal claim about Plan-disj translates into the same claim for Plan-choice.

Here we use a dialect of the ASP language called RASPL-1 [Lee et al. (2008)]. Notably, this language combines choice, aggregate, and disjunction constructs. Its semantics is given in terms of the SM operator, which exemplifies the approach to the semantics of first-order programs that bypasses grounding. Relying on SM-based semantics allows us to refer to earlier work that study the formal properties of first-order programs [Ferraris et al. (2011), Ferraris et al. (2009)] using this operator. We state a sequence of formal results on programs rewritings and/or programs properties. Some of these results are geared by our running example and may not appear of great general interest. Yet, we view the proofs of these results as an interesting contribution as they showcase how arguments of correctness of rewritings can be constructed by the practitioners. Also, some discussed rewritings are well known and frequently used in practice. Often, their correctness is an immediate consequence of well known properties about logic programs (e.g., relation between intuitionistically provable first-order formulas and strongly equivalent programs viewed as such formulas). Other discussed rewritings are far less straightforward and require elaborations on previous theoretical findings about the operator SM. It is well known that propositional head-cycle-free disjunctive programs [Ben-Eliyahu and Dechter (1994)] can be rewritten to nondisjunctive programs by means of a simple syntactic transformation. Here we not only generalize this result to the case of first-order programs, but also illustrate that at times we can remove disjunction from parts of a program even though the program is not head-cycle-free. This result is relevant to local shifting and component-wise shifting discussed in [Eiter et al. (2006)] and [Janhunen et al. (2007)], respectively. We also generalize so called Completion Lemma and Lemma on Explicit Definitions stated in [Ferraris (2005), Ferraris and Lifschitz (2005)] for the case of propositional theories and propositional logic programs. These generalizations are applicable to first-order programs. We conclude by applying the Lemma on Explicit Definitions proved here to argue the correctness of program rewriting system projector [Hippen and Lierler (2019)].

3.1 Running Example and Claims

This section presents two ASP formalizations of a domain independent planning module given in [Gelfond and Kahl (2014), Section 9]. Such planning module is meant to be augmented with a logic program encoding a system description expressed in action language $\mathcal{AL}$ that represents a domain of interest (in Section 8 of their book [Gelfond and Kahl (2014)], Gelfond and Kahl present a sample Blocks World domain representation). Two formalizations of a planning module are stated here almost verbatim. Predicate names $o$ and $\mathit{sthHpd}$ intuitively stand for occurs and something_happend, respectively. We eliminate classical negation symbol by

• •

utilizing auxiliary predicates non_o in place of $\neg o$; and

• •

introducing rule $\leftarrow o(A,I),non\_o(A,I).$

This is a standard practice and ASP systems perform the same rewriting when processing classical negation symbol $\neg$ occurring in programs (in other words, symbol $\neg$ is treated as syntactic sugar).

Let

[TABLE]

where $n$ is some integer specifying a limit on a length of an allowed plan. The first formalization called Plan-choice follows:

[TABLE]

One more remark is in order. In [Gelfond and Kahl (2014)], Gelfond and Kahl list only a single rule

[TABLE]

in place of rules (18-20). Note that this single rule is an abbreviation for rules (18-20) [Gebser et al. (2015)].

The second formalization that we call a Plan-disj encoding is obtained from Plan-choice by replacing rules (18-20) with the following:

[TABLE]

It is important to note several facts about the considered planning module encodings. These planning modules are meant to be used with logic programs that capture

• (i)

a domain of interest originally stated as a system description in the action language $\mathcal{AL}$;

• (ii)

a specification of an initial configuration;

• (iii)

a specification of a goal configuration.

The process of encoding (i-iii) as a logic program, which we call a Plan-instance encoding, follows a strict procedure. As a consequence, some important properties hold about any Plan-instance. To state these it is convenient to recall the notion of a simple rule and define a “terminal” predicate.

A signature is a set of function and predicate symbols/constants. A function symbol of arity 0 is an object constant. A term is an object constant, an object variable, or an expression of the form $f(t_{1},\dots,t_{m})$, where $f$ is a function symbol of arity $m$ and each $t_{i}$ is a term. An atom is an expression of the form $p(t_{1},\dots,t_{n})$ or $t_{1}=t_{2}$, where $p$ is an $n$-ary predicate symbol and each $t_{i}$ is a term. A simple body has the form

[TABLE]

where $a_{i}$ is an atom and $n\geq 0$. Expression $a_{1},\dots,a_{m}$ forms the positive part of a body. A simple rule has the form

[TABLE]

or

[TABLE]

where $h_{i}$ is an atom and $\mathit{Body}$ is a simple body. We now state a recursive definition of a terminal predicate with respect to a program. Let $i$ be a nonnegative integer. A predicate that occurs only in rules whose body is empty is called 0-terminal. We call a predicate $i+1$-terminal when it occurs only in the heads of simple rules (left hand side of an arrow), furthermore

• •

in these rules all predicates occurring in their positive parts of the bodies must be at most $i$-terminal and

• •

at least one of these rules is such that some predicate occurring in its positive part of the body is $i$-terminal .

We call any $x$-terminal predicate terminal. For example, in program

[TABLE]

$block$ is a [math]-terminal predicate, $loc$ is a $1$-terminal predicate; and both predicates are terminal.

We are now ready to state important Facts about any possible Plan-instance and, consequently, about the considered planning modules

Predicate $o$ never occurs in the heads of rules in Plan-instance. 2. 2.

Predicates $action$ and $step$ are terminal in Plan-instance as well as in Plan-instance augmented by either Plan-choice or Plan-disj. 3. 3.

By Facts 1 and 2, predicate $o$ is terminal in Plan-instance augmented by either Plan-choice or Plan-disj. 4. 4.

Predicate $\mathit{sthHpd}$ never occurs in the heads of the rules in Plan-instance.

In the remainder of the paper we use considered theoretical results to illustrate the following Claim**s:

In the presence of rule (17) it is safe to add a rule

[TABLE]

into an arbitrary program. By “safe to add/replace” we understand that the resulting program has the same answer sets as the original one. 2. 2.

It is safe to replace rule (19) with rule

[TABLE]

within an arbitrary program. 3. 3.

In the presence of rules (16) and (17), it is safe to replace rule (18) with rule

[TABLE]

within an arbitrary program. 4. 4.

Given the syntactic features of the Plan-choice encoding and any Plan-instance encoding, it is safe to replace rule (18) with rule (21). The argument utilizes Claim**s 1 and 3. Fact 4 forms an essential syntactic feature. 5. 5.

Given the syntactic features of the Plan-choice encoding and any Plan-instance encoding, it is safe to replace rule (19) with rule (22). The argument utilizes Claim 2, i.e., it is safe to replace rule (19) with rule (26). An essential syntactic feature relies on Fact 1, and the facts that (i) rule (18) is the only one in Plan-choice, where predicate $o$ occurs in the head; and (ii) rule (22) differs from (26) only in atoms that are part of the body of (18). 6. 6.

By Fact 4 and the fact that $\mathit{sthHpd}$ does not occur in any other rule but (24) in Plan-disj, the answer sets of the program obtained by replacing rule (20) with rules (23) and (24) are in one-to-one correspondence with the answer sets of the program Plan-disj extended with Plan-instance.

Essential Equivalence Between Two Planning Modules: These Claim**s are sufficient to state that the answer sets of the Plan-choice and Plan-disj programs (extended with any Plan-instance) are in one-to-one correspondence. We can capture the simple relation between the answer sets of these programs by observing that dropping the atoms whose predicate symbol is $\mathit{sthHpd}$ from an answer set of the Plan-disj program results in an answer set of the Plan-choice program.

3.2 Preliminaries: RASPL-1 Logic Programs, Operator SM, Strong Equivalence

We now review a logic programming language RASPL-1 [Lee et al. (2008)]. This language is sufficient to capture choice, aggregate, and disjunction constructs (as used in Plan-choice and Plan-disj). There are distinct and not entirely compatible semantics for aggregate expressions in the literature. We refer the interested reader to the discussion by \citeNlee08 on the roots of semantics of aggregates considered in RASPL-1.

An aggregate expression is an expression of the form

[TABLE]

($k\geq 1$), where $b$ is a positive integer (bound), $\mathbf{x}$ is a list of variables (possibly empty), and each $L_{i}$ is an atom possibly preceded by not. We call variables in x aggregate variables. This expression states that there are at least $b$ values of $\mathbf{x}$ such that conditions $L_{1},\dots,L_{k}$ hold.

A body is an expression of the form

[TABLE]

($n\geq m\geq 0$) where each $e_{i}$ is an aggregate expression or an atom. A rule is an expression of either of the forms

[TABLE]

($l\geq 0$) where each $a_{i}$ is an atom, and $\mathit{Body}$ is the body in the form (29). When $l=0$, we identify the head of (30) with symbol $\bot$ and call such a rule a denial. When $l=1$, we call rule (30) a defining rule. We call rule (31) a choice rule. A (logic) program is a set of rules. An atom of the form $not\ t_{1}=t_{2}$ is abbreviated by $t_{1}\neq t_{2}$.

3.2.1 Operator SM

Typically, the semantics of logic programs with variables is given by stating that these rules are an abbreviation for a possibly infinite set of propositional rules. Then the semantics of propositional programs is considered. The SM operator introduced by \citeNfer09 gives a definition for the semantics of first-order programs bypassing grounding. It is an operator that takes a first-order sentence $F$ and a tuple ${\bf p}$ of predicate symbols and produces the second order sentence that we denote by $\hbox{SM}_{\bf p}[F]$.

We now review the operator SM. The symbols $\bot,\land,\lor,\rightarrow$, $\forall,$ and $\exists$ are viewed as primitives. The formulas $\neg F$ and $\top$ are abbreviations for $F\rightarrow\bot$ and $\bot\rightarrow\bot$, respectively. If $p$ and $q$ are predicate symbols of arity $n$ then $p\leq q$ is an abbreviation for the formula $\forall{\bf x}(p({\bf x})\rightarrow q({\bf x})),$ where ${\bf x}$ is a tuple of variables of length $n$. If ${\bf p}$ and ${\bf q}$ are tuples $p_{1},\dots,p_{n}$ and $q_{1},\dots,q_{n}$ of predicate symbols then ${\bf p}\leq{\bf q}$ is an abbreviation for the conjunction $(p_{1}\leq q_{1})\land\dots\land(p_{n}\leq q_{n}),$ and ${\bf p}<{\bf q}$ is an abbreviation for $({\bf p}\leq{\bf q})\land\neg({\bf q}\leq{\bf p}).$ We apply the same notation to tuples of predicate variables in second-order logic formulas. If ${\bf p}$ is a tuple of predicate symbols $p_{1},\dots,p_{n}$ (not including equality), and $F$ is a first-order sentence then SM${}_{\bf p}[F]$ denotes the second-order sentence

[TABLE]

where ${\bf u}$ is a tuple of distinct predicate variables $u_{1},\dots,u_{n}$, and $F^{*}({\bf u})$ is defined recursively:

• •

$p_{i}({\bf t})^{*}$ is $u_{i}({\bf t})$ for any tuple ${\bf t}$ of terms;

• •

$F^{*}$ is $F$ for any atomic formula $F$ that does not contain members of p;555This includes equality statements and the formula $\bot$.

• •

$(F\land G)^{*}$ is $F^{*}\land G^{*}$;

• •

$(F\lor G)^{*}$ is $F^{*}\lor G^{*}$;

• •

$(F\rightarrow G)^{*}$ is $(F^{*}\rightarrow G^{*})\land(F\rightarrow G)$;

• •

$(\forall xF)^{*}$ is $\forall xF^{*}$;

• •

$(\exists xF)^{*}$ is $\exists xF^{*}$.

Note that if ${\bf p}$ is the empty tuple then SM${}_{\bf p}[F]$ is equivalent to $F$. For intuitions regarding the definition of the SM operator we direct the reader to [Ferraris et al. (2011), Sections 2.3, 2.4].

By $\sigma(F)$ we denote the set of all function and predicate constants occurring in first-order formula $F$ (not including equality). We will call this the signature of $F$. An interpretation $I$ over $\sigma(F)$ is a ${\bf p}$-stable model of $F$ if it satisfies SM${}_{\bf p}[F]$, where p is a tuple of predicates from $\sigma(F)$. We note that a ${\bf p}$-stable model of $F$ is also a model of $F$.

By $\pi(F)$ we denote the set of all predicate constants (excluding equality) occurring in a formula $F$. Let $F$ be a first-order sentence that contains at least one object constant. We call an Herbrand interpretation of $\sigma(F)$ that is a $\pi(F)$-stable model of $F$ an answer set.666 An Herbrand interpretation of a signature $\sigma$ (containing at least one object constant) is such that its universe is the set of all ground terms of $\sigma$, and every ground term represents itself. An Herbrand interpretation can be identified with the set of ground atoms (not containing equality) to which it assigns the value true. Theorem 1 from [Ferraris et al. (2011)] illustrates in which sense this definition can be seen as a generalization of a classical definition of an answer set (via grounding and reduct) for typical logic programs whose syntax is more restricted than syntax of programs considered here.

3.2.2 Semantics of Logic Programs

From this point on, we view logic program rules as alternative notation for particular types of first-order sentences. We now define a procedure that turns every aggregate, every rule, and every program into a formula of first-order logic, called its FOL representation. First, we identify the logical connectives $\wedge$, $\vee$, and $\neg$ with their counterparts used in logic programs, namely, the comma, the disjunction symbol $\mid$, and connective $not$. This allows us to treat $L_{1},\dots,L_{k}$ in (28) as a conjunction of literals.

For an aggregate expressions of the form

[TABLE]

its FOL representation follows

[TABLE]

where $\mathbf{x^{1}}\cdots\mathbf{x^{b}}$ are lists of new variables of the same length as $\mathbf{x}$.

The FOL representations of logic rules of the form (30) and (31) are formulas

[TABLE]

where each aggregate expression in $\mathit{Body}$ is replaced by its FOL representation. Symbol $\widetilde{\forall}$ denotes universal closure.

For example, expression $SG(I)$ stands for formula $step(I)\wedge\neg goal(I)\wedge\neg I=n$ and rules (18) and (20) in the Plan-choice encoding have the FOL representation:

[TABLE]

The FOL representation of rule (19) is the universal closure of the following implication

[TABLE]

We define a concept of an answer set for logic programs that contain at least one object constant. This is inessential restriction as typical logic programs without object constants are in a sense trivial. In such programs, whose semantics is given via grounding, rules with variables are eliminated during grounding. Let $\Pi$ be a logic program with at least one object constant. (In the sequel we often omit expression “with at least one object constant”.) By $\widehat{\Pi}$ we denote its FOL representation. (Similarly, for a head $H$, a body $\mathit{Body}$, or a rule $R$, by $\widehat{H}$, $\widehat{\mathit{Body}}$, or $\widehat{R}$ we denote their FOL representations.) An answer set of $\Pi$ is an answer set of its FOL representation $\widehat{\Pi}$. In other words, an answer set of $\Pi$ is an Herbrand interpretation of $\widehat{\Pi}$ that is a \pi(\hbox{\widehat{\Pi}})-stable model of $\widehat{\Pi}$, i.e., a model of

[TABLE]

Sometimes, it is convenient to identify a logic program $\Pi$ with its semantic counterpart (35) so that formal results stated in terms of SM operator immediately translate into the results for logic programs.

3.2.3 Review: Strong Equivalence

We restate the definition of strong equivalence for first-order formulas given in [Ferraris et al. (2011)] and recall some of its properties. First-order formulas $F$ and $G$ are strongly equivalent if for any formula $H$, any occurrence of $F$ in $H$, and any tuple $\bf p$ of distinct predicate constants, SM${}_{\bf p}[H]$ is equivalent to SM${}_{\bf p}[H^{\prime}]$, where $H^{\prime}$ is obtained from $H$ by replacing $F$ by $G$. Trivially, any strongly equivalent formulas are such that their stable models coincide (relative to any tuple of predicate constants). \citeNlif07a show that first-order formulas $F$ and $G$ are strongly equivalent if they are equivalent in SQHT= logic — an intermediate logic between classical and intuitionistic logics. Every formula provable using natural deduction, where the axiom of the law of the excluded middle ($F\vee\neg F$) is replaced by the weak law of the excluded middle ($\neg F\vee\neg\neg F$), is a theorem of SQHT=.

The definition of strong equivalence between first-order formulas paves the way to a definition of strong equivalence for logic programs. A logic program $\Pi_{1}$ is strongly equivalent to logic program $\Pi_{2}$ when for any program $\Pi$,

[TABLE]

It immediately follows that logic programs $\Pi_{1}$ and $\Pi_{2}$ are strongly equivalent if first-order formulas $\widehat{\Pi_{1}}$ and $\widehat{\Pi_{2}}$ are equivalent in logic of SQHT=.

We now review an important result about properties of denials.

Theorem 1** (Theorem 3 [[Ferraris

et al. (2011)](#bib.bib12)])**

For any first-order formulas $F$ and $G$ and arbitrary tuple ${\bf p}$ of predicate constants, $\hbox{SM}_{\bf p}[F\wedge\neg G]$ is equivalent to $\hbox{SM}_{\bf p}[F]\wedge\neg G.$

As a consequence, p-stable models of $F\wedge\neg G$ can be characterized as the p-stable models of $F$ that satisfy first-order logic formula $\neg G$. Consider any denial $\leftarrow\mathit{Body}.$ Its FOL representation has the form $\widetilde{\forall}(\mathit{Body}\rightarrow\bot)$ that is intuitionistically equivalent to formula $\neg\widetilde{\exists}\mathit{Body}$. Thus, Theorem 1 tells us that given any denial of a program it is safe to compute answer sets of a program without this denial and a posteriori verify that the FOL representation of a denial is satisfied.

Corollary 1

Two denials are strongly equivalent if their FOL representations are classically equivalent.

This corollary is also an immediate consequence of the Replacement Theorem for intuitionistic logic for first-order formulas [Mints (2000)] stated below.

Proposition 4** (Replacement Theorem II [Mints (2000)], Section 13.1)**

If $F$ is a first-order formula containing a subformula $G$ and $F^{\prime}$ is the result of replacing that subformula by $G^{\prime}$ then $\widetilde{\forall}(G\leftrightarrow G^{\prime})$ intuitionistically implies $F\leftrightarrow F^{\prime}$.

3.3 Rewritings

3.3.1 Rewritings via Pure Strong Equivalence

Strong equivalence can be used to argue the correctness of some program rewritings practiced by ASP software engineers. Here we state several theorems about strong equivalence between programs. Claim**s 1, 2, and 3 are consequences of these results.

We say that body $\mathit{Body}$ subsumes body $\mathit{Body}^{\prime}$ when $\mathit{Body}^{\prime}$ has the form $\mathit{Body},\mathit{Body}^{\prime\prime}$ (note that an order of expressions in a body is immaterial) . We say that a rule $R$ subsumes rule $R^{\prime}$ when heads of $R$ and $R^{\prime}$ coincide while body of $R$ subsumes body of $R^{\prime}$. For example, rule (17) subsumes rule (25).

Subsumption Rewriting: Let ${\bf R^{\prime}}$ denote a set of rules subsumed by rule $R$. It is easy to see that formulas $\widehat{R}$ and \hbox{\widehat{R}}\wedge\hbox{\widehat{\bf R^{\prime}}} are intuitionistically equivalent. Thus, program composed of rule $R$ and program $\{R\}\cup{\bf R^{\prime}}$ are strongly equivalent. It immediately follows that Claim 1 holds. Indeed, rule (17) is strongly equivalent to the set of rules composed of itself and (25). Indeed, rule (17) subsumes rule (25).

Removing Aggregates: The following theorem is an immediate consequence of the Replacement Theorem II.

Theorem 2

Program

[TABLE]

is strongly equivalent to program

[TABLE]

where $G$ and $H$ have no occurrences of variables in $\mathbf{x^{i}}$ $(1\leq i\leq b)$.

Theorem 2 shows us that Claim 2 is a special case of a more general fact. Indeed, take rules (19) and (26) to be the instances of rules (36) and (37) respectively.

We note that the Replacement Theorem II also allows us to immediately conclude the following.

Corollary 2

Program   $H\leftarrow G$   is strongly equivalent to program   $H\leftarrow G^{\prime}$   when   \widetilde{\forall}(\hbox{\widehat{G}}\leftrightarrow\hbox{\widehat{G^{\prime}}}).

Corollary 2 equips us with a general semantic condition that can be utilized in proving the syntactic properties of programs in spirit of Theorem 2.

Replacing Choice Rule by Defining Rule: Theorem 3 shows us that Claim 3 is an instance of a more general fact.

Theorem 3

Program

[TABLE]

is strongly equivalent to program composed of rules (38), (39) and rule

[TABLE]

where $F_{1}$ and $F_{2}$ are the expressions of the form (29).

To illustrate the correctness of Claim 3 by Theorem 3: (i) take rules (16), (17), (18) be the instances of rules (38), (39), (40) respectively, and (ii) rule (27) be the instance of rule (41).

3.3.2 Useful Rewritings using Structure

In this subsection, we study rewritings on a program that rely on its structure. We review the concept of a dependency graph used in posing structural conditions on rewritings.

Review: Predicate Dependency Graph

We present the concept of the predicate dependency graph of a formula following the lines of [Ferraris et al. (2009)]. An occurrence of a predicate constant, or any other subexpression, in a formula is called positive if the number of implications containing that occurrence in the antecedent is even, and strictly positive if that number is 0. We say that an occurrence of a predicate constant is negated if it belongs to a subformula of the form $\neg F$ (an abbreviation for $F\rightarrow\bot$), and nonnegated otherwise.

For instance, in formula (33), predicate constant $o$ has a strictly positive occurrence in the consequence of the implication; whereas the same symbol $o$ has a negated positive occurrence in the antecedent

[TABLE]

of (33). Predicate symbol $action$ has a strictly positive non-negated occurrence in (42). The occurrence of predicate symbol $goal$ is negated and not positive in (42). The occurrence of predicate symbol $goal$ is negated and positive in (33).

An FOL rule of a first-order formula $F$ is a strictly positive occurrence of an implication in $F$. For instance, in a conjunction of two formulas (33) and (34) the FOL rules are as follows

[TABLE]

For any first-order formula $F$, the (predicate) dependency graph of $F$ relative to the tuple p of predicate symbols (excluding $=$) is the directed graph that (i) has all predicates in p as its vertices, and (ii) has an edge from $p$ to $q$ if for some FOL rule $G\rightarrow H$ of $F$

• •

$p$ has a strictly positive occurrence in $H$, and

• •

$q$ has a positive nonnegated occurrence in $G$.

We denote such a graph by $DG_{\bf p}[F]$. For instance, Figure 2 presents the dependence graph of a conjunction of formulas (33) and (34) relative to all its predicate symbols. It contains four vertices, namely, $o$, $action$, $step$, and $goal$, and two edges: one from vertex $o$ to vertex $action$ and the other one from $o$ to $step$. Indeed, consider the only two FOL rules (43) and (44) stemming from this conjunction. Predicate constant $o$ has a strictly positive occurrence in the consequent $o(A,I)$ of the implication (43), whereas $action$ and $step$ are the only predicate constants in the antecedent $\neg\neg o(A,I)\wedge SG(I)\wedge action(A)$ of (43) that have positive and nonnegated occurrence in this antecedent. It is easy to see that a FOL rule of the form $G\rightarrow\bot$, e.g., FOL rule (44), does not contribute edges to any dependency graph.

For any logic program $\Pi$, the dependency graph of $\Pi$, denoted $DG[\Pi]$, is a directed graph of $\widehat{\Pi}$ relative to the predicates occurring in $\Pi$. For example, let $\Pi$ be composed of two rules (18) and (20). The conjunction of formulas (33) and (34) forms its FOL representation. Thus, Figure 2 captures its dependency graph $DG[\Pi]$.

Shifting

We call a logic program disjunctive if all its rules have the form (30), where $\mathit{Body}$ only contains atoms possibly preceded by $not$. We say that a disjunctive program is normal when it does not contain disjunction connective $\mid$. \citeNgel91a defined a mapping from a propositional disjunctive program $\Pi$ to a propositional normal program by replacing each rule (30) with $l>1$ in $\Pi$ by $l$ new rules

[TABLE]

They showed that every answer set of the constructed program is also an answer set of $\Pi$. Although the converse does not hold in general, \citeNben94 showed that the converse holds if $\Pi$ is “head-cycle-free”. \citeNlin04a illustrated how this property holds about programs with nested expressions that capture choice rules, for instance. Here we generalize these findings further. First, we show that shifting is applicable to first-order programs (which also may contain choice rules and aggregates in addition to disjunction). Second, we illustrate that under certain syntactic/structural conditions on a program we may apply shifting “locally” to some rules with disjunction and not others.

For an atom $a$, by $a^{0}$ we denote its predicate constant. For example $o(A,I)^{0}=o$. Let $R$ be a rule of the form (30) with $l>1$. By \hbox{\mathit{shift}}_{\bf p}(R) (where ${\mathbf{p}}$ is a tuple of distinct predicates) we denote the rule

[TABLE]

Let ${\mathcal{P}^{R}}$ be a partition of the set composed of the distinct predicate symbols occurring in the head of rule $R$. By \hbox{\mathit{shift}}_{\mathcal{P}^{R}}(R) we denote the set of rules composed of rule \hbox{\mathit{shift}}_{\bf p}(R) for every member p of the partition $\mathcal{P}^{R}$ (order of the elements in p is immaterial).

For instance, if $R_{1}$ denotes a rule

[TABLE]

then ${\mathcal{P}_{1}}^{R_{1}}=\{\{a,b\},\{c,d,e\}\}$ and ${\mathcal{P}_{2}}^{R_{1}}=\{\{a,b\},\{c\},\{d,e\}\}$ form sample partitions of the described kind. Set \hbox{\mathit{shift}}_{\mathcal{P}_{1}^{R_{1}}}(R_{1}) consists of rules

[TABLE]

whereas set \hbox{\mathit{shift}}_{\mathcal{P}_{2}^{R_{1}}}({R_{1}}) consists of rules

[TABLE]

Theorem 4

Let $\Pi$ be a logic program, $\bf R$ be a set of rules in $\Pi$ of the form (30) with $l>1$, and $C$ be the set of strongly connected components in the dependency graph of $\Pi$. A program constructed from $\Pi$ by replacing each rule $R\in\bf R$ with \hbox{\mathit{shift}}_{\mathcal{P}^{R}}(R) has the same answer sets as $\Pi$ if any partition $\mathcal{P}^{R}$ is such that there are no two distinct members ${\bf p}_{1}$ and ${\bf p}_{2}$ in $\mathcal{P}^{R}$ so that for some strongly connected component $c$ in $C$, $c\cap\bf p_{1}\neq\emptyset$ and $c\cap\bf p_{2}\neq\emptyset$.777The statement of this theorem was suggested by Pedro Cabalar and Jorge Fandinno in personal communication on January 17, 2019.

Consider a sample program $\Pi_{samp}$ composed of rule (46), which we denote as $R_{1}$, and rules

[TABLE]

The strongly connected components of program $\Pi_{samp}$ are $\{\{a,b\},\{c\},\{d\},\{e(1)\}\}$. Theorem 4 tells us, for instance, that the answer sets of program $\Pi_{samp}$ coincide with the answer sets of two distinct programs:

a program composed of rules \hbox{\mathit{shift}}_{\mathcal{P}_{1}^{R_{1}}}(R_{1}) and rules (47); 2. 2.

a program composed of rules \hbox{\mathit{shift}}_{\mathcal{P}_{2}^{R_{1}}}(R_{1}) and rules (47).

We now use Theorem 4 to argue the correctness of Claim 4. Let Plan-choice*′* denote a program constructed from the Plan-choice encoding by replacing (18) with (21). Let Plan-choice*′′* denote a program constructed from the Plan-choice, by (i) replacing (18) with (27) and (ii) adding rule (25). Theorem 4 tells us that programs Plan-choice*′* and Plan-choice*′′* have the same answer sets. Indeed,

take ${\bf R}$ to consist of rule (21) and 2. 2.

recall Facts 1, 2, and 3. Given any Plan-instance intended to use with Plan-choice a program obtained from the union of Plan-instance and Plan-choice*′* is such that $o$ is terminal. It is easy to see that any terminal predicate in a program occurs only in the singleton strongly connected components of a program dependency graph.

Due to Claim**s 1 and 3, the Plan-choice encoding has the same answer sets as Plan-choice*′′* and consequently the same answer sets as Plan-choice*′*. This argument accounts for the proof of Claim 4.

Completion

We now proceed at stating formal results about first-order formulas and their stable models. The fact that we identify logic programs with their FOL representations translates these results to the case of the RASPL-1 programs.

About a first-order formula $F$ we say that it is in Clark normal form [Ferraris et al. (2011)] relative to the tuple/set p of predicate symbols if it is a conjunction of formulas of the form

[TABLE]

one for each predicate $p\in{\bf p}$, where $\mathbf{x}$ is a tuple of distinct object variables. We refer the reader to Section 6.1 in [Ferraris et al. (2011)] for the description of the intuitionistically equivalent transformations that can convert a first-order formula, which is a FOL representation for a RASPL-1 program (without disjunction and denials), into Clark normal form.

The completion of a formula $F$ in Clark normal form relative to predicate symbols p, denoted by $Comp_{\bf p}[F]$, is obtained from $F$ by replacing each conjunctive term of the form (48) with

[TABLE]

We now review an important result about properties of completion.

Theorem 5** (Theorem 10 [[Ferraris

et al. (2011)](#bib.bib12)])**

For any formula $F$ in Clark normal form and arbitrary tuple ${\bf p}$ of predicate constants, formula

[TABLE]

is logically valid.

The following Corollary is an immediate consequence of this theorem, Theorem 1, and the fact that formula of the form $\widetilde{\forall}(\mathit{Body}\rightarrow\bot)$ is intuitionistically equivalent to formula $\neg\widetilde{\exists}\mathit{Body}$.

Corollary 3

For any formula $G\wedge H$ such that (i) formula $G$ is in Clark normal form relative to p and $H$ is a conjunction of formulas of the form $\widetilde{\forall}(K\rightarrow\bot)$, the implication

[TABLE]

is logically valid.

To illustrate the utility of this result we now construct an argument for the correctness of Claim 5. This argument finds one more formal result of use:

Theorem 6

For a program $\Pi$, a first-order formula $F$ such that every answer set of $\Pi$ satisfies $F$, and any two denials $R$ and $R^{\prime}$ such that F\rightarrow(\hbox{\widehat{R}}\leftrightarrow\hbox{\widehat{R^{\prime}}}), the answer sets of programs $\Pi\cup\{R\}$ and $\Pi\cup\{R^{\prime}\}$ coincide.

Theorem 1 provides grounds for a straightforward argument for this statement.

Consider the Plan-choice encoding without denial (19) extended with any Plan-instance. We can partition it into two parts: one that contains the denials, denoted by $\Pi_{H}$, and the remainder, denoted by $\Pi_{G}$. Recall Fact 1. Following the steps described by \citeN[Section 6.1]fer09, formula $\widehat{\Pi_{G}}$ turned into Clark normal form relative to the predicate symbols occurring in $\Pi_{H}\cup\Pi_{G}$ contains implication (33). The completion of this formula contains equivalence

[TABLE]

By Corollary 3 it follows that any answer set of $\Pi_{H}\cup\Pi_{G}$ satisfies formula (49). It is easy to see that an interpretation satisfies (49) and the FOL representation of (26) if and only if it satisfies (49) and the FOL representation of denial (22). Thus, by Theorem 6 program $\Pi_{H}\cup\Pi_{G}$ extended with (26) and program $\Pi_{H}\cup\Pi_{G}$ extended with (22) have the same answer sets. Recall Claim 2 claiming that it is safe to replace denial (19) with denial (26) within an arbitrary program. It follows that program $\Pi_{H}\cup\Pi_{G}$ extended with (22) have the same answer sets $\Pi_{H}\cup\Pi_{G}$ extended with (19). This concludes the argument for the claim of Claim 5.

We now state the main formal results of the second part of the paper. The Completion Lemma for first-order programs stated next is essential in proving the Lemma on Explicit Definitions for first-order programs. Claim 6 follows immediately from the latter lemma.

Theorem 7** (Completion Lemma)**

Let $F$ be a first-order formula and q be a set of predicate constants that do not have positive, nonnegated occurrences in any FOL rule of $F$. Let $\bf p$ be a set of predicates in $F$ disjoint from q. Let $D$ be a formula in Clark normal form relative to q so that in every conjunctive term (48) of $D$ no occurrence of an element in ${\bf q}$ occurs in $G$ as positive and nonnegated. Formula

[TABLE]

is equivalent to formulas

[TABLE]

This result tells us that pq-stable models of $F\wedge D$ are such that they satisfy the classical first-order formula $Comp[D]$. These models also can be characterized as (i) the p-stable models of $F$ that satisfy $Comp[D]$, and (ii) the pq-stable models of $F$ extended with the counterpart of choice rules for member of q that satisfy $Comp[D]$.

For an interpretation $I$ over signature $\Sigma$, by $I_{|\sigma}$ we denote the interpretation over $\sigma\subseteq\Sigma$ constructed from $I$ so that every function or predicate symbol in $\sigma$ is assigned the same value in both $I$ and $I_{|\sigma}$. We call formula $G$ in (48) a definition of $p(\mathbf{x})$.

Theorem 8** (Lemma on Explicit Definitions)**

Let $F$ be a first-order formula, q be a set of predicate constants that do not occur in $F$, and p be an arbitrary set of predicate constants in $F$. Let $D$ be a formula in Clark normal form relative to q so that in every conjunctive term (48) of $D$ there is no occurrence of an element in ${\bf q}$ in $G$. Then

• i

$M\mapsto M_{|\sigma(F)}$* is a 1-1 correspondence between the models of $\hbox{SM}_{\bf pq}[F\wedge D]$ and the models $\hbox{SM}_{\bf p}[F]$, and*

• ii

$\hbox{SM}_{\bf pq}[F\wedge D]$* and $\hbox{SM}_{\bf pq}[F^{\bf q}\wedge D]$ are equivalent, where we understand $F^{\bf q}$ as a formula obtained from $F$ by replacing occurrences of the definitions of $q(\mathbf{x})$ in $D$ with $q(\mathbf{x})$.*

• iii

$\hbox{SM}_{\bf pq}[F\wedge D]$* and $\hbox{SM}_{\bf pq}[F^{\prime\bf q}\wedge D]$ are equivalent, where we understand $F^{\prime\bf q}$ as a formula obtained from $F$ by replacing occurrences of any subformula of the definitions of $q(\mathbf{x})$ in $D$ with $q(\mathbf{x})$.*

It is easy to see that the program composed of the single rule

[TABLE]

and the program $p(\mathbf{y})\leftarrow F(\mathbf{x},\mathbf{y})$ are strongly equivalent. Thus, we can identify rule (23) in the Plan-disj encoding with the rule

[TABLE]

Using this fact and Theorem 8 allows us to support Claim 6. Take $F$ to be the FOL representation of Plan-choice encoding extended with any Plan-instance and $D$ be the FOL representation of (54), q be composed of a single predicate $\mathit{sthHpd}$ and p be composed of all the predicates in Plan-choice and Plan-instance.

3.4 Projection

\citeN

har16 considered a rewriting technique called projection. We start by reviewing their results. We then illustrate how the theory developed here is applicable in their settings. Furthermore, it allows us to generalize their results to more complex programs. In addition, our results give us a proof of correctness for system projector [Hippen and Lierler (2019)] that implements so called $\alpha$ and $\beta$-projections.

\citeN

har16 considered programs to be first-order sentence formed as a conjunction of formulas of the form

[TABLE]

It is easy to see that the FOL-representation of RASPL-1 rule without aggregate expressions comply with this form. We will now generalize the main result by \citeNhar16 to the case of RASPL-1 programs.

Recall how in Section 3.2.2 we identify the logical connective $\neg$ with its counterpart used in logic programs, namely, $not$. This allows us to call an expression $not\ a$, where $a$ is an atom, a literal. To simplify the presentation of rewriting in this section we will treat $L_{1},\dots,L_{k}$ in (28) as a set of literals. We will also identify body (29) with the set $\{e_{1},\dots,e_{m},not\ e_{m+1},not\ e_{n}\}$ of its elements.

Let $R$ be a RASPL-1 rule in a program $\Pi$, and let x be a non-empty tuple of variables occurring only in body of $R$ outside of any aggregate expression. By $\alpha({\bf x,y})$ we denote a set of literals in the body of $R$ so that it includes all literals in the body of $R$ that contain at least one variable from x. Tuple y denotes all the variables occurring in the literals of $\alpha({\bf x,y})$ different from x. By $\alpha^{\prime}$ we denote any subset of $\alpha({\bf x,y})$ whose literals do not contain any variables occurring in ${\bf x}$. By $\mathit{Body}$ and $H$ we denote the body and the head of $R$ respectively. Let $u$ be a predicate symbol that does not occur in $\Pi$. Then a result of projecting variables ${\bf x}$ out of $R$ using predicate symbol $u$ consists of the following two rules

[TABLE]

For example, one possible result of projecting $Y$ out of

[TABLE]

using predicate symbol $u$ is

[TABLE]

Another possible result of projecting $Y$ out of rule (55) using predicate symbol $u$ consists of rule (56) and rule

[TABLE]

Yet, another possible result of projecting $Y$ out of rule (55) using predicate symbol $u$ consists of rule

[TABLE]

and rule (58).

We are now ready to state a formal result about projecting that is a generalization of Theorem 6 in [Harrison and Lierler (2016)].

Theorem 9

Let $R$ be a RASPL-1 rule in a program $\Pi$, and let x be a non-empty tuple of variables occurring only in body of $R$ outside of any aggregate expression and not in the head. If $\Pi^{\prime}$ is constructed from $\Pi$ by replacing $R$ in $\Pi$ with a result of projecting variables ${\bf x}$ out of $R$ using a predicate symbol $u$ that is not in the signature of $\Pi$, then M\mapsto M_{|\sigma(\hbox{\widehat{\Pi}})} is a 1-1 correspondence between the models of SM{}_{{\bf p},u}[\hbox{\widehat{\Pi^{\prime}}}] and the models of SM{}_{{\bf p}}[\hbox{\widehat{\Pi}}].

This result on correctness of projection is immediate consequences of Lemma on Explicit Definitions presented here. We note that the proof of a more restricted statement by \citeNhar16 is rather complex relying directly on the definition of SM operator. This illustrates the utility of presented theory, e.g., Lemma on Explicit Definitions, as it equips ASP practitioners with a formal result that eases a construction of proofs of correctness of their rewritings.

\citeN

hip18 considered rewritings that they call $\alpha$ and $\beta$-projections. They also implement these rewritings in system projector. Both $\alpha$ and $\beta$-projections are instances of the projection defined here. As a result, Theorem 9 provides a proof of correctness for the $\alpha$ and $\beta$-projections.

Here we reproduce the definition of $\alpha$-projection by \citeN[Section 2]hip18 for the case of positive rules of the form

[TABLE]

where $a_{0}$ is an atom or $\bot$ and $a_{1},\dots,a_{m}$ are atoms (we use the notation of this paper to reproduce the definition). Expression (55) exemplifies a positive rule. For a positive rule $\rho$ and a set ${\bf x}$ of variables, by $\mathit{alpha}(\rho,{\bf x})$ we denote the set of all atoms in the body of $\rho$ such that they contain some variable in ${\bf x}$. For instance, let $\rho_{1}$ be rule  (55). Then,

[TABLE]

For a set ${\bf x}$ of variables and a positive rule $\rho$ of the form $H\leftarrow\mathit{Body}$, where no variable in ${\bf x}$ occurs in $H$, the process of $\alpha$-projecting ${\bf x}$ out of this rule will result in replacing it by two rules:

a rule

[TABLE]

so that

• •

$u$ is a fresh predicate symbol with respect to original program, and

• •

${\bf y}$ is composed of the variables that occur in $\mathit{alpha}(\rho,{\bf x})$, but not in ${\bf x}$; 2. 2.

a rule

[TABLE]

For instance, replacing rule (55) with rules (56) and (57) exemplifies $\alpha$-projection of $Y$. It is easy to see that $\alpha$-projection on positive programs is an instance of projection rewriting studied here. The definitions of $\alpha$ and $\beta$-projections for general programs require substantially more notation. Thus, we refer an interested reader to the paper by \citeN[Section 2]hip18 for the details. Yet, it is still easy to see that these rewritings are instances of projection as defined here. For example, replacing rule (55) with rules (59) and (58) exemplifies $\beta$-projection.

4 Conclusions

We illustrated how the concepts of strong equivalence and conservative extensions can be used jointly to argue the correctness of a newly designed program or correctness of program rewritings. This work outlines a methodology for such arguments. Also, this paper lifts several important theoretical results for propositional programs to the case of first-order logic programs. These new formal findings allow us to argue a number of first-order program rewritings to be safe. We illustrate the usefulness of these findings by utilizing them in constructing an argument which shows that the sample programs Plan-choice and Plan-disj are essentially the same. We believe that these results provide a strong building block for a portfolio of safe rewritings that can be used in creating an automatic tool for carrying these rewritings during program performance optimization phase. For example, system projector discussed in the last section implements projection rewritings for the sake of performance. In this work we utilized the presented formal results to argue the correctness of this system.

Acknowledgements

We are grateful to Pedro Cabalar, Jorge Fandinno, Nicholas Hippen, Vladimir Lifschitz, Miroslaw Truszczynski for valuable discussions on the subject of this paper. We are also thankful to the anonymous reviewers for their help to improve the presentation of the material in the paper. Yuliya Lierler was partially supported by the NSF 1707371 grant.

Appendix A ”Weak” Natural Deduction System

Recall that in addition to introducing the strong equivalence, \citeNlif01 also illustrated that traditional programs can be associated with the propositional formulas and a question whether the programs are strongly equivalent can be turned into a question whether the respective propositional formulas are equivalent in the HT logic. The authors also state that every formula provable in the natural deduction system, where the axiom of the law of the excluded middle ($F\vee\neg F$) is replaced by the weak law of the excluded middle ($\neg F\vee\neg\neg F$), is a theorem of logic HT. We call this system weak natural deduction system. Since we use this observation in providing formal arguments stated in Section 2, we review the weak natural deduction system here. We denote this system by N. Its review follows the lines of [Lifschitz (2016)] to a large extent. For another reference to natural deductions system we refer the reader to [Lifschitz et al. (2008)]. We note that \citeNmin10 introduced an alternative sequent calculus for logic of HT that was further generalized to first-order case.

A sequent is an expression of the form

[TABLE]

(“$F$ under assumptions $\mathcal{G}$”), where $F$ is a propositional formula that allows connectives

[TABLE]

and $\mathcal{G}$ is a finite set of formulas. If $\mathcal{G}$ is written as $\{G_{1},\dots,G_{n}\}$, we drop the braces and write (60) as $G_{1},\dots,G_{n}\Rightarrow F.$ Intuitively, this sequent is understood as the formula $(G_{1}\wedge\cdots\wedge G_{n})\rightarrow F$ if $n>0$, and as $F$ if $n=0$.

The axioms of N are sequents of the forms

[TABLE]

In the list of inference rules presented in Figure 3, $\mathcal{G}$, $\Delta$, $\Sigma$ are finite sets of formulas, and $F,G,H$ are formulas. The inference rules of N except for the two rules at the last row are classified into introduction rules $({\mathbf{\cdot}}I)$ and elimination rules $({\mathbf{\cdot}}E)$; the exceptions are the contradiction rule $(C)$ and the weakening rule $(W)$.

A proof/derivation is a list of sequents $S_{1},\dots,S_{n}$ such that each $S_{i}$ is either an axiom or can be derived from some of the sequents in $S_{1},\dots,S_{i-1}$ by one of the inference rules. To prove a sequent $S$ means to find a proof with the last sequent $S$. To prove a formula $F$ means to prove the sequent $\Rightarrow F$.

The De Morgan’s law

[TABLE]

is provable intuitionistically (where we understand formula $H\leftrightarrow H^{\prime}$ as an abbreviation for $(H\rightarrow H^{\prime})\wedge(H^{\prime}\rightarrow H)$). Thus, formulas $\neg(F\vee G)$ and $\neg F\wedge\neg G$ are intuitionistically equivalent. The other De Morgan’s law

[TABLE]

is such that its one half is provable intuitionistically, while the other one is provable in HT (thus, formulas $\neg(F\wedge G)$ and $\neg F\vee\neg G$ are equivalent in HT-logic). We illustrate the latter fact in Figure 4 using system N. In other words, we prove sequent $\Rightarrow\neg(F\wedge G)\rightarrow\neg F\vee\neg G$ in N. It is convenient to introduce abbreviations for the assumptions used in the proofs so that $A_{1}$ abbreviates assumption $\neg(F\wedge G)$ in Figure 4.

It is easy to show that the propositional formulas $F\rightarrow\bot$ and $\neg F$ are equivalent using N, so that in the sequel we often identify rules of the form

[TABLE]

with the propositional formula

[TABLE]

Appendix B Proofs

B.1 Proofs for Section 2

To prove Proposition 1 several earlier results from the literature are of use.

Proposition 5** (Replacement Theorem I in [Mints (2000)], Section 2.8)**

If $F$ is a formula containing a subformula $G$ and $F^{\prime}$ is the result of replacing that subformula by $G^{\prime}$ then $G\leftrightarrow G^{\prime}$ intuitionistically implies $F\leftrightarrow F^{\prime}$.

To rely on formal results stated earlier in the literature, we now consider the case of programs that are more general than traditional logic programs. We call such programs definitional. In other words, traditional programs are their special case. A definitional program consists of rules of the form (3) (recall that we identify rule (1) with the propositional formula (3)) and rules of the form $a\rightarrow F$, where $a$ is an atom and $F$ is a basic conjunction. If a program contains two rules $F\rightarrow a$ and $a\rightarrow F$ we abbreviate that by a single expression $F\leftrightarrow a$. A definitional program is a special case of propositional theories presented in [Ferraris (2005)]. We understand answer sets for definitional programs as presented there. \citeN[Section 2]fer05 illustrates that in application to any traditional program the definition from [Lifschitz et al. (1999)], presented here, and their definition are equivalent.

We now restate the results that immediately follow from Lemma on Explicit Definitions and Completion Lemma presented in [Ferraris (2005)] for the case of definitional programs.

Proposition 6** (Proposition 4 [Ferraris (2005)])**

Let $\Pi$ be a definitional program and $Q$ be a set of atoms that do not occur in $\Pi$. For each $q\in Q$, let $Def(q)$ be a basic conjunction that does not contain any atom in $Q$. Then, $X\mapsto X\setminus Q$ is a 1-1 correspondence between the answer sets if $\Pi\cup\{Def(q)\rightarrow q\mid q\in Q\}$ and the answer sets of $\Pi$.

Proposition 7** (Proposition 5 [Ferraris (2005)])**

Let $\Pi$ be a definitional program and $Q$ be a set of atoms that do not occur in $\Pi$. For each $q\in Q$, let $Def(q)$ be a basic conjunction that does not contain any atom in $Q$. Then, $\Pi\cup\{Def(q)\rightarrow q\mid q\in Q\}$ and $\Pi\cup\{Def(q)\leftrightarrow q\mid q\in Q\}$ have the same answer sets.

Proof B.10** (Proof of Proposition 1).**

By $\Pi^{\prime}$ we denote a program constructed from $\Pi$ by adding a rule $def(q)\rightarrow q$ for every atom $q\in Q$. By Proposition 6, $\Pi^{\prime}$ is a conservative extension of $\Pi$. By Proposition 7, traditional program $\Pi^{\prime}$ has the same answer sets as the definitional program $\Pi^{\prime\prime}$ constructed from $\Pi^{\prime}$ by replacing a rule $def(q)\rightarrow q$ with a rule $def(q)\leftrightarrow q$ . Similarly, traditional program $\Pi[Q,def(Q)]$ has the same answer sets as the definitional program $\Pi[Q,def(Q)]^{\prime}$ constructed from it by replacing a rule $def(q)\rightarrow q$ with a rule $def(q)\leftrightarrow q$. By Replacement Theorem I, $\Pi^{\prime\prime}$ and $\Pi[Q,def(Q)]^{\prime}$ are strongly equivalent.

We now state auxiliary lemmas that are useful in the argument of Proposition 3. It is constructed by uncovering the formal link between logic programs $simp_{T}(D)$ and $lp_{T}(D)$, where $lp_{T}(D)$ serves the role of a gold standard by the virtue of Proposition 2.

Lemma B.11**.**

If $F$ is a formula containing a subformula $G$ and $F^{\prime}$ is the result of replacing that subformula by $G^{\prime}$ then the sequent

[TABLE]

is provable in N, where $\Gamma$ is arbitrary set of assumptions.

Proof B.12**.**

Trivially follows from the Replacement Theorem I stated as Proposition 5 here.

Lemma B.13**.**

The sequent

[TABLE]

is provable in N.

Proof B.14**.**

We illustrate the proof in N for the sequent

[TABLE]

We allow ourselves a freedom to use De Morgan’s Laws as if they were given to us as additional inference rules in N.

[TABLE]

Similar proofs in structure are available for the sequents

[TABLE]

Several applications of $(\wedge I)$ will allow us to conclude the proof in N for the sequent in the statement of this lemma.

Proof B.15** (Proof of Proposition 3).**

It is easy to see that the signatures of $simp_{T}(D)$ and $lp_{T}(D)$ differ by complement action atoms present in $lp_{T}(D)$. What we show next is the fact that $lp_{T}(D)$ is a conservative extension of $simp_{T}(D)$. Then the claim of this proposition follows from Proposition 2.

Claim 1*: The set of rules from groups 1 and 3 of $lp_{T}(D)$ are strongly equivalent to the set of rules from group 1 of $lp_{T}(D)$ and the rules*

[TABLE]

for all $t=0,\dots,T-1$, for every dynamic law (7) in $D$.

It is easy to see that these sets of rules only differ in structure of rules (12) and (61) so that the atoms of the form \hbox{\overline{l_{i}}}(t+1) $(1\leq i\leq m)$ in (12) are replaced by the expressions of the form not\ \hbox{\widehat{l_{i}}}(t+1) in (61).

Let $\Gamma$ denote the set of rules from group 1 of $lp_{T}(D)$. Using Lemmas B.11 and B.13 it is easy to see that the sequent 1 presented in Figure 5 is provable in N. It is easy to construct a proof in N from this sequent 1 to the sequent 2 in the same figure. This immediately concludes the proof of Claim 1.

Claim 2*: The set of rules from groups 1 and 2 of $lp_{T}(D)$ are strongly equivalent to the set of rules from group 1 and 2 of $simp_{T}(D)$.*

The proof for this claim follows the lines of a proof for Claim 1.

Claim 3*: The set of rules from groups 1 and 4 of $lp_{T}(D)$ are strongly equivalent to the set of rules from group 1 and 4 of $simp_{T}(D)$.*

The proof for this claim is similar to that of a proof of Claim 1.

Due to Claims 1, 2, and 3, it follows that $lp_{T}(D)$ has the same answer sets as the program $lp^{\prime}_{T}(D)$ constructed from $lp_{T}(D)$ by replacing (i) the rules from group 3 with rules (61) for all $t=0,\dots,T-1$, for every dynamic law (7) in $D$, and (ii) the rules from groups 2 and 4 in $lp_{T}(D)$ by the rules from groups 2 and 4 in $simp_{T}(D)$.

Let def(\hbox{\hbox{-}{a}}) denote formula $\neg a$ for every elementary action $a$ in $\sigma^{act}_{T}$. It is easy to see that $lp^{\prime}_{T}(D)$ coincides with the program

[TABLE]

By Proposition 1, program $lp^{\prime}_{T}(D)$ is a conservative extension of $simp_{T}(D)$. Consequently, $lp_{T}(D)$ is a conservative extension of $simp_{T}(D)$.

B.2 Proofs for Section 3

Proof B.16** (Proof of Theorem 2).**

Consider the case when $H$ is a disjunction of atoms then FOL representation of rule (36) is the universal closure of formula

[TABLE]

The FOL representation of rule (37) is the universal closure of formula

[TABLE]

Given that formula $\forall\mathbf{z}(H\rightarrow H^{\prime})$ where $H^{\prime}$ has no free occurrences of variables in $\mathbf{z}$ is intuitionistically equivalent to $\exists\mathbf{z}(H)\rightarrow H^{\prime}$, the FOL representation of rule (37) can be written as the universal closure of formula

[TABLE]

It is easy to see that the left hand sides of the implications in this formula and formula (62) are classically equivalent. And thus by Replacement Theorem II these formulas are intuitionistically equivalent. Similarly we can argue for the case when $H$ is of the form $\{a\}$.

Proof B.17** (Outline of the Proof of Theorem 3).**

We can derive the former program given in the theorem statement (its FOL representation) from the latter intuitionistically; and we can derive the later from the former in logic SQHT=. For the second direction, De Morgan’s law $\neg(F\wedge G)\rightarrow\neg F\vee\neg G$ (provable in logic SQHT=, but not valid intuitionistically) is essential.

To prove Theorem 4 we recall the Splitting Lemma from [Ferraris et al. (2009)] (this Splitting Lemma is the generalization of the Splitting Set Theorem [Lifschitz and Turner (1994)]).

Splitting Lemma.   Let $F$ be a first-order sentence.

Version 1*: Let p, q be disjoint tuples of distinct predicate constants. If each strongly connected component of $DG_{\bf pq}[F]$ is a subset of p or a subset of q, then $\hbox{SM}_{\bf pq}[F]$ is equivalent to $\hbox{SM}_{\bf p}[F]\wedge\hbox{SM}_{\bf q}[F]$.*

Version 2*: Let p be a tuple of distinct predicate constants. If ${\bf c^{1},\dots,c^{n}}$ are all the strongly connected components of $DG_{\bf p}[F]$, then $\hbox{SM}_{\bf p}[F]$ is equivalent to $\hbox{SM}_{\bf c^{1}}[F]\wedge\cdots\wedge\hbox{SM}_{\bf c^{n}}[F]$. *

Proof B.18** (Proof of Theorem 4).**

We start by partitioning $C$ into two sets $Q$ and ${\bf r}$ so that

• •

any element in $Q$ is such that at least one of its predicate symbols occurs in a head of some rule in $\bf R$,

• •

any element in ${\bf r}$ is such that none of its predicate symbols occurs in a head of some rule in $\bf R$.

We identify set ${\bf r}$ with a tuple (order is immaterial) composed of the predicate symbols occurring in its elements. For set $Q$ we identify every strongly connected component ${\bf q}\in Q$, with a tuple of predicate symbols in this component.

By $\Pi^{sh}$ we denote a program constructed from $\Pi$ by replacing each rule $R\in\bf R$ with \hbox{\mathit{shift}}_{\mathcal{P}^{R}}(R).

By definition, an answer set of $\Pi$ is an Herbrand model of formula (35). Similarly, an answer set of $\Pi^{sh}$ is an Herbrand model of

[TABLE]

We now show that formulas (35) and  (63) are equivalent.

By the Splitting Lemma, formula (35) is equivalent to

[TABLE]

Theorem 5 from [Ferraris et al. (2011)] shows that given formulas $\hbox{SM}_{{\bf p}}[F]$ and $\hbox{SM}_{{\bf p}}[G]$ so that $\pi(F)=\pi(G)$ if the equivalence between $F$ and $G$ can be derived intuitionistically from the law of excluded middle formulas for all predicates in $\pi(F)\setminus{\bf p}$, then they have the same stable models. Following claims are the consequences of that theorem

• •

\hbox{SM}_{{\bf r}}[\hbox{\widehat{\Pi}}]* is equivalent to \hbox{SM}_{{\bf r}}[\hbox{\widehat{\Pi^{sh}}}],*

• •

for every ${\bf q}$ in $Q$, \hbox{SM}_{{\bf q}}[\hbox{\widehat{\Pi}}] is equivalent to \hbox{SM}_{{\bf q}}[\hbox{\widehat{\Pi^{sh}}}].

Consequently, formula (64) is equivalent to formula

[TABLE]

It is easy to see that \pi(\hbox{\widehat{\Pi}})=\pi(\hbox{\widehat{\Pi^{sh}}}). By the Splitting Lemma, formula (65) is equivalent to (63).

In order to state a proof for Completion Lemma, we recall several important theorems from [Ferraris et al. (2009), Ferraris et al. (2011)].

Theorem B.19** **(Splitting Theorem [[Ferraris

et al. (2009)](#bib.bib13)]).

Let $F$ and $D$ be first-order sentences, and let ${\bf p,q}$ be disjoint tuples of distinct predicate constants. If

• •

each strongly connected component of $DG_{\bf p,q}[F\wedge D]$ is a subset of p or q,

• •

members of p have no strictly positive occurrences in $D$, and

• •

members of q have no strictly positive occurrences in $F$

then

[TABLE]

Theorem B.20** **(Theorem 2 [[Ferraris

et al. (2011)](#bib.bib12)]).

Let $F$ be first-order sentences, and let ${\bf p,q}$ be disjoint tuples of distinct predicate constants. Then

[TABLE]

We say that formula $\hbox{SM}_{\bf p}[F]$ is tight if the graph $DG_{\bf p}[F]$ is acyclic.

Theorem B.21** **(Theorem 11 [[Ferraris

et al. (2009)](#bib.bib13)]).

For any tight formula $\hbox{SM}_{\bf p}[F]$ where $F$ is in Clark normal form relative to p, $\hbox{SM}_{\bf p}[F]$ is equivalent to the completion of $F$.

Proof B.22** (Proof of Theorem 7).**

Recall that $D$ and $Comp[D]$ denote

[TABLE]

respectively. From the conditions posed on the occurrence of elements in q in $F$ and $D$ it is easy to see that every element in q forms a singleton strongly connected component in $DG_{\bf p,q}[F\wedge D]$ and in $DG_{\bf q}[D]$. Consequently, each strongly connected component of $DG_{\bf p,q}[F\wedge D]$ is a subset of p or q and $D$ is tight. Furthermore, by the assumptions of the theorem, members of p have no strictly positive occurrences in $D$, and members of q have no strictly positive occurrences in $F$. By Theorem B.19, formula (50) is equivalent to $\hbox{SM}_{\bf p}[F]\wedge\hbox{SM}_{\bf q}[D]$. By Theorem B.21, $\hbox{SM}_{\bf q}[D]$ is equivalent to $Comp[D]$. Consequently, formula (50) is equivalent to (51) and (52). By Theorem B.20, formula (52) is equivalent to formula (53).

Proof B.23** (Proof of Theorem 8).**

By Theorem 8, $\hbox{SM}_{\bf pq}[F\wedge D]$ is equivalent to $\hbox{SM}_{\bf p}[F]\wedge Comp[D]$. Formula $Comp[D]$ corresponds to so called explicit definitions of predicates in q. There is an obvious 1-1 correspondence between the models of $\hbox{SM}_{\bf p}[F]$ and the models of the same formula extended with explicit definitions (for predicates that do not occur in $F$). In particular, if $M$ is a model of $\hbox{SM}_{\bf p}[F]\wedge Comp[D]$ then $M_{|\sigma(F)}$ is a model of $\hbox{SM}_{\bf p}[F]$. This concludes the proof of statement (i). By the Replacement Theorem for intuitionistic logic, we conclude that $\hbox{SM}_{\bf p}[F]\wedge Comp[D]$ is equivalent to $\hbox{SM}_{\bf p}[F^{\bf q}]\wedge Comp[D]$ and hence to $\hbox{SM}_{\bf pq}[F^{\bf q}\wedge D]$ by Theorem 8. This concludes the proof of statement (ii). Statement (iii) is proved similarly.