#  Integration and Simulation of Bivariate Projective-Cauchy Distributions
within Arbitrary Polygonal Domains

Jonathan Dupuy Laurent Belcour Eric Heitz

###### Abstract

Consider a uniform variate on the unit upper-half sphere of dimension $d$. It
is known that the straight-line projection through the center of the unit
sphere onto the plane above it distributes this variate according to a
$d$-dimensional projective-Cauchy distribution. In this work, we leverage the
geometry of this construction in dimension $d=2$ to derive new properties for
the bivariate projective-Cauchy distribution. Specifically, we reveal via
geometric intuitions that integrating and simulating a bivariate projective-
Cauchy distribution within an arbitrary domain translates into respectively
measuring and sampling the solid angle subtended by the geometry of this
domain as seen from the origin of the unit sphere. To make this result
practical for, e.g., generating truncated variants of the bivariate
projective-Cauchy distribution, we extend it in two respects. First, we
provide a generalization to Cauchy distributions parameterized by location-
scale-correlation coefficients. Second, we provide a specialization to
polygonal-domains, which leads to closed-form expressions. We provide a
complete MATLAB implementation for the case of triangular domains, and briefly
discuss the case of elliptical domains and how to further extend our results
to bivariate Student distributions.

&

$d\mathbf{x}$

$d\boldsymbol{\omega}$

$\mathcal{S}^{2}$

$\mathbb{R}^{2}\times\\{1\\}$

${\color[rgb]{0.10,0.50,0.10}\definecolor[named]{pgfstrokecolor}{rgb}{0.10,0.50,0.10}d\boldsymbol{\omega}}=\frac{1}{(x_{1}^{2}+x_{2}^{2}+1)^{3/2}}{\color[rgb]{0.86,0.00,0.00}\definecolor[named]{pgfstrokecolor}{rgb}{0.86,0.00,0.00}d\mathbf{x}}$

(1) (2)

Figure 1: Projective construction of the (1) univariate and (2) bivariate
Cauchy distribution.

&

$\mathbb{D}$

(1) (2)

Figure 2: Isocontours of (1) the bivariate Cauchy density. We show how to (2)
integrate and simulate random variates distributed according to such a density
over an arbitrary domain $\mathbb{D}$.

##  1 Introduction

### Construction of the Projective-Cauchy Distribution.

A classic way of constructing a projective-Cauchy distribution is the
following [6, 3]: Consider the projection of the upper-half unit sphere
$\mathcal{S}^{d}$ of $\mathbb{R}^{d+1}$, $d\geq 1$, onto the plane
$\mathbb{R}^{d}\times\\{1\\}\subset\mathbb{R}^{d+1}$ defined as

$\displaystyle g_{\perp}(\boldsymbol{\omega})$
$\displaystyle=(\omega_{1}/\omega_{d+1},\,\ldots,\omega_{d}/\omega_{d+1},\,1),$
(1)

where we use the notation
$\boldsymbol{\omega}=(\omega_{1},\,\ldots,\,\omega_{d+1})\in\mathcal{S}^{d}$,
i.e., $\|\boldsymbol{\omega}\|=1$. The application of such a projection to a
uniform variate on the upper-half unit sphere $\mathcal{S}^{d}$ of
$\mathbb{R}^{d+1}$ distributes it on the $\mathbb{R}^{d}\times\\{1\\}$ plane
according to a standard projective-Cauchy distribution111 Existing literature
[6, 3] consider a uniform variate on the unit sphere $\mathcal{S}^{d}$ rather
than on its upper-half as we do here. Since the projection defined in Equation
(1) is a two-to-one mapping as for any
$\boldsymbol{\omega}\in\mathcal{S}^{d}$, we have
$g_{\perp}(\boldsymbol{\omega})=g_{\perp}(-\boldsymbol{\omega})$, it follows
trivially that applying $g_{\perp}$ to a uniform variate on the upper-half
unit sphere of $\mathbb{R}^{d+1}$ also distributes it on the
$\mathbb{R}^{d}\times\\{1\\}$ plane according to a standard projective-Cauchy
distribution. with density

$p_{\textrm{std}}(\mathbf{x})=\frac{\Gamma(\alpha)}{\pi^{\alpha}}\frac{1}{(x_{1}^{2}+\cdots+x_{d}^{2}+1)^{\alpha}},\quad\alpha=\frac{d+1}{2},$
(2)

where we use the notation
$\mathbf{x}=(x_{1},\,\ldots,\,x_{d},\,1)\in\mathbb{R}^{d}\times\\{1\\}$;
Figure  Integration and Simulation of Bivariate Projective-Cauchy
Distributions within Arbitrary Polygonal Domains illustrates the geometry of
this construction for the $d=\\{1,2\\}$ cases.

### Bivariate Case.

In this work, we focus on the specific case of the standard bivariate
projective-Cauchy probability distribution, whose density is given by Equation
(2) with $d=2$, i.e.,

$f_{\textrm{std}}(\mathbf{x})=\frac{1}{2\pi}\frac{1}{(x_{1}^{2}+x_{2}^{2}+1)^{3/2}}.$
(3)

Figure  Integration and Simulation of Bivariate Projective-Cauchy
Distributions within Arbitrary Polygonal Domains (1) shows a color-mapped plot
of such a density, which is radially-symmetric and heavy-tailed. Hereafter, we
refer to the standard bivariate projective-Cauchy distribution simply as the
bivariate Cauchy distribution.

### Contributions and Outline.

In the following sections, we leverage the geometry of the projective
construction to derive new properties for the bivariate Cauchy distribution.
Specifically, we show that the projective construction links the bivariate
Cauchy distribution to the solid-angle metric in Section 2. Based on this
result, we introduce a systematic approach to simulate and integrate the
bivariate Cauchy distribution against an arbitrary domain
$\mathbb{D}\subseteq\mathbb{R}^{2}$ in Section 3; this is useful, for, e.g.,
generating truncated variants of the bivariate Cauchy distribution. Next, we
extend our results to more general bivariate Cauchy densities parameterized by
location-scale-correlation coefficients in Section 4. Finally, we consider the
special case where the domain $\mathbb{D}$ represents the area enclosed by an
arbitrary triangle in Section 5; Figure  Integration and Simulation of
Bivariate Projective-Cauchy Distributions within Arbitrary Polygonal Domains
(2) shows an example of simulation of a location-scale-correlation Cauchy
variate within a triangle using our contributions. A complete MATLAB
implementation is provided in the supplemental material of this work.

##  2 The Bivariate Cauchy Metric as the projection of Solid Angles

In this section, we introduce and prove the main result of this paper. For
this, we need to consider the mapping $g_{\perp}$ defined in Equation (1)
along with its inverse $g_{\perp}^{-1}$, which is defined as

$g_{\perp}^{-1}(\mathbf{x})=\frac{(x_{1},\,\ldots,\,x_{d},1)}{\|(x_{1},\,\ldots,\,x_{d},1)\|}.$
(4)

### Main Result.

In the case $d=2$, the bivariate Cauchy density evaluates to the product of
the uniform density on the upper-half sphere $\mathcal{S}^{2}$, times the
Jacobian due to the change of measure from
$d\boldsymbol{\omega}\subset\mathcal{S}^{2}$ to
$d\mathbf{x}\subset\mathbb{R}^{2}\times\\{1\\}$:
$f_{\textrm{std}}(\mathbf{x})=\frac{1}{2\pi}\left\|\frac{dg_{\perp}^{-1}(\mathbf{x})}{d\mathbf{x}}\right\|.$
(5) Put in other words, the bivariate Cauchy distribution is a solid-angle
measure expressed on the plane subtented by the action of $g_{\perp}$ on the
upper-half unit sphere $\mathcal{S}^{2}$.

### Proof.

Let us consider an infinitesimal solid angle
$d\boldsymbol{\omega}\subset\mathcal{S}^{2}$ centered around a directon
$\boldsymbol{\omega}\in\mathcal{S}^{2}$ under the action of the projective
mapping $g_{\perp}$. The projection maps $d\boldsymbol{\omega}$ to an
infinitesimal area $d\mathbf{x}$ located on the $\mathbb{R}^{2}\cup\\{1\\}$
plane around the point
$\mathbf{x}=g_{\perp}(\boldsymbol{\omega})\in\mathbb{R}^{2}\cup\\{1\\}$;
Figure  Integration and Simulation of Bivariate Projective-Cauchy
Distributions within Arbitrary Polygonal Domains (1) illustrates this setup.

&

$d\mathbf{x}$

$\mathbf{x}$

$d\boldsymbol{\omega}$

$\boldsymbol{\omega}$

$\theta$

$\|\mathbf{x}\|\,=\,\sqrt{x_{1}^{2}+x_{2}^{2}+1}$

$\mathcal{S}^{2}$

$\mathbb{R}^{2}\times\\{1\\}$

(1) (2)

Figure 3: Projective construction of the bivariate projective-Cauchy
distribution. The projection operator maps (1) solid angles to areas, whose
respective metrics are (2) linked through simple algebraic relations.

By construction, the infinitesimal area $d\mathbf{x}$ is located at distance
$\|\mathbf{x}\|=\|g_{\perp}(\boldsymbol{\omega})\|$ from the origin and
projected at an angle $\theta$ onto the $\mathbb{R}^{2}\cup\\{1\\}$ plane;
Figure  Integration and Simulation of Bivariate Projective-Cauchy
Distributions within Arbitrary Polygonal Domains (2) illustrates this
geometric relationship. Since solid angles scale quadratically with distance
and oriented projections produces a foreshortening effect of $\sin\theta$, we
have

$\displaystyle\|\mathbf{x}\|^{2}\,d\boldsymbol{\omega}$
$\displaystyle=\sin\theta\,d\mathbf{x}.$ (6)

Now, using the identities $\|\mathbf{x}\|=\sqrt{x_{1}^{2}+x_{2}^{2}+1}$ and
$\sin\theta=1/\|\mathbf{x}\|$, we further obtain

$d\boldsymbol{\omega}=\frac{1}{(x_{1}^{2}+x_{2}^{2}+1)^{3/2}}\,d\mathbf{x}.$
(7)

Hence, the Jacobian $\left\|\frac{d\boldsymbol{\omega}}{d\mathbf{x}}\right\|$
is directly proportional to Equation (3). Under the projective construction,
the algebraic expression of the bivariate Cauchy density translates into the
Jacobian of the projection, which is Equation (7), normalized by the solid
angle of the hemisphere, which is $2\pi$. Using the equality
$\boldsymbol{\omega}=g_{\perp}^{-1}(\mathbf{x})$, we finally obtain our main
result:

$f_{\textrm{std}}(\mathbf{x})=\frac{1}{2\pi}\left\|\frac{d\boldsymbol{\omega}}{d\mathbf{x}}$
(8) =12π∥dg⟂-1(x)dx∥.

This concludes our proof.

##  3 Integration and Simulation

In this section, we introduce a systematic approach for simulating and
integrating the bivariate Cauchy distribution within an arbitrary domain
$\mathbb{D}\subseteq\mathbb{R}^{2}\times\\{1\\}$. This requires the following
corollary result:

### Corollary Result.

Consider an arbitrary domain $\mathbb{D}\subseteq\mathbb{R}^{2}\times\\{1\\}$.
The inverse projection $g_{\perp}^{-1}$ maps $\mathbb{D}$ to the solid angle
it subtends with respect to the unit sphere $\mathcal{S}^{2}$ of
$\mathbb{R}^{3}$.

### Variate Simulation.

The projective construction of the bivariate Cauchy distribution implies a
straightforward simulation mechanism: it suffices to generate a uniform
variate within the solid angle $\Omega=g_{\perp}^{-1}(\mathbb{D})$ and project
it using $g_{\perp}$, i.e., Equation (1) with $d=2$; Figure  Integration and
Simulation of Bivariate Projective-Cauchy Distributions within Arbitrary
Polygonal Domains (1) illustrates this approach. It follows that if the
geometry of $\Omega$ can be analytically sampled with uniform probability,
then the bivariate Cauchy distribution can be simulated analytically within
the area enclosed by $\mathbb{D}$.

### Bounded Integration.

The projective construction of the bivariate Cauchy distribution implies a
straightforward method for solving integrals of the form

$\displaystyle\mathcal{I}=\int_{\mathbb{D}}f_{\textrm{std}}(\mathbf{x})\,d\mathbf{x}.$
(9)

Let $\Omega$ denote the solid angle subtented by $\mathbb{D}$ with respect to
the unit sphere unit sphere $\mathcal{S}^{2}$ of $\mathbb{R}^{3}$, i.e.,
$\Omega=g_{\perp}^{-1}(\mathbb{D})$. We re-express Equation (9) as a measure
over solid-angles using the substitution
$\mathbf{x}=g_{\perp}(\boldsymbol{\omega})$, which makes integrand constant

$\mathcal{I}=\int_{\Omega}\underbrace{f_{\textrm{std}}(g_{\perp}(\boldsymbol{\omega}))}_{=\frac{1}{2\pi}\left\|\frac{d\boldsymbol{\omega}}{d\mathbf{x}}\right\|,\,\textrm{Eq.(\ref{eq_main_result}})}\left\|\frac{d\mathbf{x}}{d\boldsymbol{\omega}}\right\|d\boldsymbol{\omega}=\int_{\Omega}\frac{1}{2\pi}\;d\boldsymbol{\omega},\quad\Omega=g_{\perp}^{-1}(\mathbb{D}).$
(10)

Put in other words, integrating the bivariate Cauchy distribution reduces to
computing a solid angle; Figure  Integration and Simulation of Bivariate
Projective-Cauchy Distributions within Arbitrary Polygonal Domains (2)
illustrates this approach. It follows that if the solid angle of $\Omega$ can
be computed analytically, then the bivariate Cauchy distribution can be
integrated analytically within the area enclosed by $\mathbb{D}$.

&

$\mathcal{S}^{2}$

$\mathbb{R}^{2}\times\\{1\\}$

$\Omega$

$\mathbb{D}$

${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathbb{D}}\mapsto
g_{\perp}^{-1}({\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathbb{D}})={\color[rgb]{0.10,0.50,0.10}\definecolor[named]{pgfstrokecolor}{rgb}{0.10,0.50,0.10}\Omega}$

(1) (2)

Figure 4: Geometric interpretation of our systematic methodology for (1)
simulating and (2) integrating bivariate Cauchy distributions within an
arbitrary domain $\mathbb{D}\subseteq\mathbb{R}^{2}\times\\{1\\}$. We re-
express both operations on the surface of the unit sphere $\mathcal{S}^{2}$.

##  4 Generalization to Location-Scale-Correlation

In this section, we generalize the results of the previous section to a more
general parameterization of the bivariate Cauchy distribution.

### Parameterization.

The bivariate Cauchy density exhibits radially symmetric isocontours. These
can be extended to more general elliptic isocontours when the random variates
are transformed according to a location-scale-correlation substitution. For
the 2D case, considering the location parameters $a_{1},a_{2}\in\mathbb{R}$,
scale parameters $b_{1},b_{2}>0$, and correlation parameter $\rho\in(-1,1)$,
the transformation takes the form

$g_{\mathcal{E}}(\mathbf{x})=\left(b_{1}\,x_{1}+a_{1},\;b_{2}\left[\rho
x_{1}+x_{2}{\textstyle\sqrt{1-\rho^{2}}}\right]+a_{2},1\right).$ (11)

The application of $g_{\mathcal{E}}$ on a random variate distributed as a
bivariate Cauchy distribution redistributes it according to a more general
bivariate Cauchy distribution with density

$\displaystyle f(\mathbf{x};a_{1},a_{2},b_{1},b_{2},\rho)$
$\displaystyle=f_{\textrm{std}}\left(g^{-1}_{\mathcal{E}}(\mathbf{x})\right)\left\|\frac{dg^{-1}_{\mathcal{E}}(\mathbf{x})}{d\mathbf{x}}\right\|,$
(12)
$\displaystyle\left\|\frac{dg^{-1}_{\mathcal{E}}(\mathbf{x})}{d\mathbf{x}}\right\|$
$\displaystyle=\frac{1}{b_{1}b_{2}\sqrt{1-\rho^{2}}},$ (13)

where $g^{-1}_{\mathcal{E}}$ denotes the inverse of $g_{\mathcal{E}}$, which
takes the form

$g^{-1}_{\mathcal{E}}(\mathbf{x})=\left(\frac{x_{1}-a_{1}}{b_{1}},\frac{b_{1}(x_{2}-a_{2})-\rho\,b_{2}(x_{1}-a_{1})}{b_{1}b_{2}\sqrt{1-\rho^{2}}},1\right).$
(14)

The standard bivariate Cauchy case corresponds to setting the parameters to
$a_{1}=a_{2}=0$, $b_{1}=b_{2}=1$, and $\rho=0$. Figure  Integration and
Simulation of Bivariate Projective-Cauchy Distributions within Arbitrary
Polygonal Domains plots the isocontours of the standard bivariate Cauchy
density against that of an elliptic one. Hereafter, we refer to such
generalized bivariate Cauchy distributions as elliptical bivariate Cauchy
distributions. Note that Equation (12) is equivalent to the more standard
expression

$f(\mathbf{x};a_{1},a_{2},b_{1},b_{2},\rho)=\frac{1}{2\pi
b_{1}b_{2}\sqrt{1-\rho^{2}}}\left(1+\frac{z}{1-\rho^{2}}\right)^{-\frac{3}{2}},$
(15)

where

$z=\frac{(x_{1}-a_{1})^{2}}{b_{1}^{2}}+\frac{(x_{2}-a_{2})^{2}}{b_{2}^{2}}-\frac{2\rho(x_{1}-a_{1})(x_{2}-a_{2})}{b_{1}b_{2}}.$
(16)

& (1) (2)

Figure 5: Isocontours of (1) the standard projective-Cauchy density, and (2) a
general projective-Cauchy density with location parameters
$a_{1}=-1.9,a_{2}=-0.1$, scale parameters $b_{1}=1.4,b_{2}=1.7$, and
correlation $\rho=0.8$.

### Variate Simulation.

The location-scale-correlation construction of the elliptical bivariate Cauchy
distribution implies a straightforward simulation mechanism within an
arbitrary domain $\mathbb{D}\subset\mathbb{R}^{2}\times\\{1\\}$: it suffices
to generate a bivariate Cauchy variate within the domain
$\mathbb{D}_{\textrm{std}}=g_{\mathcal{E}}^{-1}(\mathbb{D})$ using the results
from the previous section, i.e., uniformily sample the spherical domain
$\Omega=g_{\perp}^{-1}(\mathbb{D}_{\textrm{std}})$, and then transform it
using Equation (11); Figure  Integration and Simulation of Bivariate
Projective-Cauchy Distributions within Arbitrary Polygonal Domains illustrates
this approach. It follows that if the geometry of
$\Omega=g_{\perp}^{-1}(\mathbb{D}_{\textrm{std}})$ can be analytically sampled
with uniform probability, then the bivariate Cauchy distribution can be
simulated analytically within the area enclosed by $\mathbb{D}$.

### Bounded Integration.

The location-scale-correlation construction of the elliptical bivariate Cauchy
distribution implies a straightforward method for solving integrals of the
form

$\displaystyle\mathcal{J}=\int_{\mathbb{D}}f(\mathbf{y};a_{1},a_{2},b_{1},b_{2},\rho)\,d\mathbf{y}.$
(17)

Let $\mathbb{D}_{\textrm{std}}$ denote the domain resulting from the
application of $g_{\mathcal{E}}$ to $\mathbb{D}$. We re-express Equation (17)
as a measure over the bivariate Cauchy distribution using the substitution
$\mathbf{y}=g_{\mathcal{E}}(\mathbf{x})$, i.e.,

$\mathcal{J}=\int_{\mathbb{D}_{\textrm{std}}}\underbrace{f(g_{\mathcal{E}}(\mathbf{x});a_{1},a_{2},b_{1},b_{2},\rho)}_{=f_{\textrm{std}}(\mathbf{x})\,\left\|\frac{d\mathbf{x}}{d\mathbf{y}}\right\|\textrm{,
Eq.(\ref{eq_pdf})}}\,\left\|\frac{d\mathbf{y}}{d\mathbf{x}}\right\|\,d\mathbf{x},=\int_{\mathbb{D}_{\textrm{std}}}f_{\textrm{std}}(\mathbf{x})\,d\mathbf{x},\quad\mathbb{D}_{\textrm{std}}=g_{\mathcal{E}}^{-1}(\mathbb{D}).$
(18)

Using the results of the previous section, we re-express this new integral as
a uniform measure over solid-angles, where the integrand becomes constant

$\mathcal{J}=\int_{\Omega}\underbrace{f_{\textrm{std}}(g_{\perp}(\boldsymbol{\omega}))}_{=\frac{1}{2\pi}\left\|\frac{d\boldsymbol{\omega}}{d\mathbf{x}}\right\|,\,\textrm{Eq.(\ref{eq_main_result}})}\left\|\frac{d\mathbf{x}}{d\boldsymbol{\omega}}\right\|d\boldsymbol{\omega}=\int_{\Omega}\frac{1}{2\pi}\;d\boldsymbol{\omega},\quad\Omega=g_{\perp}^{-1}(\mathbb{D}_{\textrm{std}}).$
(19)

It follows that if the solid angle of $\Omega$ can be computed analytically,
then the elliptical bivariate Cauchy distribution can be integrated
analytically within the area enclosed by $\mathbb{D}$.

&

$\mathbb{D}_{\textrm{std}}$

(1) (2)

Figure 6: Invariance of polygonal integrals over Cauchy densities. (1) The
integral of any elliptical bivariate Cauchy density against a domain
$\mathbb{D}$ is equal to (2) another integral of a bivariate Cauchy density
over a domain $\mathbb{D}_{\textrm{std}}$.

##  5 Polygonal Bounds

In this section, we specialize our results from Section 3 to the case where
$\mathbb{D}$ represents the area enclosed by an arbitrary polygon. We also
show that these results extend trivially to the location-scale-correlation
generalization introduced in Section 4.

### Variate Simulation.

Simulating a bivariate Cauchy distribution withing the area enclosed by a
polygon requires uniformly sampling the solid angle of the spherical geometry
it subtends via $g_{\perp}^{-1}$, which is a spherical polygon, and then
projecting these samples using Equation (1). If
$\mathbf{v}_{1},\ldots,\mathbf{v}_{n}\in\mathbb{R}^{2}\times\\{1\\}$ denote
the vertices of the polygon, then the spherical polygon has vertices
$g_{\perp}^{-1}(\mathbf{v}_{1}),\ldots,g_{\perp}^{-1}(\mathbf{v}_{n})\in\mathcal{S}^{2}$.
For details on how to uniformly sampling such geometries, we refer the reader
to the literature on the subject [2, 7], as this is out of the scope of this
paper; Appendix 7 provides pseudocode for the case where the polygonal-domain
is defined by an arbitrary triangle, and Figure  Integration and Simulation of
Bivariate Projective-Cauchy Distributions within Arbitrary Polygonal Domains
(2) shows an example of variate simulation within a triangle.

### Polygonal Integration.

Integrating a bivariate Cauchy distribution against the area enclosed by a
polygon requires computing the solid angle of the spherical geometry it
subtends via $g_{\perp}^{-1}$, which is a spherical polygon. For a polygon
with $N\geq 3$ vertices, the solid angle of the spherical polygon is given by

$\mathcal{I}=\sum_{n=1}^{N}A_{n}-(N-2)\pi,$ (20)

where $A_{n}:=A_{n}(\Omega)$ denotes the $n$-th interior angle of the
spherical polygon. Appendix 7 provides pseudocode for the case where the
polygonal-domain is defined by an arbitrary triangle.

### Location-Scale-Correlation Generalization.

The results derived here for the bivariate Cauchy distribution extend
trivially to the location-scale-correlation generalization of Section 4: Since
the mapping $g_{\mathcal{E}}$ defined in Equation (14) is a linear
transformation, it acts as an automorphism on polygons. Put in other words, if
we can integrate and simulate the bivariate Cauchy density against arbitrary
polygons, then we can also integrate and simulate arbitrary location-scale-
correlation densities against arbitrary polygons using the simulation and
integration methods introduced in the previous section. Appendix 7 provides
pseudocode for the case where the polygonal-domain is defined by an arbitrary
triangle.

##  6 Discussion

In this section, we informally discuss the extension of our results to
elliptical domains, and Student distributions with integer-valued degrees of
freedom. We defer rigorous proofs from our claims for future work.

### On Elliptical Domains.

Following the methodology introduced in Section 3, we can integrate and
simulate the bivariate Cauchy density against arbitrary ellipses as long as we
can deal with the solid angle they subtend on $\mathcal{S}^{2}$. Such
geometries have been studied in the literature, and there exists methods to
compute their solid angles [5], as well as uniform-sample them [4].
Furthermore, the mapping $g_{\mathcal{E}}$ acts as an automorphism on
ellipses, which means that we can also integrate and simulate arbitrary
location-scale-correlation densities against arbitrary ellipses.

### On Student Distributions.

As demonstrated by Equation (5), the bivariate Cauchy distribution arises from
the uniform distribution on the upper-half sphere $\mathcal{S}^{2}$ times the
Jacobian of the projection $g_{\perp}$. This suggests a mechanism for deriving
other distributions than just the Cauchy distribution by weighting directional
distributions that differ from the uniform one. Interestingly, if we consider
the power-law distribution $\omega_{3}^{\nu}$, $\nu\geq 1$, then using the
identity due to Equation (4)

$\omega_{3}=\frac{1}{\sqrt{x_{1}^{2}+x_{2}^{2}+1}},$ (21)

we get

$d\boldsymbol{\omega}=\frac{1}{(x_{1}^{2}+x_{2}^{2}+1)^{\frac{2+\nu}{2}}}d\mathbf{x},$
(22)

which implies that the Jacobian
$\left\|\frac{d\boldsymbol{\omega}}{d\mathbf{x}}\right\|$ is now directly
proportional to the bivariate Student distribution with $\nu$ degrees of
freedom. As such, any integral of the form

$\mathcal{I}^{\prime}=\int_{\mathbb{D}}\frac{1}{(x_{1}^{2}+x_{2}^{2}+1)^{\frac{2+\nu}{2}}}d\mathbf{x},$
(23)

may be re-expressed in the directional domain as a

$\mathcal{I}^{\prime}=\int_{\Omega}\omega_{3}^{\nu}\,d\boldsymbol{\omega},\quad\Omega=g_{\perp}^{-1}(\mathbb{D}).$
(24)

Since it is known that such integrals have analytical solutions over polygonal
domains for any $\nu\in\mathbb{N}$ [1], we believe that new properties for the
bivariate Student distribution may be derived based on our results for the
bivariate Cauchy distribution.

##  7 Appendix: Pseudocode

⬇

1/* Project to the unit hemisphere */

2function PlaneToHemisphere($\mathbf{x}=\\{x_{1},\;x_{2},\;1\\}$)

3 return $\boldsymbol{\omega}=\mathbf{x}\;/\;\|\mathbf{x}\|$

4

5/* Project to the plane */

6function
HemisphereToPlane($\boldsymbol{\omega}=\\{\omega_{1},\;\omega_{2},\;\omega_{3}\\}$)

7 return $\mathbf{x}=\boldsymbol{\omega}\;/\;\omega_{3}$

8

9/* Polygonal simulation of a standard bivariate Cauchy distribution */

10function
SimulateCauchyStd($\mathcal{P}=\\{\mathbf{v}_{1},\ldots,\mathbf{v}_{N}\\}$,
$\mathbf{u}=\\{u_{1},\;u_{2}\\}$)

11 $\Omega\;\leftarrow\;\\{$PlaneToHemisphere($\mathbf{v}_{1}$)$,\ldots,$
PlaneToHemisphere($\mathbf{v}_{N}$)$\\}$

12 return HemisphereToPlane(SampleSolidAngle($\Omega$, $\mathbf{u}$))

13

14/* Polygonal integral of a standard bivariate Cauchy distribution */

15function
IntegrateCauchyStd($\mathcal{P}=\\{\mathbf{v}_{1},\ldots,\mathbf{v}_{N}\\}$)

16 $\Omega\;\leftarrow\;\\{$PlaneToHemisphere($\mathbf{v}_{1}$)$,\ldots,$
PlaneToHemisphere($\mathbf{v}_{N}$)$\\}$

17 return ComputeSolidAngle($\Omega$)

Listing 1: Simulating and integrating a bivariate Cauchy density against a
polygon.

⬇

1/* LocationScaleCorrelationForward */

2function LSCForward($\mathbf{x}=\\{x_{1},\;x_{2},\;1\\}$,
$a_{1},\;a_{2},\;b_{1},\;b_{2},\;\rho$)

3 /* See Equation (6) */

4 $x_{1}^{\prime}\;\leftarrow\;b_{1}x_{1}+a_{1}$

5 $x_{2}^{\prime}\;\leftarrow\;b_{2}[\rho
x_{1}+x_{2}{\textstyle\sqrt{1-\rho^{2}}}]+a_{2}$

6 return $\\{x_{1}^{\prime},\;x_{2}^{\prime},\;1\\}$

7

8/* LocationScaleCorrelationForward */

9function LSCBackward($\mathbf{x}=\\{x_{1},\;x_{2},\;1\\}$,
$a_{1},\;a_{2},\;b_{1},\;b_{2},\;\rho$)

10 /* See Equation (6) */

11 $x_{1}^{\prime}\;\leftarrow\;(x_{1}-a_{1})\;/\;b_{1}$

12
$x_{2}^{\prime}\;\leftarrow\;(b_{1}(x_{2}-a_{2})-\rho\,b_{2}(x_{1}-a_{1}))\;/\;(b_{1}b_{2}\sqrt{1-\rho^{2}})$

13 return $\\{x_{1}^{\prime},\;x_{2}^{\prime},\;1\\}$

14

15/* Polygonal simulation of a standard bivariate Cauchy distribution */

16function
SimulateCauchyElliptic($\mathcal{P}=\\{\mathbf{v}_{1},\ldots,\mathbf{v}_{N}\\}$,
$\mathbf{u}=\\{u_{1},\;u_{2}\\}$)

17 return LSCForward(SimulateCauchy(LSCBackward($\mathcal{P}$), $\mathbf{u}$))

18

19/* Polygonal integral of a standard bivariate Cauchy distribution */

20function
IntegrateCauchyElliptic($\mathcal{P}=\\{\mathbf{v}_{1},\ldots,\mathbf{v}_{N}\\}$)

21 return IntegrateCauchyStd(LSCBackward($\mathcal{P}$))

Listing 2: Simulating and integrating a bivariate Cauchy density against a
polygon with location-scale-correlation parameters.

## References

  * [1] James Arvo.  Applications of irradiance tensors to the simulation of non-lambertian phenomena.  In Proceedings of the 22nd annual conference on Computer graphics and interactive techniques, pages 335–342. ACM, 1995.
  * [2] James Arvo.  Stratified sampling of spherical triangles.  In Proceedings of the 22Nd Annual Conference on Computer Graphics and Interactive Techniques, SIGGRAPH ’95, pages 437–438, New York, NY, USA, 1995. ACM.
  * [3] Jean-Louis Dunau and Henri Sénateur.  Une caracterisation du type de la loi de cauchy-conforme sur rn.  Probability Theory and Related Fields, 77(1):129–135, Mar 1988\.
  * [4] Ibón Guillén, Carlos Ureña, Alan King, Marcos Fajardo, Iliyan Georgiev, Jorge López-Moreno, and Adrian Jarabo.  Area-preserving parameterizations for spherical ellipses.  In Computer Graphics Forum, volume 36, pages 179–187. Wiley Online Library, 2017.
  * [5] Eric Heitz.  Computing a front-facing ellipse that subtends the same solid angle as an arbitrarily oriented ellipse.  working paper or preprint, July 2017.
  * [6] FB Knight and PA Meyer.  Une caractérisation de la loi de cauchy.  Zeitschrift für Wahrscheinlichkeitstheorie und Verwandte Gebiete, 34(2):129–134, 1976.
  * [7] Carlos Ureña, Marcos Fajardo, and Alan King.  An area-preserving parametrization for spherical rectangles.  In Computer Graphics Forum, volume 32, pages 59–66. Wiley Online Library, 2013.


March 2003 External Behavior of a Logic Program and Verification of
Refactoring–LABEL:lastpage

# External Behavior of a Logic Program
and Verification of Refactoring

JORGE FANDINNO  ZACHARY HANSEN  YULIYA LIERLER
University of Nebraska Omaha  VLADIMIR LIFSCHITZ  NATHAN TEMPLE
University of Texas at Austin

(2003)

###### Abstract

Refactoring is modifying a program without changing its external behavior. In
this paper, we make the concept of external behavior precise for a simple
answer set programming language. Then we describe a proof assistant for the
task of verifying that refactoring a program in that language is performed
correctly.

###### doi:

S1471068401001193

###### keywords:

Answer set programming, software verification, proof assistant, automated
reasoning

##  1 Introduction

This paper is about the process of refactoring in the context of answer set
programming (ASP), that is, about modifying an ASP program without changing
its external behavior. Examples of refactoring logic programs can be found in
papers by ser03 (ser03), geb11b (geb11b, Section 3.1) and bud15 (bud15,
Section 3). In this paper we propose, for a simple ASP language, a precise
definition of external behavior and a method for verifying that two programs
exhibit the same external behavior.

Refactoring a program usually involves a series of small changes that improve
its structure or performance. The example below shows that, in ASP,
refactoring may serve also another purpose: to transform a program that a
grounder classifies as unsafe into an equivalent program that it is able to
ground. The program

      composite(I*J) :- I > 1, J > 1.
            prime(I) :- I = a..b, not composite(I).

defines the set of primes in the interval $\\{a,\dots,b\\}$, assuming that
$a>1$. The grounder gringo [Gebser et al. (2019)] tells us that the program is
unsafe. A safe program defining the same set can be obtained by replacing the
first rule with

      composite(I*J) :- I = 2..b, J = 2..b.

This is an example of refactoring, because the extent of `prime/1` did not
change.

We can also refactor the program to improve its performance using the fact
that every composite number in $\\{a,\dots,b\\}$ has a divisor in the interval
$\\{2,\dots\lfloor\sqrt{b}\rfloor\\}$:

           sqrt_b(M) :- M = 1..b, M*M <= b, (M+1)*(M+1) > b.
      composite(I*J) :- sqrt_b(M), I = 2..M, J = 2..b.
            prime(I) :- I = a..b, not composite(I).

In the Abstract Gringo language [Gebser et al. (2015)], a program is defined
as a set of rules, so that a program includes neither directives nor comments.
Under this narrow definition, the program itself does not tell us which
predicate symbols are meant to represent the output, and which symbols are
auxiliary. But this difference is essential, because changing auxiliary
predicates does not indicate a mistake in the process of refactoring.

Furthermore, the rules of a program do not show what kind of input is supposed
to be provided for it. Generally, an input for an ASP program can be specified
in two ways. First, some symbolic constants, such as a and b in the programs
above, may be meant to serve as placeholders for elements of the input.
Second, some predicate symbols occurring in the program may occur in the
bodies of rules only, not in the heads. The extents of such predicates may be
specified as part of input when we run the program. Some inputs may not
conform to the programmer’s assumptions about the intended use of the program.
For instance, when we run the prime number programs above, the placeholders a
and b are expected to be replaced by integers; the cases when they are
replaced by symbolic constants are not related to external behavior if the
programs are used as intended.

To sum up, _what we consider external behavior of a set of rules depends on
how these rules are meant to be used._ In Sections 3–5, we make this idea
precise for the subset of Abstract Gringo called mini-gringo (fan20, Section
2; lif22a, Sections 2, 3). After that, we describe the proof assistant
anthem-p2p,111Available at https://github.com/ZachJHansen/anthem-p2p. which
uses the theorem prover vampire [Kovaćs and Voronkov (2013)] to verify that
two mini-gringo programs have the same external behavior. This proof assistant
is built on top of the system anthem [Fandinno et al. (2020)], whose focus is
on the related and yet different task of confirming that an ASP program
adheres to its specification. The prime number programs above are used as a
running example. To make the paper more self-contained, we have reviewed some
background material in Appendices A–C.

##  2 On the syntax of mini-gringo

There are minor syntactic differences between mini-gringo and the input
language of the grounder gringo, explained by the fact the former is designed
for theoretical studies, and the latter for actual programming. For example,
the definition of `sqrt_b/1` in the introduction, rewritten in the syntax of
mini-gringo, becomes

$\emph{sqrt\\_b\/}(M)\leftarrow M=\overline{1}\,..\,b\,\land\,M\times M\leq
b\,\land\,(M+\overline{1})\times(M+\overline{1})>b.$

Overlined symbols, such as $\overline{1}$, are “numerals”—syntactic objects
representing integers. In examples of rules and programs, we will freely
switch between the two styles.

In mini-gringo, _precomputed terms_ are numerals, symbolic constants, and the
symbols _inf_ , _sup_. We assume that a total order on precomputed terms is
chosen, such that _inf_ is its least element, _sup_ is its greatest element,
and, for all integers $m$ and $n$, $\overline{m}<\overline{n}$ iff $m<n$. A
_precomputed atom_ is an expression of the form $p({\bf t})$, where $p$ is a
symbolic constant and $\bf t$ is a tuple of precomputed terms. A _predicate
symbol_ is a pair $p/n$, where $p$ is a symbolic constant and $n$ is a
nonnegative integer. About a rule or another syntactic expressions we say that
it _contains_ $p/n$ if it contains an atom of the form $p(t_{1},\dots,t_{n})$.

##  3 External behavior

Definition 1  A _user guide_ is a quadruple

$(\emph{PH},\emph{In},\emph{Out},\emph{Dom\/})$ (1)

where

  * •

_PH_ is a finite set of symbolic constants, called _placeholders_ ,

  * •

_In_ and _Out_ are disjoint finite sets of predicate symbols, called _input
symbols_ and _output symbols_ , and

  * •

_Dom_ is a set such that each of its elements is a pair $(v,\mathcal{I})$,
where

    * (i)

$v$ is a function that maps elements of  _PH_ to precomputed terms that do not
belong to  _PH_ , and

    * (ii)

$\mathcal{I}$ is a subset of the set of precomputed atoms that contain an
input symbol and do not contain placeholders.

The set _Dom_ is the _domain_ of the user guide, and pairs $(v,\mathcal{I})$
satisfying conditions (i) and (ii) are called _inputs_. An input
$(v,\mathcal{I})$ represents a way to choose the values of placeholders and
the extents of input predicates: for every placeholder $c$, specify $v(c)$ as
its value, and add the atoms $\mathcal{I}$ to the rules of the program as
facts. If $\Pi$ is a mini-gringo program then $v(\Pi)$ stands for the program
obtained from $\Pi$ by replacing every occurrence of every constant $c$ in the
domain of $v$ by $v(c)$. Using this notation, we can say that choosing
$(v,\mathcal{I})$ as input for $\Pi$ amounts to replacing $\Pi$ by the program
$v(\Pi)\cup\mathcal{I}$.

To use a program in accordance with user guide (1) means to run it for inputs
that belong to _Dom_. The inputs that do not belong to _Dom_ are not related
to the external behavior of the program when it is used as intended.

Example 1  The intended use of the programs discussed in the introduction can
be described by user guide (1) with $\emph{PH}=\\{a,b\\}$,
$\emph{In}=\emptyset$, $\emph{Out}=\\{\emph{prime}/1\\}$, and with the domain
consisting of the inputs $(v,\emptyset)$ such that $v(a)$, $v(b)$ are
numerals. (We could choose also to include the condition $v(b)\geq
v(a)>\overline{1}$.) This user guide will be denoted by $\emph{UG}_{p}$.

Example 2  We would like to describe the meaning of the word _orphan_ by a
logic program [Gelfond and Kahl (2014), Section 4.1.2]. The intended use of
such a program can be described by user guide (1) with

$\emph{PH}=\emptyset,\
\emph{In}=\\{\emph{father/2},\emph{mother/2},\emph{living/1}\\},\
\emph{Out}=\\{\emph{orphan/1}\\},$

and with the domain consisting of all inputs. We will denote this user guide
by $\emph{UG}_{o}$. In the next two sections, we examine two possible
definitions of _orphan/1_ and consider the question of their equivalence with
respect to $\emph{UG}_{o}$.

User guides are closely related to lp-functions [Gelfond (2002), Section 2],
and also to io-programs [Fandinno et al. (2020), Section 5], reviewed in C.

An _output atom_ of a user guide  _UG_ is a precomputed atom that contains an
output symbol of  _UG_.

Definition 2  Let $(v,\mathcal{I})$ be an input in the domain of a user guide
_UG_ , and let $\Pi$ be a mini-gringo program such that the heads of its rules
do not contain input symbols of  _UG_. The _external behavior_ of $\Pi$ for
the user guide  _UG_ and the input $(v,\mathcal{I})$ is the collection of all
sets that can be represented as the intersection of a stable model of
$v(\Pi)\cup\mathcal{I}$ with the set of output atoms of  _UG_.

Example 1, continued  If $\Pi$ is one of the three prime number programs from
the introduction, and $(v,\mathcal{I})$ is an input in the domain of
$\emph{UG}_{p}$, then the program $v(\Pi)\cup\mathcal{I}$ is $v(\Pi)$, and it
has a unique stable model. If $v$ is defined by the conditions
$v(a)=\overline{10}$, $v(b)=\overline{15}$, then that stable model includes
the atoms $\emph{prime}(\overline{11})$, $\emph{prime}(\overline{13})$, and
some atoms containing $\emph{composite}/1$. The external behavior of each of
the programs for this input is
$\\{\\{\emph{prime}(\overline{11}),\emph{prime}(\overline{13})\\}\\}$. For the
safe and optimized versions, this external behavior can be calculated by
instructing clingo to find all answers for the file obtained from the program
by appending the directives

      #const a = 10.  #const b = 15.  #show prime/1.

Example 2, continued  If $\Pi$ is the program

$\begin{array}[]{l}\verb|parent_living(X) :- father(Y,X), living(Y).|\\\
\verb|parent_living(X) :- mother(Y,X), living(Y).|\\\ \verb| orphan(X) :-
living(X), not parent_living(X).|\end{array}$ (2)

and $(v,\mathcal{I})$ is an input in the domain of $\emph{UG}_{o}$, then the
program $v(\Pi)\cup\mathcal{I}$ is $\Pi\cup\mathcal{I}$, and it has a unique
stable model. If $\mathcal{I}$ is

$\begin{array}[]{l}\\{\emph{father\/}(\emph{jacob},\emph{joseph}),\emph{mother\/}(\emph{rachel},\emph{joseph}),\\\
\quad\quad\emph{living}(\emph{jacob}),\emph{living}(\emph{rachel}),\emph{living}(\emph{joseph})\\},\end{array}$
(3)

then that stable model includes the atoms $\emph{orphan\/}(\emph{jacob})$,
$\emph{orphan\/}(\emph{rachel})$, and some atoms containing predicate symbols
other than _orphan/1_. The external behavior of this program for
$\emph{UG}_{o}$ and input (3) is

$\\{\\{\emph{orphan\/}(\emph{jacob}),\emph{orphan\/}(\emph{rachel})\\}\\}.$
(4)

It can be calculated by instructing clingo to find all answers for the file
obtained from program (2) by appending the facts

      father(jacob,joseph).
      mother(rachel,joseph).
      living(jacob). living(rachel). living(joseph).

and the directive `#show orphan/1`.

In the special case when _UG_ has neither placeholders nor input symbols, and
its set of output symbols includes all predicate symbols occurring in $\Pi$,
the external behavior of $\Pi$ with respect to  _UG_ and
$(\emptyset,\emptyset)$ is the set of stable models of $\Pi$. In this sense,
the concept of external behavior is a generalization of the stable model
semantics.

##  4 Equivalence

Definition 3  Let  _UG_ be a user guide, and let $\Pi_{1}$, $\Pi_{2}$ be mini-
gringo programs such that the heads of their rules do not contain input
symbols of  _UG_. We say that $\Pi_{1}$ is _equivalent to $\Pi_{2}$ with
respect to_  _UG_ if, for every input $(v,\mathcal{I})$ in the domain of  _UG_
, the external behavior of $\Pi_{1}$ for  _UG_ and $(v,\mathcal{I})$ is the
same as the external behavior of $\Pi_{2}$.

Example 1, continued  The three programs from the introduction are equivalent
to each other with respect to $\emph{UG}_{p}$. As discussed in Section 6, this
claim can be verified using the automated reasoning tools anthem-p2p and
vampire.

Example 2, continued  Perhaps surprisingly, the one-rule program

$\begin{array}[]{l}\verb|orphan(X) :- living(X), father(Y,X), mother(Z,X),|\\\
\verb| not living(Y), not living(Z).|\end{array}$ (5)

is not equivalent to (2) with respect to $\emph{UG}_{o}$. Indeed, the external
behavior of this program with respect to $\emph{UG}_{o}$ and input (3) is
$\\{\emptyset\\}$, which is different from (4). We will see that anthem-p2p
can help us clarify the relationship between programs (2) and (5).

We understand _refactoring_ a mini-gringo program with respect to a user guide
_UG_ as replacing it by a program that is equivalent to it with respect to
_UG_.

This equivalence relation is essentially an example of relativized uniform
equivalence with projection [Oetsch and Tompits (2008)], except that the
language discussed by oet08 includes neither arithmetic operations nor
placeholders. It is _uniform_ equivalence, because the programs are extended
by adding facts, rather than more complex rules; _relativized_ , because these
facts $\mathcal{I}$ are assumed to be atoms containing input symbols, not
arbitrary atoms; _with projection_ , because we look at the output atoms in
the stable model, not the entire model.

##  5 Formal notation for user guides

To design software for verifying the equivalence of programs with respect to a
user guide, we need to represent user guides in formal notation. The format
that we chose for user guide files is similar to the format of specification
files, defined by fan20 2020 within their work on the system anthem.
Placeholders and input symbols are represented by `input` statements, for
instance:

      input: n.
      input: living/1, father/2, mother/2.

Output symbols are represented by `output` statements:

      output: prime/1.

There can be several statements of both kinds in a user guide file, in any
order.

The question of representing the domain _Dom_ by a string of characters is
more difficult, because the domain is a set of inputs, which is generally
infinite. Our approach is to define “assumptions” as sentences of an
appropriate first-order language, and characterize the domain by a list of
assumptions; an input belongs to the domain iff it satisfies all assumptions
on that list.

For any set $\mathcal{P}$ of predicate symbols, by $\sigma_{0}(\mathcal{P})$
we denote the subsignature of the two-sorted signature $\sigma_{0}$, described
in A, in which the set of predicate symbols is limited to the comparison
symbols and the symbols from $\mathcal{P}$. In this paper, an _assumption_ is
a sentence over the signature $\sigma_{0}(\emph{In\/})$. Besides `input` and
`output` statements, a user guide file may include one or more statements
consisting of the word `assume` followed by an assumption.

To use assumptions as conditions on an input, we need to relate inputs to
interpretations in the sense of first-order logic. If $v$ is a function that
maps elements of some set  _PH_ of symbolic constants to symbolic constants,
and $\mathcal{I}$ is a subset of the set of precomputed atoms that contain a
predicate symbol from $\mathcal{P}$, then there exists a unique interpretation
$I$ of $\sigma_{0}(\mathcal{P})$ such that

  * (a)

the domain of the sort _general_ in $I$ is the set of all precomputed terms;

  * (b)

the domain of the sort _integer_ in $I$ is the set of all numerals;

  * (c)

$I$ interprets every symbolic constant $c$ in  _PH_ as $v(c)$;

  * (d)

$I$ interprets every precomputed term $t$ that does not belong to  _PH_ as
$t$;

  * (e)

$I$ interprets the symbols for arithmetic operations as usual in arithmetic;

  * (f)

if $p/n$ is a predicate constant from $\mathcal{P}$, and $\bf c$ is an
$n$-tuple of precomputed atoms, then $I$ interprets $p({\bf c})$ as true iff
$p({\bf c})\in\mathcal{I}$;

  * (g)

$I$ interprets the comparison symbols as in the definition of mini-gringo.

We will denote that interpretation by $I(v,\mathcal{I})$. The domain of the
user guide defined by a set of assumptions is the set of inputs
$(v,\mathcal{I})$ such that the interpretation $I(v,\mathcal{I})$ of
$\sigma_{0}(\emph{In})$ satisfies all assumptions in that set.

Example 1, continued  The user guide $\emph{UG}_{p}$ can be described by the
statements

      input: a, b.
      assume: exists N (a = N) and exists N (b = N).
      output: prime/1.

The first two lines can be written more concisely as

      input: a -> integer, b -> integer.

Example 2, continued  The user guide $\emph{UG}_{o}$ can be described by the
statements

$\begin{array}[]{l}\verb| input: living/1, father/2, mother/2.|\\\ \verb|
output: orphan/1.|\end{array}$ (6)

The absence of `assume` statements here shows that the domain is the set of
all inputs.

##  6 Functionality of anthem-p2p

The proof assistant anthem-p2p uses the theorem prover vampire to verify that
two mini-gringo programs have the same external behavior with respect to a
given user guide. We can verify, for instance, that the first two versions of
the prime number program from the introduction are equivalent with respect to
the user guide $\emph{UG}_{p}$ by running anthem-p2p on three files: the
unsafe program

$\begin{array}[]{l}\verb|composite(I*J) :- I > 1, J > 1.|\\\ \verb| prime(I)
:- I = a..b, not composite(I).|\end{array}$ (7)

the safe program

$\begin{array}[]{l}\verb|composite(I*J) :- I = 2..b, J = 2..b.|\\\ \verb|
prime(I) :- I = a..b, not composite(I).|\end{array}$ (8)

and the user guide

$\begin{array}[]{l}\verb|input: a -> integer, b -> integer.|\\\ \verb|output:
prime/1.|\end{array}$ (9)

The system anthem-p2p transforms the task of verifying equivalence with
respect to a user guide (1) into the problem of verifying the provability of a
formula in a first-order theory over the signature
$\sigma_{0}(\emph{In}\cup\emph{Out})$, and submits that problem to vampire;
see Sections 7–9 for details.

The user can help vampire organize search more efficiently by supplying
anthem-p2p with “helper” files. Such a file may instruct vampire to prove a
series of lemmas before trying to prove the goal formula. A helper file can
suggest also instances of the induction schema that may be useful for the job
in hand. This kind of help is needed, for instance, for verifying the
equivalence of the optimized prime number program to the other two.

The use of anthem-p2p for proving equivalence of programs is, generally, an
interactive process. If vampire does not prove the goal formula in the
allotted time then one of the options is to provide more lemmas and run
anthem-p2p again. Alternatively, the user can look for a counterexample that
refutes the equivalence claim, as in Example 2 above.

Sometimes, anthem-p2p can help us clarify the source of a puzzling discrepancy
between two versions of a program if we run it in the presence of additional
`assume` statements. If adding an assumption to the user guide makes the
programs equivalent then it is possible that perceiving that assumption as
self-evident is the reason why the discrepancy is puzzling. For instance, we
can observe that the anthem-p2p/vampire combination proves the equivalence of
program (2) to program (5) if we extend user guide (6) by two existence and
uniqueness assumptions:

      assume: forall X exists Y forall Z (father(Z,X) <-> Y=Z).
      assume: forall X exists Y forall Z (mother(Z,X) <-> Y=Z).

The limitations of the anthem-p2p algorithm are inherited from the limitations
of anthem and can be described as follows. The _predicate dependency graph_ of
a mini-gringo program $\Pi$ (Fandinno et al., 2020, Section 6.3) is the
directed graph that

  * •

has the predicate symbols contained in $\Pi$ as its vertices, and

  * •

has an edge from $p/n$ to $q/m$ if some rule of $\Pi$ contains $p/n$ in the
head and $q/m$ in the body.

The edge from $p/n$ to $q/m$ is _positive_ if there is a rule $R$ in $\Pi$
such that $p/n$ is contained in the head of $R$, and $q/m$ is contained in an
atom in the body of $R$ that is not in the scope of negation. For example, the
predicate dependency graph of program (2) has 6 edges; all of them except for
the edge from `parent_living/1` to `orphan/1` are positive. We say that $\Pi$
is _tight_ if this graph has no cycles consisting of positive edges.

A vertex $p/n$ of the graph is _private_ for a user guide  _UG_ if it is
neither an input symbols nor an output symbol of  _UG_. We say that $\Pi$
_uses private recursion_ for  _UG_ if

  * •

the predicate dependency graph of $\Pi$ has a cycle such that every vertex in
it is a private symbol, or

  * •

$\Pi$ includes a choice rule with the head containing a private symbol.

As discussed in the next two sections, the applicability of the algorithm
implemented in anthem-p2p to a pair of mini-gringo programs and a user guide
_UG_ is guaranteed whenever the programs are tight and do not use private
recursion with respect to  _UG_. We expect that it will be possible to replace
the tightness requirement by a significantly weaker condition using the ideas
of a recent paper on “locally tight” programs Fandinno and Lifschitz (2021);
this is a topic for future work.

##  7 Equivalence of tight programs

The theorem stated below relates equivalence of tight programs to the
satisfaction relation of second-order logic. Its statement refers to the
concept of second-order completion, reviewed in B, and also to the concept of
standard interpretation, defined as follows. An interpretation $I$ of
$\sigma_{0}(\mathcal{P})$ is _standard_ for a set  _PH_ of symbolic constants
if it satisfies conditions (a), (b), (d), (e), (g) from Section 5 and the
condition

  * (c′)

$I$ interprets every symbolic constant in  _PH_ as a term that does not belong
to  _PH_.

Theorem  _Let UG be a user guide (PH,In,Out,Dom) such that its domain is
described by a finite set of assumptions, and let Asm be the conjunction of
these assumptions. For any tight mini- gringo programs $\Pi_{1}$, $\Pi_{2}$
such that the heads of their rules do not contain the input symbols of UG,
$\Pi_{1}$ is equivalent to $\Pi_{2}$ with respect to UG iff the sentence_

$\emph{Asm}\to(\hbox{COMP}(\Pi_{1},\emph{In},\emph{Out\/})\leftrightarrow\hbox{COMP}(\Pi_{2},\emph{In},\emph{Out\/}))$
(10)

_is satisfied by all interpretations of the signature $\sigma_{0}$(In
$\cup$Out) that are standard for PH._

This theorem shows that the equivalence of tight programs may be established
by choosing a first-order theory $T$ over the signature
$\sigma_{0}(\emph{In\/}\cup\emph{Out})$ such that its axioms are satisfied by
all interpretations that are standard for  _PH_ , and then exhibiting a
derivation of formula (10) from the axioms of $T$ in classical second-order
logic. For programs that do not use private recursion, the problem of
constructing such a derivation can be reduced to proof search in first-order
logic (see Section 8 below), for which many automated reasoning tools are
available. This is the core of the procedure used by anthem-p2p.

The proof of the theorem, including the lemma below, uses terminology related
to io-programs, which is reviewed in C.

Lemma  _Let $\Pi$ be a mini-gringo program such that the heads of its rules do
not contain input symbols of a user guide_ (_PH_ ,_In_ ,_Out_ ,_Dom_). _For
any input $(v,\mathcal{I})$, a set $\mathcal{J}$ of output atoms is an element
of the external behavior of $\Pi$ for_ (_PH_ ,_In_ ,_Out_ ,_Dom_) _and
$(v,\mathcal{I})$ iff $\mathcal{I}\cup\mathcal{J}$ is an io-model of the io-
program_ ($\Pi$,_PH_ ,_In_ ,_Out_) _for $(v,\mathcal{I})$._

Proof  For every set $\mathcal{J}$ of output atoms, the conditions

  * •

$\mathcal{J}$ is the set of all output atoms in some stable model
$\mathcal{M}$ of $v(\Pi)\cup\mathcal{I}$;

  * •

$\mathcal{I}\cup\mathcal{J}$ is the set of all public atoms in some stable
model $\mathcal{M}$ of $v(\Pi)\cup\mathcal{I}$

are equivalent to each other. Indeed, since the heads of rules of $v(\Pi)$ do
not contain input atoms, the set of input atoms in $\mathcal{M}$ is
$\mathcal{I}$.

Proof of the Theorem  The condition

$\Pi_{1}\hbox{ is equivalent to }\Pi_{2}\hbox{ with respect to }\emph{UG}$
(11)

means that for any input $(v,\mathcal{I})$ such that
$I(v,\mathcal{I})\models\emph{Asm}$ and any set $\mathcal{J}$ of output atoms,

$\begin{array}[]{c}\mathcal{J}\hbox{ is an element of the external behavior
of~{}$\Pi_{1}$ for \emph{UG} and }(v,\mathcal{I})\\\ \hbox{iff}\\\
\mathcal{J}\hbox{ is an element of the external behavior of~{}$\Pi_{2}$ for
\emph{UG} and }(v,\mathcal{I}).\end{array}$ (12)

By the lemma, condition (12) can be reformulated as follows:

$\begin{array}[]{c}\mathcal{I}\cup\mathcal{J}\hbox{ is an io-model of the io-
program ($\Pi_{1}$,\emph{PH},\emph{In},\emph{Out}) for }(v,\mathcal{I})\\\
\hbox{iff}\\\ \mathcal{I}\cup\mathcal{J}\hbox{ is an io-model of the io-
program ($\Pi_{2}$,\emph{PH},\emph{In},\emph{Out}) for }(v,\mathcal{I}).\\\
\end{array}$

By the theorem quoted at the end of C, this can be further reformulated as

$I(v,\mathcal{I}\cup\mathcal{J})\models\hbox{COMP($\Pi_{1}$,\emph{In\/},\emph{Out\/})}\leftrightarrow\hbox{COMP($\Pi_{2}$,\emph{In\/},\emph{Out\/})}.$
(13)

Hence condition (11) is equivalent to requiring that (13) hold for all inputs
$(v,\mathcal{I})$ such that $I(v,\mathcal{I})\models\emph{Asm}$ and all set
$\mathcal{J}$ of output atoms.

Since assumptions do not contain output symbols,
$I(v,\mathcal{I})\models\emph{Asm}$ is equivalent to
$I(v,\mathcal{I}\cup\mathcal{J})\models\emph{Asm}$. It follows that (11) is
equivalent to asserting that implication (10) is satisfied by
$I(v,\mathcal{I}\cup\mathcal{J})$ for all inputs $(v,\mathcal{I})$ and all
sets $\mathcal{J}$ of output atoms. It remains to observe that an
interpretation of the signature $\sigma_{0}(\emph{In\/}\cup\emph{Out\/})$ can
be represented in the form $I(v,\mathcal{I}\cup\mathcal{J})$ if and only if it
is standard for  _PH_.

##  8 Reduction to first-order logic

If $\Pi_{1}$ and $\Pi_{2}$ do not use private recursion then the reference to
second-order consequences of the axioms of $T$ in Section 7 can be eliminated
in the following way. Represent the formula
COMP$(\Pi_{1},\emph{In\/},\emph{Out\/})$ in the form

$\exists{\bf P}\left(\bigwedge_{i}F_{i}({\bf P})\land F^{\prime}({\bf
P})\right),$

where $\bf P$ is a list of distinct predicate variables corresponding to the
private symbols $p_{1},p_{2},\dots$ of $\Pi_{1}$, and $F_{i}({\bf P})$ is the
formula obtained from the completed definition of $p_{i}$ in $\Pi_{1}$ by
replacing each of $p_{1},p_{2},\dots$ by the corresponding member of $\bf P$.
(Thus the conjunctive members of $F^{\prime}({\bf P})$ correspond to the
completed definitions of the output symbols and to the constraints of
$\Pi_{1}$.) Similarly, write COMP$(\Pi_{2},\emph{In\/},\emph{Out\/})$ as

$\exists{\bf Q}\left(\bigwedge_{j}G_{j}({\bf Q})\land G^{\prime}({\bf
Q})\right),$ (14)

where $\bf Q$ is a list of distinct predicate variables corresponding to the
private symbols $q_{1},q_{2},\dots$ of $\Pi_{2}$, and the formulas $G_{j}({\bf
Q})$ are obtained from the completed definitions of these symbols in $\Pi_{2}$
by replacing them with corresponding variables. Take one half

$\emph{Asm}\to(\hbox{COMP}(\Pi_{1},\emph{In},\emph{Out\/})\to\hbox{COMP}(\Pi_{2},\emph{In},\emph{Out\/}))$
(15)

of condition (10). Since $\Pi_{2}$ does not use private recursion, formula
(14) is equivalent to

$\forall{\bf Q}\left(\bigwedge_{j}G_{j}({\bf Q})\to G^{\prime}({\bf
Q})\right)$

(Fandinno et al., 2020, Theorem 3). It follows that formula (15) is equivalent
to

$\emph{Asm}\to\left(\exists{\bf P}\left(\bigwedge_{i}F_{i}({\bf P})\land
F^{\prime}({\bf P})\right)\to\forall{\bf Q}\left(\bigwedge_{j}G_{j}({\bf
Q})\to G^{\prime}({\bf Q})\right)\right)$

and consequently to

$\forall{\bf PQ}\left(\left(\emph{Asm}\land\bigwedge_{i}F_{i}({\bf
P})\land\bigwedge_{j}G_{j}({\bf Q})\right)\to(F^{\prime}({\bf P})\to
G^{\prime}({\bf Q}))\right)$ (16)

(with the bound variables in P, Q renamed, if necessary, to ensure that they
are pairwise disjoint). Similarly, the second half

$\emph{Asm}\to(\hbox{COMP}(\Pi_{2},\emph{In},\emph{Out\/})\to\hbox{COMP}(\Pi_{1},\emph{In},\emph{Out\/}))$

of condition (10) is equivalent to the formula obtained from (16) by swapping
$F^{\prime}({\bf P})$ with $G^{\prime}({\bf Q})$. Thus (10) can be rewritten
as

$\forall{\bf PQ}\left(\left(\emph{Asm}\land\bigwedge_{i}F_{i}({\bf
P})\land\bigwedge_{j}G_{j}({\bf Q})\right)\to(F^{\prime}({\bf
P})\leftrightarrow G^{\prime}({\bf Q}))\right).$

Finally, observe that this formula is entailed by the axioms of $T$ if and
only if the axioms entail the first-order formula

$\left(\emph{Asm}\land\bigwedge_{i}F_{i}({\bf p})\land\bigwedge_{j}G_{j}({\bf
q})\right)\to(F^{\prime}({\bf p})\leftrightarrow G^{\prime}({\bf q})),$ (17)

where p, q are lists of fresh predicate constants.

We return to this formula in the description of the design of anthem-p2p
below. Note that its subformulas $F_{i}({\bf p})$, $G_{j}({\bf q})$,
$F^{\prime}({\bf p})$, $G^{\prime}({\bf q})$ are parts of the first-order
completion formulas of $\Pi_{1}$ and $\Pi_{2}$, modified by replacing their
private symbols $p_{1},p_{2},\dots$, $q_{1},q_{2},\dots$ by members of the
lists p and q.

##  9 Design of anthem-p2p

The system anthem-p2p is a Python program than operates by converting a claim
about the equivalence of two mini-gringo programs into an input for anthem.
The system anthem verifies the correctness of an io-program with respect to a
formal specification. The file describing a specification includes lists of
placeholders, input symbols, output symbols, and assumptions, and also a list
of “specs” that describe the intended behavior of the future program by
sentences over the signature $\sigma_{0}(\emph{In\/}\cup\emph{Out\/})$.

Given programs $\Pi_{1}$ and $\Pi_{2}$ and a user guide (_PH_ ,_In_ ,_Out_
,_Dom_) with the domain described by assumptions  _Asm_ , anthem-p2p
constructs the following specification  _Sp_ :

  * (i)

the placeholders of  _Sp_ are the placeholders  _PH_ of the given user guide;

  * (ii)

the input symbols of  _Sp_ are the input symbols  _In_ of the user guide and
the predicate symbols p corresponding to the private symbols
$p_{1},p_{2},\dots$ of the program $\Pi_{1}$;

  * (iii)

the output symbols of  _Sp_ are the output symbols  _Out_ of the user guide;

  * (iv)

the assumptions of  _Sp_ are the assumptions  _Asm_ of the user guide and the
modified completed definitions $F_{i}({\bf p})$ of the private symbols of
$\Pi_{1}$;

  * (v)

the specs of  _Sp_ are the remaining conjunctive terms $F^{\prime}({\bf p})$
of the modified first-order completion formula of $\Pi_{1}$.

Then anthem-p2p instructs anthem to prove the claim that the io-program
$(\Pi_{2},\emph{PH},\emph{In},\emph{Out})$ implements  _Sp_. Providing anthem
with such an instruction makes it to look for a derivation of the formula

$\left(\emph{Asm}\land\bigwedge_{i}F_{i}({\bf p})\land\bigwedge_{j}G_{j}({\bf
q})\right)\to(G^{\prime}({\bf q})\leftrightarrow F^{\prime}({\bf p}))$ (18)

from the axioms of $T$ by invoking the theorem prover vampire (Fandinno et
al., 2020, Section 6.4). This formula is equivalent to (17). Thus instructing
anthem to verify that the io-program
$(\Pi_{2},\emph{PH},\emph{In},\emph{Out})$ implements the specification  _Sp_
amounts to verifying the provability of formula (17) in $T$.

As an example, consider the operation of the anthem-p2p algorithm on programs
(7) and (8) and user guide (9). In each of the programs, the only private
predicate is `composite/1`; it corresponds to both $p_{1}$ and $q_{1}$ in the
notation of Section 8. The symbols `composite_1/1` and `composite_2/1`,
generated by anthem-p2p, play the parts of $\bf p$ and $\bf q$ in formula
(17). The file describing the specification  _Sp_ is obtained in this case
from user guide (9) by adding three statements. First, in accordance with
clause (ii) in the description of _Sp_ above, anthem-p2p adds the statement

      input: composite_1/1.

Second, in accordance with clause (iv), a definition of `composite_1/1` is
assumed:

      assume: forall X (composite_1(X) <->
                        exists N1, N2 (N1 > 1 and N2 > 1 and X = N1 * N2)).

Finally, in accordance with clause (v), a definition of `prime/1` in terms of
`composite_1/1` is added as a spec:

      spec: forall X (prime(X) <->
                      exists N1 (not composite_1(N1) and
                          exists N2, N3 (N2 = a and N3 = b and
                                         N2 <= N1 and N1 <= N3) and X = N1)).

Once  _Sp_ is generated, anthem calls vampire to prove formula (18) in the
theory $T$, first by deriving the specs $F^{\prime}({\bf p})$ from the
antecedent of (18) and $G^{\prime}({\bf q})$ (“verification of specification
from translated program”), and then by deriving $G^{\prime}({\bf q})$ from the
antecedent of (18) and the specs $F^{\prime}({\bf p})$ (“verification of
translated program from specification”). In this example, the runtime of
vampire will be significantly reduced (a few seconds instead of a few minutes)
if we instruct it to start by proving two lemmas:

      lemma: forall I, J (I > 1 and J > 1 -> I < I*J).
      lemma: forall X (prime(X) ->
                       exists N1 (not composite_1(N1) and
                           exists N2, N3 (N2 = a and N3 = b and
                                          N2 <= N1 and N1 <= N3) and X = N1)).

The anthem-p2p website222Available at https://ap2p.unomaha.edu/. allows users
to experiment with the system in their web browser. The proof search is
conducted on a University of Nebraska Omaha server (Oracle Linux 8, 4 Intel(R)
Xeon(R) Gold 6248 CPUs, 4 GB RAM) subject to a 10 minute timeout. For smaller
problems, this is the recommended introduction to the system.

##  10 Conclusion

This paper contributes to the theory of logic programming by defining user
guides, external behaviors, and equivalence with respect to a user guide. The
theorem proved in Section 7 relates equivalence of tight programs to program
completion.

The problem of checking equivalence between programs arises in many areas of
computer science. For example, verifying the correctness of the translation
performed by an optimizing compiler is a problem of this kind. What is special
about the verification of refactoring is that it involves a pair of similar
programs written in the same programming language. mediator Wang et al. (2018)
is a tool that uses an SMT solver for the verification of database
refactoring.

The proof assistant anthem-p2p can be used for verifying the correctness of
refactoring an ASP program, and also for comparing alternative solutions to
the same programming problem (for instance, in classroom teaching and in ASP
programming contests). To make this tool more versatile, we plan to make it
applicable to programs with aggregates, along the lines of recent publications
(fan22a,lif22a).

## Acknowledgements

We are grateful to Isil Dillig, Warren Hunt and Jayadev Misra for valuable
comments on the problems discussed in this paper. Thanks also to Michael
Gelfond and to the anonymous referees for advice on improving the previous
version.

##  Appendix A Two-sorted formulas

The signature $\sigma_{0}$ has two sorts: the sort _general_ and its subsort
_integer_. Variables of the first sort are meant to range over arbitrary
precomputed terms, and we will identify them with variables used in mini-
gringo rules. Variables of the second sort are meant to range over
numerals—or, equivalently, integers. The signature includes

  * •

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

  * •

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

  * •

all predicate symbols $p/n$ as $n$-ary predicate constants; their arguments
have the sort _general_ ;

  * •

the comparison symbols $\neq\ <\ >\ \leq\ \geq$ as binary predicate constants;
their arguments have the sort _general_.

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

In this paper, we adopt the convention that general variables start with $U$,
$V$, $W$, $X$, $Y$, and $Z$; integer variables start with $I$, $J$, $K$, $L$,
$M$, and $N$. For example, the formula $\exists X(N=X)$ expresses that the
value of $N$ is an object of the sort _general_ ; it is universally true,
because _integer_ is a subsort of _general_. The formula $\exists N(N=X)$
expresses that the value of $X$ is an object of the sort _integer_ ; it is
generally not true.

##  Appendix B Second-order completion

Second-order completion (Fandinno et al., 2020, Sections 6.1, 6.2) is a
generalization of Clark’s completion Clark (1978) that uses bound predicate
variables to model auxiliary (“private”) predicates, such as `composite/1` in
our prime number programs. The definition covering the full syntax of mini-
gringo is rather lengthy, and in this appendix we only give an outline and an
example.

Let _In_ and _Out_ be disjoint sets of predicate symbols, and let $\Pi$ be a
mini-gringo program such that atoms in the heads of its rules do not contain
predicate symbols from  _In_. If a predicate symbol $p/n$

  * •

is contained in an atom that occurs in a rule of $\Pi$, and

  * •

belongs neither to  _In_ nor to  _Out_ ,

then $p/n$ is a _private symbol_ of $\Pi$. We denote the set of private
symbols of $\Pi$ by  _Prv_.

The _first-order completion_ of $\Pi$ is the conjunction of the following
first-order sentences over the signature
$\sigma_{0}(\emph{In\/}\cup\emph{Out\/}\cup\emph{Prv\/})$:

  * •

the completed definitions of the predicate symbols from
$\emph{Out\/}\cup\emph{Prv\/}$ in $\Pi$;

  * •

the constraints of $\Pi$ rewritten in the syntax of first-order logic.

The _second-order completion_ of $\Pi$ is the sentence over the signature
$\sigma_{0}(\emph{In\/}\cup\emph{Out\/})$ obtained from the first-order
completion of $\Pi$ by replacing all private symbols by predicate variables
and binding these variables by an existential quantifier. We will denote the
second-order completion of $\Pi$ by COMP$(\Pi,\emph{In\/},\emph{Out\/})$.

If, for instance, $\emph{In}=\emptyset$, $\emph{Out}=\\{q/2\\}$, and $\Pi$ is
the program

$\begin{array}[]{l}p(a),\\\ p(b),\\\ q(X,Y)\leftarrow p(X)\land
p(Y),\end{array}$

then $\emph{Prv}=\\{p/1\\}$, the first-order completion of $\Pi$ is

$\begin{array}[]{l}\forall V(p(V)\leftrightarrow V=a\lor V=b)\,\land\\\
\forall V_{1}V_{2}(q(V_{1},V_{2})\leftrightarrow\exists XY(q(V_{1},V_{2})\land
p(X)\land p(Y)\land V_{1}=X\land V_{2}=Y)),\end{array}$

and COMP$(\Pi,\emph{In\/},\emph{Out\/})$ is

$\begin{array}[]{l}\exists P(\forall V(P(V)\leftrightarrow V=a\lor
V=b)\,\land\\\ \forall V_{1}V_{2}(q(V_{1},V_{2})\leftrightarrow\exists
XY(q(V_{1},V_{2})\land P(X)\land P(Y)\land V_{1}=X\land
V_{2}=Y))).\end{array}$

This formula is equivalent to the first-order sentence

$\forall V_{1}V_{2}(q(V_{1},V_{2})\leftrightarrow(V_{1}=a\lor
V_{1}=b)\land(V_{2}=a\lor V_{2}=b)).$

##  Appendix C Programs with input and output

A _program with input and output_ , or an _io-program_ , is a quadruple

$(\Pi,\emph{PH},\emph{In},\emph{Out\/}),$ (19)

where _PH_ , _In_ and _Out_ are as in the definition of a user guide (Section
3), and $\Pi$ is a mini-gringo program such that the heads of its rules do not
contain symbols from _In_ (Fandinno et al., 2020, Section 5.1). Inputs for an
io-program are defined in the same way as inputs for a user guide in Section
3.

A _public atom_ of an io-program (19) is a precomputed atom that contains a
predicate symbol from $\emph{In\/}\cup\emph{Out\/}$.

An _io-model_ of an io-program (19) for an input $(v,\mathcal{I})$ is a set
that can be represented as the intersection of a stable model of
$v(\Pi)\cup\mathcal{I}$ with the set of public atoms of (19).

If $(v,\mathcal{I})$ is an input for an io-program (19), and the program $\Pi$
is tight, then, for any set $\mathcal{J}$ of output atoms,
$\mathcal{I}\cup\mathcal{J}$ is an io-model of (19) iff the interpretation
$I(v,\mathcal{I}\cup\mathcal{J})$ of the signature
$\sigma_{0}(\emph{In\/}\cup\emph{Out\/})$ satisfies the second-order
completion sentence COMP$(\Pi,\emph{In\/},\emph{Out\/})$ (Fandinno et al.,
2020, Theorem 2).

## References

  * Buddenhagen and Lierler (2015) Buddenhagen, M. and Lierler, Y. 2015\.  Performance tuning in answer set programming.  In Proceedings of International Conference on Logic Programming and Nonmonotonic Reasoning.
  * Clark (1978) Clark, K. 1978\.  Negation as failure.  In Logic and Data Bases, H. Gallaire and J. Minker, Eds. Plenum Press, New York, 293–322.
  * Fandinno et al. (2022) Fandinno, J., Hansen, Z., and Lierler, Y. 2022\.  Axiomatization of aggregates in answer set programming.  In Proceedings of the AAAI Conference on Artificial Intelligence.
  * Fandinno and Lifschitz (2021) Fandinno, J. and Lifschitz, V. 2021\.  Verification of locally tight programs (extended abstract).  In Technical Communications of the 37th International Conference on Logic Programming (ICLP).
  * Fandinno et al. (2020) Fandinno, J., Lifschitz, V., Lühne, P., and Schaub, T. 2020\.  Verifying tight logic programs with Anthem and Vampire.  Theory and Practice of Logic Programming 20.
  * Gebser et al. (2015) Gebser, M., Harrison, A., Kaminski, R., Lifschitz, V., and Schaub, T. 2015\.  Abstract Gringo.  Theory and Practice of Logic Programming 15, 449–463.
  * Gebser et al. (2019) Gebser, M., Kaminski, R., Kaufmann, B., Lindauer, M., Ostrowski, M., Romero, J., Schaub, T., and Thiele, S. 2019\.  Potassco User Guide.  Available at https://github.com/potassco/guide/releases/.
  * Gebser et al. (2011) Gebser, M., Kaminski, R., Kaufmann, B., and Schaub, T. 2011\.  Challenges in answer set solving.  In Logic programming, knowledge representation, and nonmonotonic reasoning. Essays Dedicated to Michael Gelfond on the Occasion of His 65th Birthday. Springer, 74–90.
  * Gelfond (2002) Gelfond, M. 2002\.  Representing knowledge in A-Prolog.  Lecture Notes in Computer Science 2408, 413–451.
  * Gelfond and Kahl (2014) Gelfond, M. and Kahl, Y. 2014\.  Knowledge Representation, Reasoning, and the Design of Intelligent Agents: The Answer-Set Programming Approach.  Cambridge University Press.
  * Kovaćs and Voronkov (2013) Kovaćs, L. and Voronkov, A. 2013\.  First-order theorem proving and Vampire.  In International Conference on Computer Aided Verification. 1––35.
  * Lifschitz (2022) Lifschitz, V. 2022\.  Strong equivalence of logic programs with counting.  Theory and Practice of Logic Programming 22.
  * Oetsch and Tompits (2008) Oetsch, J. and Tompits, H. 2008\.  Program correspondence under the answer-set semantics: The non-ground case.  In Proceedings of International Conference on Logic Programming.
  * Serebrenik and Demoen (2003) Serebrenik, A. and Demoen, B. 2003\.  Refactoring logic programs: Extended abstract.  In International Conference on Logic Programming.
  * Wang et al. (2018) Wang, Y., Dillig, I., Lahiri, S., and Cook, W. 2018\.  Verifying equivalence of database-driven applications.  In Proceedings of the ACM Symposium on Programming Languages.


HD 142267 | HIP 77801 | $141.2^{+2.6}_{-2.7}$ | $0.4924^{+0.0048}_{-0.0050}$ | $0.54768^{+0.00018}_{-0.00018}$
HD 144287 | HIP 78709 | $343^{+39}_{-29}$ | $5.043^{+0.052}_{-0.053}$ | $0.666^{+0.026}_{-0.022}$
HD 157338 | HD 157338 | $154^{+54}_{-47}$ | $24.1^{+13.0}_{-6.1}$ | $0.689^{+0.088}_{-0.062}$
HD 16160 | HIP 12114 | $67.3^{+1.5}_{-1.5}$ | $16.37^{+0.28}_{-0.28}$ | $0.6427^{+0.0038}_{-0.0039}$
HD 161797 | HIP 86974 | $238^{+60}_{-44}$ | $22.2^{+4.4}_{-3.2}$ | $0.427^{+0.069}_{-0.058}$
HD 167215 | HD 167215 | $201.1^{+4.2}_{-4.2}$ | $7.205^{+0.077}_{-0.076}$ | $0.8522^{+0.00059}_{-0.00066}$
HD 167215 | HD 167215 | $24.0^{+19.0}_{-4.3}$ | $7.99^{+1.00}_{-0.51}$ | $0.3^{+0.27}_{-0.20}$
HD 17382 | HIP 13081 | $197.9^{+4.5}_{-4.5}$ | $5.967^{+0.072}_{-0.073}$ | $0.6563^{+0.0058}_{-0.0061}$
HD 18445 | HIP 13769 C | $33.8^{+7.0}_{-4.3}$ | $1.209^{+0.016}_{-0.017}$ | $0.67^{+0.120}_{-0.098}$
HD 185414 | HIP 96395 | $109.4^{+3.6}_{-3.7}$ | $6.02^{+0.10}_{-0.11}$ | $0.69345^{+0.00058}_{-0.00059}$
HD 190406 | HIP 98819 | $67.4^{+2.0}_{-2.0}$ | $15.54^{+0.32}_{-0.31}$ | $0.4618^{+0.0054}_{-0.0053}$
HD 211681 | HD 211681 | $76.4^{+3.3}_{-3.2}$ | $7.79^{+0.21}_{-0.19}$ | $0.4413^{+0.0076}_{-0.0064}$
HD 215578 | HD 215578 | $1405^{+50}_{-46}$ | $25.8^{+1.3}_{-1.1}$ | $0.477^{+0.018}_{-0.016}$
HD 239960 | HIP 110893 A | $54^{+10}_{-13}$ | $15.1^{+7.1}_{-5.0}$ | $0.61^{+0.11}_{-0.14}$
HD 28185 | HD 28185 | $40^{+43}_{-28}$ | $15.9^{+7.3}_{-5.1}$ | $0.26^{+0.120}_{-0.093}$
HD 29461 | HD 29461 | $88.8^{+4.8}_{-3.4}$ | $4.907^{+0.062}_{-0.064}$ | $0.596^{+0.0140}_{-0.0088}$
HD 30649 | HD 30649 | $213.5^{+2.8}_{-2.8}$ | $16.19^{+0.25}_{-0.24}$ | $0.5878^{+0.0054}_{-0.0051}$
HD 31412 | HD 31412 | $359.9^{+8.9}_{-9.0}$ | $19.78^{+0.3}_{-0.3}$ | $0.97822^{+0.00051}_{-0.00042}$
HD 3795 | HIP 3185 | $370^{+100}_{-86}$ | $18.7^{+3.3}_{-2.7}$ | $0.296^{+0.064}_{-0.057}$
HD 5470 | HD 5470 | $229.8^{+6.0}_{-6.0}$ | $8.08^{+0.11}_{-0.11}$ | $0.35749^{+0.00110}_{-0.00088}$
HD 6558 | HIP 5189 | $220^{+260}_{-120}$ | $24.1^{+9.8}_{-7.4}$ | $0.35^{+0.12}_{-0.11}$
HD 4747 | HIP 3850 | $49.2^{+1.6}_{-1.6}$ | $9.85^{+0.17}_{-0.17}$ | $0.731^{+0.0015}_{-0.0015}$
HD 50639 | HD 50639 | $940^{+440}_{-300}$ | $31.0^{+29.0}_{-9.4}$ | $0.69^{+0.12}_{-0.09}$
HD 65430 | HIP 39064 | $95.5^{+1.7}_{-1.7}$ | $4.24^{+0.038}_{-0.039}$ | $0.37796^{+0.00068}_{-0.00066}$
HD 68017 | HIP 40118 | $33.8^{+5.7}_{-5.8}$ | $21.2^{+4.8}_{-4.4}$ | $0.432^{+0.075}_{-0.090}$
HD 6872 B | HD 6872 B | $950^{+150}_{-110}$ | $18.4^{+6.6}_{-3.4}$ | $0.718^{+0.060}_{-0.043}$
HD 72659 | HD 72659 | $230^{+730}_{-190}$ | $49^{+24}_{-19}$ | $0.21^{+0.19}_{-0.14}$
HD 8375 | HD 8375 | $146.4^{+5.8}_{-6.0}$ | $0.44^{+0.0087}_{-0.0092}$ | $0.01707^{+0.00057}_{-0.00061}$
HD 8375 | HD 8375 | $500^{+2200}_{-450}$ | $27^{+18}_{-10}$ | $0.28^{+0.25}_{-0.20}$
HD 87359 | HD 87359 | $200^{+170}_{-93}$ | $28.1^{+9.0}_{-8.7}$ | $0.28^{+0.11}_{-0.13}$
HD 8765 | HD 8765 | $43.0^{+1.5}_{-1.5}$ | $3.356^{+0.050}_{-0.052}$ | $0.3936^{+0.0099}_{-0.0095}$
HIP 42220 | HIP 42220 | $229.9^{+8.0}_{-7.7}$ | $7.06^{+0.61}_{-0.34}$ | $0.721^{+0.035}_{-0.022}$
HIP 63510 | HIP 63510 | $74.1^{+3.1}_{-3.2}$ | $4.775^{+0.057}_{-0.054}$ | $0.309^{+0.028}_{-0.025}$
HD 16287 | HIP 12158 | $126.1^{+2.4}_{-2.4}$ | $0.1129^{+0.0011}_{-0.0011}$ | $0.20693^{+0.00027}_{-0.00027}$
HD 40647 | HD 40647 | $193.9^{+5.3}_{-5.2}$ | $7.01^{+0.16}_{-0.15}$ | $0.5085^{+0.0054}_{-0.0047}$
HD 103829 | HD 103829 | $1010^{+240}_{-170}$ | $20.4^{+3.7}_{-2.4}$ | $0.468^{+0.058}_{-0.045}$
HD 139457 | HD 139457 | $240^{+430}_{-140}$ | $37^{+29}_{-15}$ | $0.64^{+0.16}_{-0.20}$
HD 167665 | HD 167665 | $48.4^{+1.4}_{-1.4}$ | $5.39^{+0.079}_{-0.080}$ | $0.3421^{+0.0040}_{-0.0044}$
HD 200565 | HD 200565 | $177^{+57}_{-34}$ | $7.22^{+1.0}_{-0.7}$ | $0.6^{+0.16}_{-0.14}$
HD 217165 | HD 217165 | $520^{+35}_{-25}$ | $24.1^{+3.9}_{-2.0}$ | $0.499^{+0.062}_{-0.039}$
HIP 52942 A | HIP 52942 A | $201^{+42}_{-24}$ | $7.99^{+0.15}_{-0.16}$ | $0.901^{+0.021}_{-0.016}$

##  Appendix E Long-Term Trends

We record all linear and parabolic trends recovered by RVSearch in Table 5.

Table 5: Long Term Trends CPS Name | Lit. Name |  $\dot{\gamma}$ [m s-1 d-1] |  $\ddot{\gamma}$ [m s-1 d-2]
---|---|---|---
HD 100623 | HIP 56452 | $0.00475\pm 0.00028$ | 0
HD 110315 | HIP 61901 | $-0.05545\pm 0.00039$ | $1.85*10^{-6}\pm 1.1*10^{-7}$
HD 110537 | HIP 62039 | $0.01936\pm 0.00051$ | 0
HD 114174 | HIP 64150 | $0.16278\pm 0.00058$ | $-2.5*10^{-6}\pm 1.4*10^{-7}$
HD 115404 A | HIP 64797 A | $0.0156\pm 0.0011$ | 0
HD 131156 | HD 131156 | $0.066\pm 0.0019$ | $2.21*10^{-6}\pm 2.9*10^{-7}$
HD 136925 | HD 136925 | $0.0026\pm 0.0012$ | $7.6*10^{-7}\pm 6.2*10^{-7}$
HD 1388 | HIP 1444 | $0.05279\pm 0.00094$ | $-4.22*10^{-6}\pm 2.2*10^{-7}$
HD 140538 A | HIP 77052 | $-0.00647\pm 0.00038$ | 0
HD 145934 | HD 145934 | $-0.0589\pm 0.0011$ | $-2.05*10^{-6}\pm 3.3*10^{-7}$
HD 145958 A | HD 145958 A | $-0.01751\pm 0.0005$ | 0
HD 145958 B | HD 145958 B | $0.01627\pm 0.00038$ | $4.1*10^{-7}\pm 1.1*10^{-7}$
HD 146362 B | HD 146362 B | $0.0139\pm 0.0011$ | 0
HD 149806 | HIP 81375 | $0.00597\pm 0.00042$ | 0
HD 153557 | HIP 83020 A | $0.0092\pm 0.0016$ | 0
HD 156668 | HD 156668 | $-0.00074\pm 0.00014$ | 0
HD 159062 | HD 159062 | $-0.0361\pm 0.0002$ | $1.14*10^{-6}\pm 1.5*10^{-7}$
HD 163489 | HD 163489 | $-0.00596\pm 0.00081$ | 0
HD 165401 | HIP 88622 | $0.14734\pm 0.00098$ | $2.63*10^{-6}\pm 6*10^{-7}$
HD 168443 | HD 168443 | $-0.00795\pm 0.00029$ | 0
HD 17230 | HD 17230 | $-0.00587\pm 0.00038$ | 0
HD 173739 | HIP 12929 | $0.01702\pm 0.00054$ | 0
HD 173740 | HIP 91772 | $-0.02088\pm 0.00054$ | 0
HD 179957 | HD 179957 | $-0.00632\pm 0.00017$ | 0
HD 179958 | HIP 94336 A | $0.00533\pm 0.00022$ | 0
HD 180617 | HD 180617 | $-0.00122\pm 0.00036$ | 0
HD 18143 | HIP 13642 A | $0.01043\pm 0.00044$ | 0
HD 182488 | HIP 95319 | $-0.00539\pm 0.00035$ | $-9.48*10^{-7}\pm 9*10^{-8}$
HD 186408 | HIP 96895 | $-0.00459\pm 0.0002$ | 0
HD 187123 | HD 187123 | $-0.00129\pm 0.00022$ | 0
HD 188512 | HIP 98036 | $0.00207\pm 0.00023$ | 0
HD 190067 | HIP 98677 | $0.01134\pm 0.00027$ | 0
HD 191408 | HIP 99461 | $0.00831\pm 0.00021$ | 0
HD 19467 | HD 19467 | $-0.00392\pm 0.0006$ | 0
HD 195019 | HD 195019 | $0.00385\pm 0.00057$ | 0
HD 195564 | HIP 101345 | $-0.091\pm 0.019$ | $-5.1*10^{-6}\pm 1.9*10^{-6}$
HD 196201 | HD 196201 | $0.23\pm 0.0029$ | $-1.03*10^{-5}\pm 7.6*10^{-7}$
HD 200968 | HIP 104239 A | $-0.02717\pm 0.00061$ | $-8*10^{-7}\pm 2.3*10^{-7}$
HD 201091 | HIP 104214 | $-0.00737\pm 0.00036$ | $-3.19*10^{-7}\pm 5.4*10^{-8}$
HD 201092 | HIP 104217 | $0.01301\pm 0.00038$ | $-4.02*10^{-7}\pm 5.9*10^{-8}$
HD 21019 A | HD 21019 A | $-0.00452\pm 0.00096$ | 0
HD 213519 | HD 213519 | $-0.00768\pm 0.00068$ | 0
HD 219834 B | HD 219834 B | $0.00531\pm 0.00036$ | 0
HD 23439 | HD 23439 | $0.00208\pm 0.00017$ | 0
HD 24040 | HD 24040 | $0.00581\pm 0.00044$ | $-6.6*10^{-7}\pm 1.2*10^{-7}$
HD 24496 | HIP 18267 | $-0.01997\pm 0.00036$ | 0
HD 24916 | HD 24916 | $-0.00386\pm 0.00067$ | 0
HD 3074 A | HD 3074 A | $-0.00977\pm 0.00066$ | 0
HD 32923 | HIP 23835 | $0.00513\pm 0.00046$ | 0
HD 34445 | HD 34445 | $-0.00328\pm 0.00043$ | 0
HD 34721 | HIP 24786 | $0.003\pm 0.00027$ | 0
HD 38230 | HIP 27207 | $0.01111\pm 0.00021$ | 0
HD 38 A | HD 38 A | $0.0039\pm 0.0012$ | 0
HD 38 B | HD 38 B | $-0.0072\pm 0.0012$ | 0
HD 39715 | HIP 27918 | $-0.0076\pm 0.001$ | $1.72*10^{-6}\pm 3.4*10^{-7}$
HD 40397 | HIP 28267 | $-0.02912\pm 0.00029$ | $-8.19*10^{-7}\pm 8.6*10^{-8}$
HD 45184 | HD 45184 | $-0.00111\pm 0.0002$ | 0
HD 4614 | HIP 3821 A | $0.02037\pm 0.00048$ | $-3.96*10^{-7}\pm 5.9*10^{-8}$
HD 4614 B | HIP 3821 B | $-0.02807\pm 0.00054$ | 0
HD 53665 | HD 53665 | $0.0104\pm 0.001$ | 0
HD 6101 | HIP 4849 A | $0.259\pm 0.022$ | 0
HD 63754 | HD 63754 | $-0.00599\pm 0.00069$ | $-6.1*10^{-7}\pm 1.6*10^{-7}$
HD 65277 | HIP 38931 | $-0.00573\pm 0.00019$ | 0
HD 6734 | HD 6734 | $-0.04096\pm 0.00069$ | $-4.54*10^{-6}\pm 1.5*10^{-7}$
HD 79210 | HIP 45343 | $0.01045\pm 0.00071$ | 0
HD 79211 | HIP 120005 | $-0.00965\pm 0.00087$ | 0
HD 8375 | HD 8375 | $0.66\pm 0.32$ | 0
HD 8648 | HIP 6653 | $0.02094\pm 0.0004$ | 0
HD 88986 | HD 88986 | $-0.00143\pm 0.00086$ | $1.78*10^{-6}\pm 1.9*10^{-7}$
HD 91204 | HD 91204 | $-0.3961\pm 0.0025$ | 0
HD 9540 A | HIP 7235 | $-0.00314\pm 0.00059$ | 0
HD 98618 | HD 98618 | $-0.0076\pm 0.00059$ | 0
GL 397 | GL 397 | $0.00574\pm 0.00089$ | 0
HIP 57050 | HIP 57050 | $0.0002\pm 0.0014$ | 0
HIP 71898 | HIP 71898 | $0.0213\pm 0.0012$ | 0
HD 71881 | HD 71881 | $-0.0314\pm 0.0012$ | 0
HD 88218 | HD 88218 | $-0.1164\pm 0.0022$ | $-4.59*10^{-6}\pm 4.3*10^{-7}$
HD 89391 | HD 89391 | $0.0116\pm 0.001$ | 0
HD 105618 | HD 105618 | $0.0064\pm 0.0015$ | 0
HD 111484 A | HD 111484 A | $-0.0862\pm 0.0054$ | 0
GL 528 B | GL 528 B | $0.0812\pm 0.003$ | 0
HD 120476 A | HD 120476 A | $-0.0708\pm 0.0011$ | $-3.18*10^{-6}\pm 3.8*10^{-7}$
HD 129814 | HD 129814 | $-0.0431\pm 0.0011$ | $2.73*10^{-5}\pm 3.5*10^{-7}$
HD 131509 | HD 131509 | $-0.01919\pm 0.00057$ | 0
HD 147231 | HD 147231 | $-0.0754\pm 0.001$ | 0
HD 151995 | HIP 82389 | $-0.00643\pm 0.00086$ | 0
HD 156826 | HD 156826 | $-0.0242\pm 0.00087$ | 0
HD 180684 | HD 180684 | $0.1709\pm 0.0019$ | $-6.73*10^{-6}\pm 5.8*10^{-7}$
HD 201203 | HD 201203 | $-0.1447\pm 0.0096$ | $-3.14*10^{-5}\pm 4.6*10^{-6}$
HD 183263 | HD 183263 | $-0.00659\pm 0.00044$ | 0

##  Appendix F Data

We include a sample table of RVs in Table 6.

Table 6: Sample of RV Data Name | Inst. | BJD - 2455000 |  $RV$ [m/s] |  $\sigma_{RV}$ [m/s] | S-Value
---|---|---|---|---|---
HD 156668 | HIRES pre-2004 | -2167.0766 | -0.45 | 1.62 | nan
HD 156668 | HIRES pre-2004 | -1925.896 | -7.47 | 1.68 | nan
HD 156668 | HIRES pre-2004 | -1803.1301 | -3.06 | 1.72 | nan
HD 156668 | HIRES post-2004 | -1521.0223 | -0.01 | 1.02 | 0.201
HD 156668 | HIRES post-2004 | -1452.0904 | -3.86 | 0.98 | 0.214
HD 156668 | HIRES post-2004 | -1395.1611 | -4.85 | 0.98 | 0.212
HD 156668 | HIRES post-2004 | -1192.8559 | 3.43 | 1.09 | 0.222
HD 156668 | HIRES post-2004 | -1067.0813 | 1.23 | 0.99 | 0.229
HD 156668 | HIRES post-2004 | -1039.086 | 3.95 | 0.92 | 0.22
HD 156668 | HIRES post-2004 | -1038.1904 | 0.36 | 0.95 | 0.219
HD 156668 | HIRES post-2004 | -1018.2294 | 3.12 | 0.88 | 0.231
HD 156668 | HIRES post-2004 | -1017.1234 | 1.06 | 0.93 | 0.233
HD 156668 | HIRES post-2004 | -1016.1809 | 6.45 | 0.87 | 0.23

##  Appendix G False Positives

We record all RVSearch-detected false positives in Table 7. The ’cause’ column
denotes why a signal was labeled as a false positive. ’A’ refers to a long-
period magnetic activity cycle, ’R’ refers to stellar rotation, and ’N’ refers
to an annual and/or instrumental systematic. Long-period instrumental
systematics are occasionally caused by offsets between dewars in the Lick
data. Several of these false positives correspond to reported planets in the
literature, or to stars that have been discussed extensively in the
literature. We elaborate on each of these cases in the subsections below.

Table 7: False Positives CPS Name | Lit. Name |  $P$ [d] |  $K$ [m s-1] | Cause
---|---|---|---|---
HD 103932 | HIP 58345 | $3660.0^{+190.0}_{-180.0}$ | $5.5^{+1.30}_{-0.98}$ | A
HD 10476 | HIP 7981 | $360.74^{+0.39}_{-0.64}$ | $2.84^{+0.59}_{-0.58}$ | N
HD 115617 | 61 Vir | $122.67^{+0.12}_{-0.14}$ | $1.94^{+0.30}_{-0.27}$ | N
HD 120467 | HIP 67487 | $66.464^{+0.056}_{-0.066}$ | $5.1^{+0.96}_{-0.82}$ | R
HD 122064 | HIP 68184 | $3100.0^{+310.0}_{-180.0}$ | $1.75^{+0.87}_{-0.39}$ | A
HD 136352 | HD 136352 | $244.5^{+1.5}_{-1.8}$ | $11.0^{+69.0}_{-3.3}$ | N
HD 136713 | HIP 75253 | $2710.0^{+140.0}_{-130.0}$ | $5.0^{+1.30}_{-0.88}$ | A
HD 136925 | HD 136925 | $311.2^{+0.55}_{-0.48}$ | $6.66^{+0.76}_{-0.73}$ | A
HD 139323 | HIP 76375 | $3310.0^{+110.0}_{-89.0}$ | $4.0^{+1.10}_{-0.97}$ | A
HD 140538 A | HD 140538 A | $1417.0^{+23.0}_{-25.0}$ | $4.73^{+0.70}_{-0.72}$ | A
HD 14412 | HIP 10798 | $364.0^{+1.5}_{-2.2}$ | $3.0^{+22.0}_{-1.1}$ | N
HD 144579 | HIP 78775 | $91.8^{+0.26}_{-0.34}$ | $2.17^{+0.58}_{-0.41}$ | N
HD 145675 | 14 Her | $3400.0^{+140.0}_{-240.0}$ | $3.52^{+1.10}_{-0.71}$ | A
HD 1461 | HD 1461 | $72.98^{+0.12}_{-0.10}$ | $1.33^{+0.25}_{-0.22}$ | N
HD 1461 | HD 1461 | $378.2^{+3.0}_{-2.2}$ | $3.8^{+1.3}_{-1.0}$ | A
HD 1461 | HD 1461 | $4060.0^{+280.0}_{-210.0}$ | $2.12^{+0.24}_{-0.24}$ | N
HD 146233 | HIP 79672 | $2426.0^{+60.0}_{-42.0}$ | $5.55^{+0.70}_{-0.67}$ | A
HD 154345 | HD 154345 | $2763.0^{+65.0}_{-69.0}$ | $5.5^{+1.10}_{-0.91}$ | A
HD 158633 | HIP 85235 | $367.5^{+1.2}_{-1.2}$ | $3.24^{+0.27}_{-0.26}$ | N
HD 161797 | HIP 86974 | $52.386^{+0.049}_{-0.049}$ | $1.69^{+0.32}_{-0.28}$ | R
HD 168009 | HIP 89474 | $368.57^{+1.00}_{-0.95}$ | $3.53^{+0.35}_{-0.32}$ | N
HD 168723 | HIP 89962 | $795.2^{+2.2}_{-11.0}$ | $8.1^{+2.3}_{-1.8}$ | N
HD 185144 | HIP 96100 | $2257.0^{+31.0}_{-30.0}$ | $1.97^{+0.13}_{-0.13}$ | A
HD 185144 | HIP 96100 | $347.11^{+0.92}_{-0.82}$ | $1.04^{+0.19}_{-0.18}$ | N
HD 18803 | HIP 14150 | $1960.0^{+36.0}_{-28.0}$ | $5.73^{+0.70}_{-0.66}$ | A
HD 190360 | HD 190360 | $90.34^{+0.11}_{-0.13}$ | $1.49^{+0.17}_{-0.18}$ | N
HD 190406 | HIP 98819 | $995.8^{+4.3}_{-4.3}$ | $8.22^{+0.73}_{-0.68}$ | A
HD 190406 | HIP 98819 | $4092.0^{+100.0}_{-73.0}$ | $9.1^{+1.2}_{-1.1}$ | A
HD 192310 | HD 192310 | $1630.0^{+51.0}_{-53.0}$ | $1.95^{+0.49}_{-0.36}$ | A
HD 193202 | HIP 99427 | $574.6^{+1.9}_{-6.7}$ | $3.8^{+0.48}_{-0.47}$ | N
HD 19373 | HIP 14632 | $367.5^{+1.90}_{-0.87}$ | $3.0^{+0.49}_{-0.45}$ | N
HD 195564 | HIP 101345 | $26000.0^{+16000.0}_{-11000.0}$ | $160.0^{+110.0}_{-120.0}$ | N
HD 197076 | HIP 102040 | $1620.0^{+29.0}_{-34.0}$ | $4.45^{+0.44}_{-0.42}$ | A
HD 197076 | HIP 102040 | $23.6803^{+0.0072}_{-0.0066}$ | $3.16^{+0.55}_{-0.49}$ | R
HD 199960 | HIP 103862 | $2357.0^{+65.0}_{-66.0}$ | $2.98^{+0.72}_{-0.48}$ | A
HD 201091 | HIP 104214 | $2571.0^{+55.0}_{-58.0}$ | $2.37^{+0.33}_{-0.32}$ | A
HD 201092 | HIP 104217 | $49.038^{+0.036}_{-0.032}$ | $1.73^{+0.26}_{-0.26}$ | R
HD 20165 | HIP 15099 | $2759.0^{+97.0}_{-91.0}$ | $4.56^{+0.57}_{-0.55}$ | A
HD 211080 | HIP 109836 | $677.6^{+7.2}_{-5.5}$ | $11.8^{+2.1}_{-1.8}$ | A
HD 213042 | HIP 110996 | $2530.0^{+210.0}_{-90.0}$ | $6.2^{+2.0}_{-1.4}$ | A
HD 214683 | HIP 111888 | $16.59^{+0.024}_{-0.540}$ | $33.0^{+120.0}_{-17.0}$ | R
HD 216520 | HIP 112527 | $181.63^{+0.64}_{-0.47}$ | $1.87^{+0.29}_{-0.29}$ | N
HD 216520 | HIP 112527 | $35.466^{+0.015}_{-0.016}$ | $2.42^{+0.27}_{-0.28}$ | R
HD 216520 | HIP 112527 | $5500.0^{+5100.0}_{-310.0}$ | $3.04^{+0.69}_{-0.46}$ | A
HD 217014 | 51 Peg | $100000.0^{+170000.0}_{-63000.0}$ | $10.0^{+280.0}_{-1.5}$ | N
HD 218868 | HIP 114456 | $1824.0^{+43.0}_{-56.0}$ | $7.3^{+1.6}_{-1.0}$ | A
HD 219134 | HD 219134 | $192.06^{+0.49}_{-0.40}$ | $2.0^{+0.21}_{-0.20}$ | N
HD 219134 | HD 219134 | $10230.0^{+830.0}_{-580.0}$ | $8.8^{+2.0}_{-1.7}$ | N
HD 219134 | HD 219134 | $364.3^{+1.9}_{-2.3}$ | $1.66^{+0.35}_{-0.31}$ | N
HD 22049 | eps Eri | $773.4^{+4.7}_{-4.8}$ | $4.1^{+0.70}_{-0.68}$ | N
HD 23439 | HD 23439 | $45.683^{+0.023}_{-0.022}$ | $2.63^{+0.40}_{-0.38}$ | R
HD 24496 | HIP 18267 | $182.13^{+0.87}_{-0.57}$ | $3.7^{+1.10}_{-0.68}$ | N
HD 26151 | HD 26151 | $113.57^{+0.13}_{-0.15}$ | $5.65^{+0.46}_{-0.46}$ | N
HD 26151 | HD 26151 | $32.879^{+0.015}_{-0.017}$ | $3.83^{+0.47}_{-0.49}$ | R
HD 26965 | HD 26965 | $42.305^{+0.015}_{-0.019}$ | $1.82^{+0.43}_{-0.31}$ | R
HD 26965 | HD 26965 | $3560.0^{+200.0}_{-580.0}$ | $1.89^{+0.37}_{-0.32}$ | A
HD 32147 | HD 32147 | $3444.0^{+91.0}_{-81.0}$ | $1.71^{+0.19}_{-0.18}$ | A
HD 32147 | HD 32147 | $51.997^{+0.078}_{-0.039}$ | $0.99^{+0.21}_{-0.19}$ | N
HD 34445 | HD 34445 | $214.74^{+0.49}_{-0.52}$ | $5.39^{+0.71}_{-0.69}$ | N
HD 34445 | HD 34445 | $117.69^{+0.16}_{-0.19}$ | $4.63^{+0.61}_{-0.58}$ | N
HD 34445 | HD 34445 | $49.231^{+0.048}_{-0.038}$ | $3.68^{+0.61}_{-0.53}$ | R
HD 36003 | HIP 23311 | $2790.0^{+140.0}_{-110.0}$ | $3.27^{+0.49}_{-0.46}$ | A
HD 3651 | HD 3651 | $5140.0^{+220.0}_{-290.0}$ | $2.45^{+0.97}_{-0.57}$ | A
HD 38858 | HD 38858 | $3113.0^{+82.0}_{-79.0}$ | $4.43^{+0.73}_{-0.64}$ | A
HD 42618 | HD 42618 | $4040.0^{+390.0}_{-260.0}$ | $2.72^{+0.27}_{-0.26}$ | A
HD 42618 | HD 42618 | $388.0^{+1.8}_{-2.2}$ | $1.64^{+0.28}_{-0.24}$ | N
HD 45184 | HD 45184 | $2479.0^{+110.0}_{-85.0}$ | $2.91^{+0.60}_{-0.56}$ | A
HD 4614 | HIP 3821 A | $91.011^{+0.093}_{-0.086}$ | $2.29^{+0.45}_{-0.39}$ | N
HD 4628 | HIP 3765 | $2468.0^{+16.0}_{-67.0}$ | $8.0^{+26.0}_{-5.2}$ | A
HD 48682 | HIP 32480 | $923.0^{+15.0}_{-28.0}$ | $4.1^{+0.84}_{-0.73}$ | A
HD 52265 | HD 52265 | $1383.0^{+25.0}_{-15.0}$ | $6.5^{+2.3}_{-1.2}$ | N
HD 52711 | HIP 34017 | $43000.0^{+140000.0}_{-27000.0}$ | $5.55^{+1.10}_{-0.74}$ | A
HD 55575 | HIP 35136 | $52.178^{+0.048}_{-0.045}$ | $2.6^{+0.37}_{-0.35}$ | R
HD 68988 | HD 68988 | $1922.0^{+49.0}_{-57.0}$ | $5.63^{+0.79}_{-0.74}$ | A
HD 69830 | HD 69830 | $200.61^{+0.68}_{-0.69}$ | $1.68^{+0.20}_{-0.21}$ | N
HD 69830 | HD 69830 | $381.8^{+4.9}_{-6.0}$ | $1.72^{+0.31}_{-0.25}$ | N
HD 75732 | 55 Cnc | $6110.0^{+280.0}_{-190.0}$ | $16.3^{+2.5}_{-2.9}$ | A
HD 75732 | 55 Cnc | $1966.0^{+23.0}_{-22.0}$ | $5.17^{+0.41}_{-0.36}$ | N
HD 7924 | HD 7924 | $24.4459^{+0.0090}_{-0.0091}$ | $1.59^{+0.18}_{-0.17}$ | A
HD 7924 | HD 7924 | $383.1^{+2.0}_{-1.8}$ | $1.69^{+0.27}_{-0.22}$ | N
HD 82943 | HD 82943 | $1078.0^{+15.0}_{-14.0}$ | $4.6^{+1.10}_{-0.94}$ | N
HD 9407 | HD 9407 | $121.91^{+0.140}_{-0.095}$ | $1.4^{+0.31}_{-0.25}$ | N
HD 9407 | HD 9407 | $178.62^{+0.46}_{-0.47}$ | $0.98^{+0.18}_{-0.17}$ | N
HD 95128 | 47 UMa | $18700.0^{+11000.0}_{-4000.0}$ | $12.4^{+1.4}_{-1.1}$ | N
HD 95128 | 47 UMa | $387.7^{+2.3}_{-2.0}$ | $2.34^{+0.37}_{-0.31}$ | N
HD 95735 | GJ 411 | $214.59^{+0.99}_{-0.64}$ | $1.45^{+0.42}_{-0.27}$ | N
HD 97101 | HD 97101 | $39.639^{+0.017}_{-0.019}$ | $3.39^{+0.29}_{-0.30}$ | R
HD 97101 | HD 97101 | $3080.0^{+170.0}_{-130.0}$ | $3.76^{+0.84}_{-0.64}$ | A
HD 97101 | HD 97101 | $19.6244^{+0.0064}_{-0.0064}$ | $1.71^{+0.30}_{-0.29}$ | R
HD 97658 | HD 97658 | $3660.0^{+170.0}_{-160.0}$ | $2.82^{+0.54}_{-0.54}$ | A
HD 9826 | ups And | $6290.0^{+140.0}_{-130.0}$ | $9.5^{+1.2}_{-1.2}$ | A
HD 9826 | ups And | $174.55^{+0.39}_{-0.34}$ | $5.07^{+0.93}_{-0.95}$ | N
HD 99491 | HIP 55846 | $2183.0^{+40.0}_{-37.0}$ | $6.49^{+0.62}_{-0.62}$ | A
HD 99492 | HD 99492 | $3680.0^{+190.0}_{-180.0}$ | $3.48^{+0.56}_{-0.54}$ | A
HD 9986 | HIP 7585 | $3103.0^{+51.0}_{-48.0}$ | $13.19^{+0.61}_{-0.62}$ | A
GL 388 | GL 388 | $2.068246^{+5.1e-05}_{-5.3e-05}$ | $27.6^{+5.6}_{-3.7}$ | R
GL 412 A | GL 412 A | $36.887^{+0.014}_{-0.017}$ | $3.14^{+0.81}_{-0.68}$ | R
GL 687 | GL 687 | $28.749^{+0.013}_{-0.012}$ | $2.92^{+0.51}_{-0.47}$ | N
HIP 42220 | HIP 42220 | $3600.0^{+2100.0}_{-770.0}$ | $41.0^{+50.0}_{-17.0}$ | N
HIP 74995 | HIP 74995 | $30.499^{+0.028}_{-0.021}$ | $2.71^{+0.51}_{-0.46}$ | R
GL 876 | GL 876 | $15.04336^{+0.00069}_{-0.00069}$ | $20.31^{+0.59}_{-0.59}$ | N
GL 876 | GL 876 | $10.014^{+0.0010}_{-0.0011}$ | $4.77^{+0.57}_{-0.59}$ | N

###  G.1 HD 115617

Vogt et al. (2010) reported three planets orbiting this star, with periods of
4.2, 38, and 124 days. RVSearch recovered signals at all three periods.
However, the 124 day signal (1/3rd of a year) has a strong harmonic at 1/4th
of a year, and there is significant residual power at roughly one year, as
seen in panels h and j of Figure 43. We investigated this candidate by
computing periodograms for the 12 HIRES PSF parameters computed for each RV
measurement, and found periodicity at 1 yr and harmonics of 1 yr for several
parameters, as seen in Figure 44. Additionally, several of these PSF
parameters correlate strongly with the corresponding RVs, after subtracting
the RV models of the two inner planets, as seen in Figure 45. Therefore, we
designated the 124 day signal as a yearly systematic.

Figure 43: RVSearch summary plot for HD 115617. See Figure 6 for plot
description. Note the nearly equivalent-height peaks at 1/3 and 1/4 year in
panel h, corresponding to the 124 day reported planet. Panel j shows that
there is residual power at 1 year after subtracting the 122 day signal,
suggesting the presence of yearly systematic noise in the data. Figure 44: PSF
Lomb–Scargle periodograms for HD 115617. Each panel corresponds to a Doppler
code PSF fitting parameter. Figure 45: PSF correlation plots for the candidate
HD 115617 d. Each panel corresponds to a Doppler code PSF fitting parameter,
with PSF value on the x-axis and RV without the signatures of the inner two
planets on the y-axis. Dashed blue lines are least-squares linear fits. R is
the Pearson correlation value; multiple PSF parameters have $|R|$ $>$ 0.15.

###  G.2 HD 154345

Here, we confirm the planetary status of the planet claim for HD 154345.
Wright et al. (2008) announced the detection of a true Jupiter analog, with
$M\sin{i}$ = 0.95 $M_{\textrm{J}}$ and an orbital period of 9.2 yr,
corresponding to an orbital separation of 4.2 AU. This paper also presented
strong evidence for a stellar magnetic activity cycle with a periodic
timescale of roughly nine years. As the CPS group continued to observe HD
154345 over the next few years, the planet candidate’s RV signature and the
corresponding S-values appeared to be strongly in phase, and Wright (2016)
noted that the candidate may be a false positive. However, in the twelve years
since HD 154345 b was initially reported, HIRES RV measurements and activity
metrics have drifted from being completely in phase to being completely out of
phase, as seen in Figure 46, and therefore are not linearly correlated. This
strongly implies that this Jupiter analog candidate cannot be attributed to
stellar activity, and that this candidate should be cemented as a confirmed
planet. RVSearch detects two signals in our HD 154345 dataset, both close to 9
yr, as seen in Figure 47. We attribute the circular orbit with a greater RV
amplitude to HD 154345 b, and the weak, eccentric signal to stellar activity.

Figure 46: HIRES post-upgrade RV and S-value activity timeseries for HD
154345. Note that the two datasets share minima and appear to be in phase when
post-upgrade observations began, but have drifted completely out of phase over
the following 23 years. Figure 47: RVSearch summary plot for HD 154345; see
Figure 6 for description. RVSearch first recovered a strong signal at 9 years,
but then recovered additional power at a similar period due to stellar
activity. The final orbit fit switched the two models, so that panels e) and
d) show the planetary signal, while panels c) and f) show the stellar activity
signal.

###  G.3 HD 26965

Ma et al. (2018) reported a 42.4 day super-Earth orbiting the nearby star HD
26965, using datasets taken by multiple spectrographs, including HIRES. We
detected significant periodicity at 42 days in the HIRES S-value measurements
as seen in Figure 48, and determined that 42 days is the likely stellar
rotation period of HD 26965. There is also evidence of a long-period magnetic
activity cycle, as seen in the juxtaposition of S-values and RVs in Figure 49.

Figure 48: Stellar rotation analysis of HIRES S-values for HD 26965. The top
panel shows a Lomb–Scargle periodogram of the S-values after we applied a
high-pass filter to them, to remove the impact of the long-period magnetic
activity cycle. The middle panel shows a periodogram of the raw S-values. The
top panel shows significant periodicity near 40 days, with a maximum at 41.6
days. The bottom-left panel shows the filtered S-values, while the bottom-
right panel shows the filtered S-values phased to 41.6 days; there appears to
be a coherent signal at this period, implying stellar rotation with this
period. Figure 49: HIRES post-upgrade S-values and RVs for HD 26965. The two
datasets both have long-period power and are in phase with each other.

###  G.4 HD 34445

Howard et al. (2010a) reported a giant planet orbiting this star at a period
of 1049 days. Vogt et al. (2017) reported five small planets, claiming
evidence in LCES-derived HIRES radial velocities. RVSearch detected the giant
planet and three of the five small planet claims, as seen in the summary plot
shown in Figure 50. The longest-period candidate among the five, not modeled
as a Keplerian here, clearly correlates with HIRES S-values; we model this
signal with a linear trend, for simplicity. Figure 51 juxtaposes the HIRES
S-values and corresponding RVs, minus the Keplerian signal of the system’s
giant planet. As for the three other periodic signals that we detect, two are
likely HIRES systematics and one is likely stellar rotation We detected
significant periodicity at 52 days in the HIRES S-value measurements as seen
in Figure 52, and determined that 52 days is the likely stellar rotation
period of HD 34445. This places our weak detection of the 49 day claimed
planet candidate under suspicion, and we have labeled it as a false positive
in our catalog. There is also evidence of semiannual HIRES systematics, as
seen in Figure 54, which shows the correlation between HIRES RVs minus the
giant planet signature and PSF parameters, and in Figure 53, which shows
periodograms of each PSF parameter time series. Multiple PSF parameters
correlate ($|R|$ $>$ 0.15) with the RV residuals, and multiple parameters show
periodicity around one-third and one-fourth of a year. The two claimed planets
at 118 and 215 days are close to one-third and one-half of a year,
respectively, and show weak and equal-strength signatures in their RVSearch
periodograms, as seen in Figure 50. Therefore, we have labeled these signals
as false positives in our catalog.

Figure 50: RVSearch summary plot for HD 34445; see Figure 6 for description.
RVSearch first recovered the known giant planet,  Figure 51: HIRES post-
upgrade RV and S-value activity timeseries for HD 34445, with the giant planet
RV model subtracted. Note that these two datasets share a negative long-term
trend, which we believe accounts for the claimed 5,700-day planet in the
system. Figure 52: Stellar rotation analysis of HIRES S-values for HD 34445.
The top panel shows a Lomb–Scargle periodogram of the S-values after we
applied a high-pass filter to them, to remove the impact of the long-period
magnetic activity cycle. The middle panel shows a periodogram of the raw
S-values. The top panel shows significant periodicity around 52.1 days. The
bottom-left panel shows the filtered S-values, while the bottom-right panel
shows the filtered S-values phased to 52.1 days; there appears to be a
coherent signal at this period, implying stellar rotation with this period.
This led us to label the 49 day claimed planet as a false positive, since
there is insufficient evidence to distinguish it from stellar rotation. Figure
53: PSF Lomb–Scargle periodograms for HD 34445. Each panel corresponds to a
Doppler code PSF fitting parameter. Figure 54: PSF correlation plots for HD
34445, without the RV signature of the star’s giant planet. Each panel
corresponds to a Doppler code PSF fitting parameter, with PSF value on the
x-axis and RV without the giant planet signature on the y-axis. Dashed blue
lines are least-squares linear fits. R is the Pearson correlation value;
multiple PSF parameters have $|R|$ $>$ 0.15.