11institutetext:  University Koblenz-Landau, Germany

# Symbol Elimination for Parametric Second-Order Entailment Problems
(with Applications to Problems in Wireless Network Theory)

Dennis Peuter  Philipp Marohn and Viorica Sofronie-Stokkermans

###### Abstract

We analyze possibilities of second-order quantifier elimination for formulae
containing parameters – constants or functions. For this, we use a constraint
resolution calculus obtained from specializing the hierarchical superposition
calculus. If saturation terminates, we analyze possibilities of obtaining
weakest constraints on parameters which guarantee satisfiability. If the
saturation does not terminate, we identify situations in which finite
representations of infinite saturated sets exist. We identify situations in
which entailment between formulae expressed using second-order quantification
can be effectively checked. We illustrate the ideas on a series of examples
from wireless network research.

##  1 Introduction

The main motivation for this work was a study of models for graph classes
naturally occurring in wireless network research – in which nodes that are
close are always connected, nodes that are far apart from each other are never
connected and any other node pairs can, but do not need to be connected.
Transformations can be applied to such graphs to make them symmetric; this way
we can define further graph classes. When checking inclusion between graph
classes described using transformations we need to check entailment of second-
order formulae. In addition, many such graph class descriptions are parametric
in nature, so the goal is, in fact, to obtain (weakest) conditions on the
parameters used in such descriptions that guarantee that graph classes are
non-empty or that inclusions hold. This can be achieved by eliminating “non-
parametric” constants or function symbols used in the description of such
classes.

In this paper we combine methods for general symbol elimination (which we use
for eliminating existentially quantified predicates) with methods for
property-directed symbol elimination (which we use for obtaining conditions on
“parameters” under which formulae are satisfiable or second-order entailment
holds). For general second-order quantifier elimination we use a form of
ordered resolution similar to that proposed in [18]. For property-directed
symbol elimination we use a method we proposed in [41]. The advantage of using
such a two-layered approach is that it avoids non-termination that might occur
if using only general symbol elimination methods. The main application area we
consider in this paper is the analysis of inclusions between graph classes
arising in wireless network research. Our main contributions are:

  * •

We analyze theories used in modeling graph classes and prove locality of
theories of “distances” occurring in this context.

  * •

We analyze possibilities of general symbol elimination, using a simple
specialization $\mathit{HRes}^{P}_{\succ}$ of the hierarchical superposition
calculus (a form of ordered resolution) for eliminating a predicate symbol
$P$.

  * •

If saturation terminates, we analyze possibilities of obtaining weakest
constraints on parameters occurring in the clauses which guarantee
satisfiability, using methods for property-directed symbol elimination.

  * •

If the saturation does not terminate, we study possibilities of representing
an (infinite) saturated set as a set of constrained clauses in which the
constraints are interpreted in the minimal model of a set of constrained Horn
clauses.

  * •

We analyze possibilities of effectively checking entailment between formulae
expressed using second-order quantification.

  * •

We illustrate the ideas on examples related to the study of wireless networks.

Related work. The study of second-order quantifier elimination goes back to
the beginning of the 20th century (cf. [10, 2, 3]). Most of its known
applications are in the study of modal logics or knowledge representation [19,
22]; in many cases second-order quantifier elimination is proved only for very
restricted fragments (cf. e.g. [43]). In [18], Gabbay and Ohlbach proposed a
resolution-based algorithm for second-order quantifier elimination which is
implemented in the system SCAN. In [5], Bachmair et al. mention that
hierarchical superposition (cf. [8, 9] for further refinements) can be used
for second-order quantifier elimination modulo a theory. In [34, 24], Hoder et
al. study possibilities of symbol elimination in inference systems (e.g. the
superposition calculus and its extension with ground linear rational
arithmetic and uninterpreted functions). The main challenge when using
saturation approaches for symbol elimination is the fact that the saturated
sets might be infinite. Sometimes finite representations of possibly infinite
sets of clauses exist: for this, Horbach and Weidenbach introduced a melting
calculus [27], later used in [25, 26] and [16]. Similar aspects were explored
in the study of acceleration for program verification modulo Presburger
arithmetic by Boigelot, Finkel and Leroux [14, 17], in relationship with array
systems by [4], or in the study of constrained Horn clauses (cf. e.g. the
survey [12]).

Orthogonal to this direction of study is what we call “property-directed”
symbol elimination: There, given a theory ${\mathcal{T}}$ and a ground formula
$G$ satisfiable w.r.t. ${\mathcal{T}}$, the goal is to derive a (weakest)
universal formula $\Gamma$ over a subset of the signature, such that
$\Gamma\wedge G$ is unsatisfiable w.r.t. ${\mathcal{T}}$. We devised methods
for solving such problems in [41] and used them for interpolant computation
[41], and invariant generation [36].

We are not aware of other similar approaches to the area of computational
(geometric) graph theory. Existing approaches use a logical representation of
graphs based on monadic second-order logic (cf. e.g. [15]) or higher-order
theorem provers like Isabelle/HOL (cf. e.g. [1]). Our approach is orthogonal;
it allows a reduction of many problems to satisfiability modulo a suitable
theory.

Structure of the paper. In Section 2 we present the motivation for our
research. In Section 3 we introduce the notions on (local) theory extensions
needed in the paper and prove the locality of theories of distance functions.
In Section 4 we describe (and slightly extend) a method for property-directed
symbol elimination we proposed in [41]. In Section 5 we present the
$\mathit{HRes}^{P}_{\succ}$ calculus we use for eliminating predicate $P$, and
analyze possibilities of giving finite representations for infinite saturated
sets and of investigating the satisfiability of the saturated sets. In Section
6 we use these ideas for checking class inclusion. In Section 7 we discuss the
way in which we tested the methods we propose on various examples. In Section
8 we present conclusions and plans for future work.

This paper is an extended version of [37] which contains full proofs of the
results, a more detailed description of the examples, a description of the
systems we used for testing and several examples illustrating how these
systems were used.

Table of Contents

section.1.1 section.1.2 section.1.3 subsection.1.3.1 subsection.1.3.2
section.1.4 section.1.5 subsection.1.5.1 subsection.1.5.2 section.1.6
section.1.6.1 section.1.7 section.1.8 section.A.1 subsection.A.1.1
subsection.A.1.2 subsection.A.1.3 section.A.2 section.A.3

##  2 Motivation

Graph Classes. Graph classes important in wireless network research are: The
class ${\bf UDG}$ of _unit disk graphs_ (two nodes are connected iff they are
different and their distance is $\leq 1$); the class ${\bf QUDG}(r)$ of quasi
unit disk graphs, for $r\in(0,1]$ (two distinct nodes with distance $\leq r$
are always connected and nodes with distance $>1$ are never connected); the
class ${\bf DTG}(\mathbf{r},r)$ of directed transmission graphs for $r>0$
(every node $v$ has a maximum communication distance ${\mathbf{r}}(v)\leq r$;
an edge from $v$ to $w$ exists iff $v\neq w$ and the distance between $v$ and
$w$ is $\leq{\mathbf{r}}(v)$).

Many graph classes ${\bf C}({\overline{p}})$ (where ${\overline{p}}$ is a
sequence of symbols denoting parameters) can be described using inclusion,
exclusion and transfer axioms.

The inclusion axioms specify which edges have to exist. For a graph class
${\bf C}$ the condition under which an edge $E(u,v)$ must exist can be
described by a formula $\pi_{C}^{i}(u,v)$. Therefore, inclusion axioms have
the form:

$(1)\quad\quad\forall u,v~{}(\pi_{C}^{i}(u,v)\rightarrow E(u,v))$

The exclusion axioms specify which edges are not allowed to exist. For a class
${\bf C}$ the condition under which an edge $E(u,v)$ is not allowed to exist
can be described by a formula $\pi_{C}^{e}(u,v)$. Therefore, transfer axioms
have the form:

$(2)\quad\quad\forall u,v~{}(\pi_{C}^{e}(u,v)\rightarrow\lnot E(u,v))$

The transfer axioms specify which edges $E(u,w)$ must exist as a consequence
of the existence of another edge $E(u,v)$. For a class ${\bf C}$, we describe
these these conditions by a formula $\pi_{C}^{t}(u,v,w)$. Therefore, inclusion
axioms have the form:

$(3)\quad\quad\forall u,v,w~{}\pi_{C}^{t}(u,w,v)\land E(u,v)\rightarrow
E(u,w)$.

If the description of the graph class ${\bf C}$ depends on parameters
${\overline{p}}$, the formulae $\pi_{C}^{i},\pi_{C}^{e}$ and $\pi_{C}^{t}$
might contain parameters. We will sometimes indicate this by adding the
parameters to the arguments, i.e. writing
$\pi_{C}^{i}(u,v,{\overline{p}}),\pi_{C}^{e}(u,v,{\overline{p}})$ resp.
$\pi_{C}^{t}(u,v,w,{\overline{p}})$.

We can, e.g., define the classes ${\bf MinDG}(r)$, ${\bf MaxDG}(r)$ and ${\bf
CRG}$ using axioms:

  * •

${\sf MinDG}(r)$: axiom $(1)$, where $\pi^{i}(u,v,r)$ is the formula $u\neq
v\land d(u,v)\leq r$;

  * •

${\sf MaxDG}(r)$: axiom $(2)$, where $\pi^{e}(u,v,r)$ is the formula
$d(u,v)>r$;

  * •

${\sf CRG}$: axiom $(3)$, where $\pi^{t}(u,w,v)$ is the formula $u\neq w\land
d(u,w)\leq d(u,v)$,

(where $r$ is supposed to be a parameter).

With this notation, the inclusion axiom ${\sf MinDG}(r)$ states that if $u\neq
v$ and $d(u,v)\leq r$ an edge from $u$ to $v$ must exist; the exclusion axiom
${\sf MaxDG}(r)$ states that if $d(u,v)>r$ then we are not allowed to have an
edge from $u$ to $v$. The transfer axiom ${\sf CRG}$ states that if $u$ and
$w$ are different and there is an edge from $u$ to $v$ and $d(u,w)\leq d(u,v)$
then there must exist an edge also from $u$ to $w$.

By combining such axioms we obtain axiomatizations for new graph classes. If
the classes ${\bf A}$ and ${\bf B}$ of graphs are axiomatized by axioms ${\sf
Ax_{A}}$ and ${\sf Ax_{B}}$ then ${\sf Ax_{A}}\wedge{\sf Ax_{B}}$ is an
axiomatization for the intersection ${\bf A}\cap{\bf B}$.
For instance, the class ${\bf UDG}={\bf MinDG}(1)\cap{\bf MaxDG}(1)$ is
axiomatized by ${\sf MinDG}(1)\wedge{\sf MaxDG}(1)$.

We may want to check whether a graph class ${\bf C}({\overline{p}})$ has non-
empty models, or to determine (weakest) conditions on the parameters
${\overline{p}}$ under which this is the case. This is one of the problems
which will be analyzed in this paper.

Simple transformations on graph classes. We can define transformations
$\gamma$ on graphs that transform the edges and leave the set of vertices
unchanged, and form graph classes

$\gamma({\bf C})=\\{\gamma(G)\mid G\in{\bf C}\\}.$

Two examples of transformations are $\cdot^{+}$ and $\cdot^{-}$: Given a graph
$G=(V,E)$, we can build the symmetric supergraph $G^{+}=(V,E^{+})$ resp.
symmetric subgraph $G^{-}=(V,E^{-})$, defined by:

$\begin{array}[]{l}\forall x,y~{}(E^{+}(x,y)\leftrightarrow(E(x,y)\lor
E(y,x)))\\\ \forall x,y~{}(E^{-}(x,y)\leftrightarrow(E(x,y)\land
E(y,x))).\end{array}$

We can thus define the classes ${\bf C}^{+}=\\{G^{+}\mid G\in{\bf C}\\}$ and
${\bf C}^{-}=\\{G^{-}\mid G\in{\bf C}\\}$.

The class of quasi unit disk graphs [7, 35] can, for instance, be described as

${\bf QUDG}(r)=({\bf MinDG}(r)\cap{\bf MaxDG}(1))^{-}.$

We might want to obtain an axiomatization for ${\bf QUDG}(r)$ that depends
only on the predicates $\pi^{i}(x,y,r),\pi^{e}(x,y,1)$ or test whether the
class is the same as the class described by $({\bf MinDG}(r)\cap{\bf
MaxDG}(1))^{+}$.

To find an axiomatization of a graph class $\gamma({\bf C})$, where $\gamma$
is a transformation, we need to find a first-order formula equivalent to
$\exists E^{\prime}({\sf N}_{E^{\prime}}\cap{\sf Tr}(E^{\prime},E)),$ where
${\sf N}_{E^{\prime}}$ is a class of clauses describing class ${\bf C}$ and
${\sf Tr}$ is a formula describing the way the edges of the graph
$(V,E)=\gamma(V,E^{\prime})$ can be obtained from the description of the graph
$(V,E^{\prime})$. We here analyze possibilities of eliminating second-order
quantifiers.

Checking class inclusion. If we can find such formulae for two graph classes,
then we can also check containment (provided the formulae belong to decidable
theory fragments). In this paper we analyze situations in which this is
possible.

##  3 Theories and local theory extensions

We assume known the basic notions in (many-sorted) first-order logic. We
consider signatures of the form $\Pi=(S,\Sigma,{\sf Pred})$, where $S$ is a
set of sorts, $\Sigma$ is a family of function symbols and ${\sf Pred}$ a
family of predicate symbols, such that for every function symbol $f$ (resp.
predicate symbol $p$) their arity $a(f)=s_{1}\dots s_{n}\rightarrow s$ (resp.
$a(p)=s_{1}\dots s_{m}$), where $s_{1},\dots,s_{n},s\in S$, is specified. If
$C$ is a fixed countable set of fresh constants, we denote by $\Pi^{C}$ the
extension of $\Pi$ with constants in $C$. We assume known standard definitions
from first-order logic such as $\Pi$-structure, model, satisfiability,
unsatisfiability. A $\Pi$-structure is a tuple

${\mathcal{A}}=(\\{A_{s}\\}_{s\in
S},\\{f_{\mathcal{A}}\\}_{f\in\Sigma},\\{p_{\mathcal{A}}\\}_{p\in{\sf
Pred}}),$

where, for every $s\in S$, $A_{s}$ is a non-empty set (the universe of sort
$s$ of the structure), for every $f\in\Sigma$ with arity $s_{1}\dots
s_{n}\rightarrow s$, $f_{\mathcal{A}}:A_{s_{1}}\times\dots\times
A_{s_{n}}\rightarrow A_{s}$, and for every $p\in{\sf Pred}$ with arity
$s_{1}\dots s_{m}$, $p_{\mathcal{A}}\subseteq A_{s_{1}}\times\dots\times
A_{s_{m}}$.

If $\mathcal{A}$ is a $\Pi$-structure, we will denote by $\mathcal{A}^{A}$ the
extension of $\mathcal{A}$, where we have an additional constant (of sort $s$)
for each element $a$ of sort $s$ of $\mathcal{A}$ (which we denote with the
same symbol) with the natural interpretation mapping the constant $a$ to the
element $a$ of $\mathcal{A}$.

If $\Pi\subseteq\Pi^{\prime}$ and $\mathcal{A}$ is a $\Pi^{\prime}$-structure,
we denote its reduct to $\Pi$ by $\mathcal{A}_{|\Pi}$.

Notation. We will denote with (indexed versions of) $x,y,z$ variables and with
(indexed versions of) $a,b,c,d$ constants; ${\overline{x}}$ will stand for a
sequence of variables $x_{1},\dots,x_{n}$, and ${\overline{c}}$ for a sequence
of constants $c_{1},\dots,c_{n}$.

Theories. Theories can be defined by specifying a set of axioms, or by
specifying a class of structures (the models of the theory). If $F$ and $G$
are formulae we write $F\models G$ (resp. $F\models_{\cal T}G$ – also written
as ${\cal T}\cup F\models G$) to express the fact that every model of $F$
(resp. every model of $F$ which is also a model of ${\mathcal{T}}$) is a model
of $G$. We denote “falsum” with $\perp$. $F\models\perp$ means that $F$ is
unsatisfiable; $F\models_{{\mathcal{T}}}\perp$ means that there is no model of
${\mathcal{T}}$ in which $F$ is true.

A theory ${\mathcal{T}}$ over a signature $\Pi$ allows quantifier elimination
(QE) if for every formula $\phi$ over $\Pi$ there exists a quantifier-free
formula $\phi^{*}$ over $\Pi$ which is equivalent to $\phi$ modulo
${\mathcal{T}}$. Examples of theories which allow quantifier elimination are
rational and real linear arithmetic (${\sf LI}({\mathbb{Q}})$, ${\sf
LI}({\mathbb{R}})$), the theory of real closed fields, and the theory of
absolutely-free data structures.

Sometimes, in order to define more complex theories we can consider theory
extensions and combinations thereof. Local theory extensions are a class of
theory extensions for which hierarchical reasoning is possible.

###  3.1 Local theory extensions

In what follows, for simplicity we present the main notions in the one-sorted
case; the extension to the many-sorted case is immediate.

Let $\Pi_{0}{=}(\Sigma_{0},{\sf Pred})$ be a signature, and
${\mathcal{T}}_{0}$ be a “base” theory with signature $\Pi_{0}$. We consider
extensions ${\mathcal{T}}:={\mathcal{T}}_{0}\cup{\mathcal{K}}$ of
${\mathcal{T}}_{0}$ with new function symbols $\Sigma$ (extension functions)
whose properties are axiomatized using a set ${\mathcal{K}}$ of (universally
closed) clauses in the extended signature $\Pi=(\Sigma_{0}\cup\Sigma,{\sf
Pred})$, such that each clause in ${\mathcal{K}}$ contains function symbols in
$\Sigma$. Especially well-behaved are the $\Psi$-local theory extensions, i.e.
theory extensions
${\mathcal{T}}_{0}\subseteq{\mathcal{T}}_{0}\cup{\mathcal{K}}$ as defined
above, in which checking ground satisfiability can be done using a finite
instantiation scheme described by a suitable closure operator $\Psi$, without
loss of completeness. We express this with the following condition:

${\sf(Loc}^{\Psi}_{f})$ | For every finite set $G$ of ground $\Pi^{C}$-clauses (for an additional
---|---
| set $C$ of constants) it holds that ${\mathcal{T}}_{0}\cup{\mathcal{K}}\cup
G\models\bot$ if and only if
|  ${\mathcal{T}}_{0}\cup{\mathcal{K}}[\Psi_{\mathcal{K}}(G)]\cup G$ is
unsatisfiable.

where, for every set $G$ of ground $\Pi^{C}$-clauses,
${\mathcal{K}}[\Psi_{\mathcal{K}}(G)]$ is the set of instances of
${\mathcal{K}}$ in which the terms starting with a function symbol in $\Sigma$
are in $\Psi_{{\mathcal{K}}}(G)=\Psi({\sf est}({\mathcal{K}},G))$, where ${\sf
est}({\mathcal{K}},G)$ is the set of ground terms starting with a function in
$\Sigma$ occurring in $G$ or ${\mathcal{K}}$.

If ${\mathcal{T}}_{0}$ is the pure theory of equality, we obtain the notion of
locality [21, 20].

Partial and total models. In [38] we showed that local theory extensions can
be recognized by showing that certain partial models embed into total ones,
and in [30] we established similar results for $\Psi$-local theory extensions
and generalizations thereof. We introduce the main definitions here, following
mainly the presentation from [30] and [42].

Let $\Pi=(\Sigma,{\sf Pred})$ be a first-order signature with set of function
symbols $\Sigma$ and set of predicate symbols ${\sf Pred}$. A _partial
$\Pi$-structure_ is a structure
$\mathcal{A}=(A,\\{f_{\mathcal{A}}\\}_{f\in\Sigma},\\{p_{\mathcal{A}}\\}_{p\in{\sf
Pred}})$, where $A$ is a non-empty set, for every $n$-ary $f\in\Sigma$,
$f_{\mathcal{A}}$ is a partial function from $A^{n}$ to $A$, and for every
$n$-ary $p\in{\sf Pred}$, $p_{\mathcal{A}}\subseteq A^{n}$. We consider
constants (0-ary functions) to be always defined. $\mathcal{A}$ is called a
_total structure_ if the functions $f_{\mathcal{A}}$ are all total. Given a
(total or partial) $\Pi$-structure $\mathcal{A}$ and $\Pi_{0}\subseteq\Pi$ we
denote the reduct of $\mathcal{A}$ to $\Pi_{0}$ by $\mathcal{A}{|_{\Pi_{0}}}$.

The notion of evaluating a term $t$ with variables $X$ w.r.t. an assignment
$\beta:X\rightarrow A$ for its variables in a partial structure $\mathcal{A}$
is the same as for total algebras, except that the evaluation is undefined if
$t=f(t_{1},\ldots,t_{n})$ and at least one of $\beta(t_{i})$ is undefined, or
else $(\beta(t_{1}),\ldots,\beta(t_{n}))$ is not in the domain of
$f_{\mathcal{A}}$.

###### Definition 1

A _weak $\Pi$-embedding_ between two partial $\Pi$-structures $\mathcal{A}$
and $\mathcal{B}$, where
$\mathcal{A}=(A,\\{f_{\mathcal{A}}\\}_{f\in\Sigma},\\{p_{\mathcal{A}}\\}_{p\in{\sf
Pred}})$ and
$\mathcal{B}=(B,\\{f_{\mathcal{B}}\\}_{f\in\Sigma},\\{p_{\mathcal{B}}\\}_{p\in{\sf
Pred}})$ is a total map $\varphi:A\rightarrow B$ such that

  1. (i)

$\varphi$ is an embedding w.r.t. ${\sf Pred}\cup\\{=\\}$, i.e. for every
$p\in{\sf Pred}$ with arity $n$ and every $a_{1},\dots,a_{n}\in\mathcal{A}$,
$(a_{1},\dots,a_{n})\,{\in}\,p_{\mathcal{A}}$ if and only if
$(\varphi(a_{1}),\dots,\varphi(a_{n}))\,{\in}\,p_{\mathcal{B}}$.

  2. (ii)

whenever $f_{\mathcal{A}}(a_{1},\dots,a_{n})$ is defined (in $\mathcal{A}$),
then $f_{\mathcal{B}}(\varphi(a_{1}),\dots,\varphi(a_{n}))$ is defined (in
$\mathcal{B}$) and
$\varphi(f_{\mathcal{A}}(a_{1},\dots,a_{n}))=f_{\mathcal{B}}(\varphi(a_{1}),\dots,\varphi(a_{n}))$,
for all $f\in\Sigma$.

######  Definition 2 (Weak validity)

Let $\mathcal{A}$ be a partial $\Pi$-algebra and $\beta:X{\rightarrow}A$ a
valuation for its variables. $(\mathcal{A},\beta)$ weakly satisfies a clause
$C$ (notation: $(\mathcal{A},\beta)\models_{w}C$) if either some of the
literals in $\beta(C)$ are not defined or otherwise all literals are defined
and for at least one literal $L$ in $C$, $L$ is true in $\mathcal{A}$ w.r.t.
$\beta$. $\mathcal{A}$ is a weak partial model of a set of clauses
${\mathcal{K}}$ if $(\mathcal{A},\beta)\models_{w}C$ for every valuation
$\beta$ and every clause $C$ in ${\mathcal{K}}$.

Recognizing $\Psi$-local theory extensions. In [38] we proved that if every
weak partial model of an extension ${\mathcal{T}}_{0}\cup{\mathcal{K}}$ of a
base theory ${\mathcal{T}}_{0}$ with total base functions can be embedded into
a total model of the extension, then the extension is local. In [28] we lifted
these results to $\Psi$-locality.

Let $\mathcal{A}=(A,\\{f_{\mathcal{A}}\\}_{f\in\Sigma_{0}\cup\Sigma}\cup
C,\\{p_{\mathcal{A}}\\}_{p\in{\sf Pred}})$ be a partial $\Pi^{C}$-structure
with total $\Sigma_{0}$-functions. Let $\Pi^{A}$ be the extension of the
signature $\Pi$ with constants from $A$. We denote by $T(\mathcal{A})$ the
following set of ground $\Pi^{A}$-terms:

$T(\mathcal{A}):=\\{f(a_{1},...,a_{n})\,|\;f\in\Sigma,a_{i}\in
A,i=1,\dots,n,f_{\mathcal{A}}(a_{1},...,a_{n})\text{ is defined }\\}.$

Let ${\sf PMod}_{w,f}^{\Psi}({\Sigma},{\mathcal{T}})$ be the class of all weak
partial models $\mathcal{A}$ of ${\mathcal{T}}_{0}\cup{\mathcal{K}}$, such
that $\mathcal{A}{|_{\Pi_{0}}}$ is a total model of ${\mathcal{T}}_{0}$, the
$\Sigma$-functions are possibly partial, $T(\mathcal{A})$ is finite and all
terms in $\Psi({\sf est}({\mathcal{K}},T(\mathcal{A})))$ are defined (in the
extension $\mathcal{A}^{A}$ with constants from $A$). We consider the
following embeddability property of partial algebras:

$({\sf Emb}_{w,f}^{\Psi})$ | Every $\mathcal{A}\in{\sf PMod}_{w,f}^{\Psi}({\Sigma},{\mathcal{T}})$ weakly embeds into a total model of ${\mathcal{T}}$.
---|---

We also consider the property $({\sf EEmb}_{w,f}^{\Psi})$, which additionally
requires the embedding to be elementary, and the property $({\sf
Comp}^{\Psi}_{f})$, which requires that every structure $\mathcal{A}\in{\sf
PMod}_{w,f}^{\Psi}({\Sigma},{\mathcal{T}})$ embeds into a total model of
${\mathcal{T}}$ with the same support. If $\Psi$ is the identity, we refer to
these properties as $({\sf Emb}_{w,f})$, $({\sf EEmb}_{w,f})$ and ${\sf
Comp}_{f}$.

When establishing links between locality and embeddability we require that the
clauses in ${\mathcal{K}}$ are _flat_ and _linear_ w.r.t. $\Sigma$-functions.
When defining these notions we distinguish between ground and non-ground
clauses.

###### Definition 3

An extension clause $D$ is flat (resp. _quasi-flat_) when all symbols below a
$\Sigma$-function symbol in $D$ are variables (resp. variables or ground
$\Pi_{0}$-terms). $D$ is _linear_ if whenever a variable occurs in two terms
of $D$ starting with $\Sigma$-functions, the terms are equal, and no term
contains two occurrences of a variable.

A ground clause $D$ is flat if all symbols below a $\Sigma$-function in $D$
are constants. A ground clause $D$ is linear if whenever a constant occurs in
two terms in $D$ whose root symbol is in $\Sigma$, the two terms are
identical, and no term which starts with a $\Sigma$-function contains two
occurrences of the same constant.

######  Definition 4 ([30])

With the above notations, let $\Psi$ be a map associating with ${\mathcal{K}}$
and a set of $\Pi^{C}$-ground terms $T$ a set $\Psi_{{\mathcal{K}}}(T)$ of
$\Pi^{C}$-ground terms. We call $\Psi_{{\mathcal{K}}}$ a _term closure
operator_ if the following holds for all sets of ground terms $T,T^{\prime}$:

  1. (1)

$\mathrm{est}({\mathcal{K}},T)\subseteq\Psi_{{\mathcal{K}}}(T)$,

  2. (2)

$T\subseteq
T^{\prime}\Rightarrow\Psi_{{\mathcal{K}}}(T)\subseteq\Psi_{{\mathcal{K}}}(T^{\prime})$,

  3. (3)

$\Psi_{{\mathcal{K}}}(\Psi_{{\mathcal{K}}}(T))\subseteq\Psi_{{\mathcal{K}}}(T)$,

  4. (4)

for any map $h:C\rightarrow C$,
$\bar{h}(\Psi_{{\mathcal{K}}}(T))=\Psi_{\bar{h}{\mathcal{K}}}(\bar{h}(T))$,
where $\bar{h}$ is the canonical extension of $h$ to extension ground terms.

######  Theorem 1 ([28, 30])

Let ${\mathcal{T}}_{0}$ be a first-order theory and ${\mathcal{K}}$ a set of
universally closed flat clauses in the signature $\Pi$. The following hold:

  1. (1)

If all clauses in ${\mathcal{K}}$ are linear and $\Psi$ is a term closure
operator with the property that for every flat set of ground terms $T$,
$\Psi(T)$ is flat then either of the conditions $({\sf Emb}_{w,f}^{\Psi})$ and
$({\sf EEmb}_{w,f}^{\Psi})$ implies $({\sf Loc}_{f}^{\Psi})$.

  2. (2)

If the extension
${\mathcal{T}}_{0}\subseteq{\mathcal{T}}{=}{\mathcal{T}}_{0}{\cup}{\mathcal{K}}$
satisfies $({\sf Loc}_{f}^{\Psi})$ then $({\sf Emb}_{w,f}^{\Psi})$ holds.

The linearity assumption needed to prove that $({\sf Emb}_{w,f}^{\Psi})$
implies $({\sf Loc}_{f}^{\Psi})$ can be relaxed if the closure operator $\Psi$
has additional properties.

###### Theorem 2

Let ${\mathcal{K}}$ be a set of $\Sigma$-flat clauses, with the property that
every variable occurs only once in every term. Let $\Psi$ be a term closure
operator with the property that for every flat set of ground terms $T$,
$\Psi(T)$ is flat.

Assume that ${\mathcal{K}}$ and $\Psi$ have the property that for every flat
set of ground terms $T$ and for every clause $C\in{\mathcal{K}}$, if $C$
contains terms $f(x_{1},\dots,x,\dots,x_{n})$ and
$g(y_{1},\dots,x,\dots,y_{m})$ (where $f,g\in\Sigma$ are extension functions
and $f$ and $g$ are not necessarily different), if
$f(t_{1},\dots,t,\dots,t_{n}),g(s_{1},\dots,s,\dots,s_{m})\in\Psi_{{\mathcal{K}}}(T)$
then
$f(t_{1},\dots,s,\dots,t_{n}),g(s_{1},\dots,t,\dots,s_{m})\in\Psi_{{\mathcal{K}}}(T)$.
Then $({\sf Emb}_{w,f}^{\Psi})$ implies $({\sf Loc}_{f}^{\Psi})$.

Proof: The proof is included in Appendix 0.B.111A similar result can be proved
also in the case in which some variables occur several times below a function
symbol if $\Psi_{{\mathcal{K}}}$ has the property that if
$f(x_{1},\dots,x,\dots,x,\dots x_{n})\in{\mathcal{K}}$ and
$f(t_{1},\dots,s,\dots,t,\dots,t_{n})\in\Psi_{{\mathcal{K}}}(T)$ then
$f(t_{1},\dots,t,\dots,t,\dots,t_{n})\in\Psi_{{\mathcal{K}}}(T)$ and
$f(t_{1},\dots,s,\dots,s,\dots,t_{n})\in\Psi_{{\mathcal{K}}}(T)$. $\Box$

######  Theorem 3 ([39, 28])

The following theory extensions have property $({\sf Comp}_{f})$, hence are
local:

  * (i)

The extension of a theory ${\mathcal{T}}_{0}$ with uninterpreted function
symbols.

  * (ii)

The extension of a theory ${\mathcal{T}}_{0}$ containing a predicate $\leq$
which is reflexive with a function $f$ satisfying the axioms
${\mathcal{K}}=\\{\forall{\overline{x}}~{}\phi_{i}({\overline{x}}){\rightarrow}L_{i}({\overline{x}})\mid
i=1,\dots,n\\},$ where:

    * –

$\phi_{i}$ are ${\mathcal{T}}_{0}$-formulae with
$\phi_{i}({\overline{x}}){\wedge}\phi_{j}({\overline{x}}){\models}{\perp}$ if
$i{\neq}j$
($n$ can be 1 and $\phi_{1}$ can be $\top$),

    * –

$L_{i}({\overline{x}})$ has the form (1) $s_{i}\leq f({\overline{x}})$ or (2)
$f({\overline{x}})\leq t_{i}$ or (3) $s_{i}\leq f({\overline{x}})\leq t_{i}$,
where $s_{i},t_{i}$ are $\Pi_{0}$-terms and in case (3)
$\phi_{i}\models_{{\mathcal{T}}_{0}}s_{i}\leq t_{i}$.

Hierarchical reasoning. Consider a $\Psi$-local theory extension
${\mathcal{T}}_{0}\subseteq{\mathcal{T}}_{0}\cup{\mathcal{K}}$. Condition
$({\sf Loc}_{f}^{\Psi})$ requires that for every finite set $G$ of ground
$\Pi^{C}$-clauses, ${\mathcal{T}}_{0}\cup{\cal K}\cup G\models\perp$ iff
${\mathcal{T}}_{0}\cup{\mathcal{K}}[\Psi_{\cal K}(G)]\cup G\models\perp$. In
all clauses in ${\mathcal{K}}[\Psi_{\cal K}(G)]\cup G$ the function symbols in
$\Sigma$ only have ground terms as arguments, so ${\mathcal{K}}[\Psi_{\cal
K}(G)]{\cup}G$ can be flattened and purified. We thus obtain a set of clauses
${\mathcal{K}}_{0}\cup G_{0}\cup{\sf Def}$, where ${\mathcal{K}}_{0}$ and
$G_{0}$ do not contain $\Sigma$-function symbols and ${\sf Def}$ contains
clauses of the form $c=f(c_{1},\dots,c_{n})$, where $f\in\Sigma$, and
$c,c_{1},\dots,c_{n}$ are constants. This transformation allows us to reduce
testing satisfiability w.r.t. ${\mathcal{T}}_{0}\cup{\mathcal{K}}$ to testing
satisfiability w.r.t. ${\mathcal{T}}_{0}$.

######  Theorem 4 ([38])

Let ${\mathcal{K}}$ be a set of clauses. Assume that
${\mathcal{T}}_{0}\subseteq{\cal T}_{1}={\mathcal{T}}_{0}\cup{\mathcal{K}}$ is
a $\Psi$-local theory extension. For any finite set $G$ of ground
$\Pi^{C}$-clauses, let ${\mathcal{K}}_{0}\cup G_{0}\cup{\sf Def}$ be obtained
from ${\mathcal{K}}[\Psi_{\cal K}(G)]\cup G$ by introducing, in a bottom-up
manner, new constants $c_{t}\in C$ for subterms $t{=}f(c_{1},\dots,c_{n})$
where $f{\in}\Sigma$ and $c_{i}$ are constants, together with definitions
$c_{t}{=}f(c_{1},\dots,c_{n})$ (included in ${\sf Def}$) and replacing the
corresponding terms $t$ with the constants $c_{t}$ in ${\mathcal{K}}$ and $G$.
Then ${\cal T}_{1}\cup G\models\perp$ if and only if
${\mathcal{T}}_{0}\cup{\mathcal{K}}_{0}\cup G_{0}\cup{\sf
Con}_{0}\models\perp,$ where $\displaystyle{{\footnotesize{\sf
Con}_{0}{=}\\{\bigwedge_{i=1}^{n}c_{i}{\approx}d_{i}\rightarrow
c{\approx}d\,{\mid}\begin{array}[]{l}f(c_{1},\dots,c_{n}){\approx}c{\in}{\sf
Def}\\\ f(d_{1},\dots,d_{n}){\approx}d{\in}{\sf Def}\end{array}\\}}}.$

This method is implemented in the program H-PILoT (Hierarchical Proving by
Instantiation in Local Theory Extensions) [29].

###  3.2 Locality of theories of distances

The theories related to wireless networks used in Section 2 refer to cost or
distance functions. We prove that axiomatizations for such functions define
local theory extensions. We first formalize the properties of metric spaces
$(X,d)$, i.e. sets endowed with a distance function $d$ satisfying the usual
axioms of a metric, and prove a locality property. We then consider variants
that contain only some of these axioms.

###### Theorem 5

Let ${\mathcal{T}}_{0}$ be the disjoint two-sorted combination of ${\cal E}$,
the pure theory of equality (no function symbols), sort ${\sf p}$, and
$LI({\mathbb{R}})$ (linear real arithmetic), sort ${\sf num}$. Let
${\mathcal{T}}^{m}_{d}$ be the extension of ${\mathcal{T}}_{0}$ with a
function $d$ with arity $a(d)={\sf p},{\sf p}\rightarrow{\sf num}$ satisfying
the following set ${\cal K}_{d}$ of axioms:

$\begin{array}[]{lrl}(d_{1})&\forall x,y&d(x,y)\geq 0\\\ (d_{2})&\forall
x,y,z&d(x,y)\leq d(x,z)+d(z,y)\\\ (d_{3})&\forall x,y&d(x,y)=d(y,x)\\\
(d_{4})&\forall x,y&x=y\rightarrow d(x,y)=0\\\ (d_{5})&\forall
x,y&d(x,y)=0\rightarrow x=y\end{array}$

Let $\Psi_{m}$ be defined for every set $T$ of ground terms by

$\Psi_{m}(T)=\\{d(a,b)\mid a,b\text{ are constants of sort }{\sf p}\text{
occurring in }T\\}.$

Then the following hold:

  * (1)

$\Psi_{m}$ is a closure operator on ground terms.

  * (2)

For every finite set $T$ of ground terms, $\Psi_{m}(T)$ is finite.

  * (3)

${\mathcal{T}}^{m}_{d}$ is a $\Psi_{m}$-local extension of ${\mathcal{T}}_{0}$
satisfying condition $({\sf Comp}^{\Psi}_{f})$.

Proof: (1) Clearly, for every set $T$ of ground terms, $T$ and $\Psi_{m}(T)$
contain the same constants of sort ${\sf p}$, so
$\Psi_{m}(\Psi_{m}(T))=\Psi_{m}(T)$. Since the only extension function symbol
is $d$, ${\sf est}({\mathcal{K}},T)\subseteq\Psi_{m}(T)$ for every set $T$ of
ground terms. The fact that if $T_{1}\subseteq T_{2}$ we have
$\Psi_{m}(T_{1})\subseteq\Psi_{m}(T_{2})$ follows from the definition. It is
also easy to check that for every map $h:C\rightarrow C$,
${\overline{h}}(\Psi_{m}(T))=\Psi_{m}({\overline{h}}(T))$, i.e. $\Psi_{m}$ is
stable under renaming of constants.

(2) If $T$ is finite, then it contains finitely many constants (say $n$).
$\Psi_{m}(T)$ has then $n^{2}$ elements.

(3) To prove that ${\mathcal{T}}^{m}_{d}$ is a $\Psi_{m}$-local extension of
$T_{0}$, we prove that it satisfies the embeddability condition (${\sf
Comp^{\Psi}_{w,f}}$), i.e. that for every partial model ${\cal
P}=(P,{\mathbb{R}},d_{P})$ of
${\mathcal{T}}_{d}={\mathcal{T}}_{0}\cup{\mathcal{K}}_{d}$ with the
properties:

  * (i)

All function symbols in $\Sigma_{0}$ are everywhere defined; $d$ is partially
defined.

  * (ii)

The set $T({\cal P})=\\{d(a_{1},a_{2})\mid\text{a}_{i}\in
A_{p},d_{P}(a_{1},a_{2})\text{ is defined}\\}$ is finite, and closed under
$\Psi_{m}$.

$d_{P}$ can be extended to a total function on $P$ that satisfies the axioms
${\mathcal{K}}_{d}$.

Let ${\cal P}=(P,{\mathbb{R}},d_{P})$ be a partial model of
${\mathcal{T}}^{m}_{d}={\mathcal{T}}_{0}\cup{\mathcal{K}}_{m}$ (where $P$ is
the support of sort p, ${\mathbb{R}}$ the support of sort num, and $d_{P}$ a
partial function from $P\times P$ to ${\mathbb{R}}$) satisfying the conditions
above. Then:

  * •

whenever $d_{P}(p_{1},p_{2})$ defined, $d_{P}(p_{1},p_{2})\geq 0$, and if
$p_{1}=p_{2}$, $d_{P}(p_{1},p_{2})=0$;

  * •

$d_{P}(p,p)=0$ whenever it is defined;

  * •

if $d_{P}(p_{1},p_{2})$ and $d_{P}(p_{2},p_{1})$ are defined then
$d_{P}(p_{1},p_{2})=d_{P}(p_{2},p_{1})$; and

  * •

if $d_{P}(p_{1},p_{2}),d_{P}(p_{2},p_{3}),d_{P}(p_{1},p_{3})$ are defined then
$d_{P}(p_{1},p_{2})\leq d_{P}(p_{2},p_{3})+d_{P}(p_{1},p_{3})$.

Let $E=\\{(p_{1},p_{2})\mid d_{P}(p_{1},p_{2})\text{ is defined}\\}$.

Let $P_{1}=\\{p\in P\mid\exists q\in P:d_{P}(p,q)\text{ defined or
}d_{P}(q,p)\text{ defined }\\}$. By the assumption that $d_{P}(p_{1},p_{2})$
is defined only for finitely many tuples $(p_{1},p_{2})$, $P_{1}$ is finite
and by condition (ii) above (as $T({\cal P})$ is closed under $\Psi_{m}$),
$E=P_{1}\times P_{1}$. Thus, $P=P_{1}\cup P_{2}$, such that
$d_{1}={d_{P}}_{|P_{1}}$ is totally defined and $d$ is nowhere defined on
$P_{2}$ (for every two different elements $p_{1},p_{2}\in P_{2}$,
$d_{P}(p_{1},p_{2})$ is undefined and for every $p\in P_{2}$ there is no $q\in
P_{1}$ such that $d_{P}(p,q)$ or $d_{P}(q,p)$ is defined).

Since $P_{1}$ is finite, the maximum $m_{1}={\sf max}\\{d(p,q)\mid p,q\in
P_{1}\\}$ exists.

Consider an arbitrary distance function $d_{2}$ on $P_{2}$ such that ${\sf
sup}\\{d_{2}(p_{1},p_{2})\mid p_{1},p_{2}\in P_{2}\\}$ is finite (such a
function is guaranteed to exist, since the distance axioms are consistent: We
can for instance regard all points in $P_{2}$ as points in the unit circle and
consider the euclidian distances between these points). Thus, the distance
function $d_{2}$ on $P_{2}$ is totally defined and bounded. Let $m_{2}$ be
such that $d_{2}(p,q)\leq m_{2}$ for all $p,q\in P_{2}$.

We now show how to extend $d$ on $P_{1}\cup P_{2}$. If $P_{1}$ or $P_{2}$ are
empty we have a total extension of $d$ already. Assume they are both non-
empty. Let $p_{1}\in P_{1}$ and $p_{2}\in P_{2}$. We construct a totally
defined function $d:(P_{1}\cup P_{2})^{2}\rightarrow{\mathbb{R}}$ as follows:

$d(p,q)=\left\\{\begin{array}[]{ll}d_{1}(p,q)&\text{ if }p,q\in P_{1}\\\
d_{2}(p,q)&\text{ if }p,q\in P_{2}\\\
d_{0}+d_{1}(p,p_{1})+d_{2}(p_{2},q)&\text{ if }p\in P_{1}\text{ and }q\in
P_{2}\\\ d_{0}+d_{1}(q,p_{1})+d_{2}(p_{2},p)&\text{ if }p\in P_{2}\text{ and
}q\in P_{1}\end{array}\right.$

where $d_{0}\in{\mathbb{R}}$, is such that $d_{0}={\sf m}+1$, where ${\sf
m}={\sf max}(m_{1},m_{2})$.

We show that $d$ is a total function that satisfies all the axioms
${\mathcal{K}}_{d}$:

  * •

It is clear that $d$ is a total function and that for all $x,y\in P_{1}\cup
P_{2},d(x,y)\geq 0$, i.e. it satisfies axiom $(d_{1})$.

  * •

Let $p\in P_{1}\cup P_{2}$. Then $p\in P_{i}$, with $i=1$ or $2$, and since
$d_{i}$ satisfies axiom $(d_{4})$, $d(p,p)=d_{i}(p,p)=0$. Thus $d$ satisfies
axiom $(d_{4})$ too.

  * •

Let $p,q\in P_{1}\cup P_{2}$. If $p,q\in P_{i}$ for $i=1$ or $2$, then
$d(p,q)=d_{i}(p,q)=d_{i}(q,p)=d(q,p)$ – since $d_{i}$ satisfies axiom
$(d_{3})$. If $p\in P_{1},q\in P_{2}$ then
$d(p,q)=d_{0}+d_{1}(p,p_{1})+d_{2}(p_{2},q)=d_{0}+d_{1}(p_{1},p)+d_{2}(q,p_{2})=d(q,p)$;
the case when $p\in P_{2},q\in P_{1}$ is similar. Thus $d$ satisfies axiom
$(d_{3})$ too.

  * •

Let $p,q\in P_{1}\cup P_{2}$. If $p,q\in P_{i}$, with $i=1$ or $2$, and
$d(p,q)=0$ then $d_{i}(p,q)=0$, so as $d_{i}$ satisfies axiom $(d_{5})$,
$p=q$. If $p\in P_{1}$ and $q\in P_{2}$ or $p\in P_{2}$ and $q\in P_{1}$ then
by definition $d(p,q)\geq d_{0}>0$, so we cannot have $d(p,q)=0$. Thus $d$
satisfies axiom $(d_{5})$ too.

  * •

We show that $d$ satisfies the triangle inequality (axiom $(d_{2})$). Let
$p,q,r\in P_{1}\cup P_{2}$. We show that $d(p,q)\leq d(p,r)+d(r,q)$. We
distinguish the following cases:

Case 1: $p\in P_{1},q\in P_{2}$.

Then $d(p,q)=d_{0}+d_{1}(p,p_{1})+d_{2}(p_{2},q)$.

Subcase 1.a: $r\in P_{1}$.

Then $d(p,r)+d(r,q)=d_{1}(p,r)+d_{0}+d_{1}(r,p_{1})+d_{2}(p_{2},q)\geq
d_{0}+d_{1}(p,p_{1})+d_{2}(p_{2},q)=d(p,q)$.

Subcase 1.b: $r\in P_{2}$.

Then $d(p,r)+d(r,q)=d_{0}+d_{1}(p,p_{1})+d_{2}(p_{2},r)+d_{2}(r,q)\geq
d_{0}+d_{1}(p,p_{1})+d_{2}(p_{2},q)=d(p,q)$.

Case 2: $p\in P_{2},q\in P_{1}$.

Then $d(p,q)=d_{0}+d_{1}(q,p_{1})+d_{2}(p_{2},p)$.

Subcase 2.a: $r\in P_{2}$.

Then
$d(p,r)+d(r,q)=d_{2}(p,r)+d_{0}+d_{1}(r,p_{2})+d_{2}(p_{1},q)=d_{2}(r,p)+d_{0}+d_{1}(q,p_{1})+d_{2}(p_{2},r)\geq
d_{0}+d_{1}(q,p_{1})+d_{2}(p_{2},p)=d(p,q)$.

Subcase 2.b: $r\in P_{1}$.

Then $d(p,r)+d(r,q)=d_{0}+d_{2}(p,p_{2})+d_{2}(p_{1},r)+d_{1}(r,q)\geq
d_{0}+d_{1}(p_{1},q)+d_{2}(p,p_{2})=d_{0}+d_{1}(q,p_{1})+d_{2}(p_{2},p)=d(p,q)$.

Case 3: $p,q\in P_{1}$.

Then $d(p,q)=d_{1}(p,q)$.

Subcase 3.a: $r\in P_{1}$.

Then $d(p,q)=d_{1}(p,q)\leq d_{1}(p,r)+d_{1}(r,q)=d(p,r)+d(r,q)$, since
$d_{1}$ satisfies axiom $(d_{2})$.

Subcase 3.b: $r\in P_{2}$.

Then $d(p,q){=}d_{1}(p,q){\leq}{\sf m}{<}d_{0}{\leq}d(p,r){+}d(r,q)$.

Case 4: $p,q\in P_{2}$.

Then $d(p,q)=d_{2}(p,q)$.

Subcase 4.a: $r\in P_{2}$.

Then $d(p,q)=d_{2}(p,q)\leq d_{2}(p,r)+d_{2}(r,q)=d(p,r)+d(r,q)$, since
$d_{2}$ satisfies axiom $(d_{2})$.

Subcase 4.b: $r\in P_{1}$.

Then $d(p,q){=}d_{2}(p,q){\leq}{\sf m}{<}d_{0}{\leq}d(p,r){+}d(r,q)$.

In [30] it was proved that condition $({\sf Comp}^{\Psi}_{f})$ for
${\mathcal{T}}_{0}\subseteq{\mathcal{T}}_{0}\cup{\mathcal{K}}$ implies
$\Psi$-locality of the extension if the clauses in ${\mathcal{K}}$ are flat
and linear. The clauses in ${\mathcal{K}}_{m}$ are flat, but are not linear.
In the proof of the fact that embeddability implies locality linearity is
needed in order to ensure that if we have a model $\mathcal{B}$ of
${\mathcal{T}}_{0}\cup{\mathcal{K}}[\Psi(G)]\cup G$ we can define a partial
model $\mathcal{A}$ of ${\mathcal{T}}_{0}\cup{\mathcal{K}}\cup G$ and argue
that (by $({\sf Comp}^{\Psi}_{f})$) this model embeds into a total model of
${\mathcal{T}}_{0}\cup{\mathcal{K}}\cup G$. We construct $\mathcal{A}$ as
follows: Its universe(s) are the same as for $\mathcal{B}$, and
$f(a_{1},\dots,a_{n})$ is defined in $\mathcal{A}$ if there exists constants
$c_{1},\dots,c_{n}$ which interpret in $\mathcal{A}$ as $a_{1},\dots,a_{n}$
and $f(c_{1},\dots,c_{n})$ occurs in $\Psi(G)$. This definition is used to
associate with every valuation in $\mathcal{A}$ in which all terms in a clause
$C$ are defined a substitution $\sigma$ such that
$C\sigma\in{\mathcal{K}}[\Psi(G)]$.

If the clause $C$ is linear the substitution can be defined without problems.
If $C$ contains a variable in different terms, it might be difficult to define
$\Sigma$ because for different occurrences of $x$ we might find different
suitable terms.

This problem does not occur here because of the fact that $\Psi_{m}$ adds all
necessary instances that allow to define $\sigma$ without problems.

Alternatively, it can be easily checked that all assumptions in Theorem 2 hold
in this case, so in this case embeddability entails locality. $\Box$

We can still obtain local theory extensions if we leave out some of the metric
axioms. Below we consider, for instance, extensions with a function $d$ in
which all the axioms of a metric except for the triangle inequality hold.

###### Theorem 6

Let ${\mathcal{T}}_{0}$ be the disjoint two-sorted combination of the theory
$\cal{E}$ of pure equality (no function symbols), sort ${\sf p}$, and
$LI({\mathbb{R}})$ (linear real arithmetic), sort ${\sf num}$. Let
${\mathcal{T}}^{n}_{d}$ be the extension of ${\mathcal{T}}_{0}$ with a
function $d$ with arity $a(d)={\sf p},{\sf p}\rightarrow{\sf num}$ satisfying
the following set ${\cal K}_{n}$ of axioms:

$\begin{array}[]{lrl}(d_{1})&\forall x,y&d(x,y)\geq 0\\\ (d_{3})&\forall
x,y&d(x,y)=d(y,x)\\\ (d_{4})&\forall x,y&x=y\rightarrow d(x,y)=0\\\
(d_{5})&\forall x,y&d(x,y)=0\rightarrow x=y\end{array}$

Let $\Psi_{n}$ be defined for every set $T$ of ground terms by

$\begin{array}[]{ll}\Psi_{n}(T)=T&\cup\\{d(t_{2},t_{1})\mid d(t_{1},t_{2})\in
T\\}\\\ &\cup\\{d(a,a)\mid a\text{ is a constant of sort {\sf p} occurring in
}T\\}\end{array}$

Then ${\mathcal{T}}^{n}_{d}$ is a $\Psi_{n}$-local extension of
${\mathcal{T}}_{0}$.

Proof: To prove locality we have to show that every partial model of
${\mathcal{T}}^{n}_{d}={\mathcal{T}}_{0}\cap{\cal K}_{n}$ which is closed
under $\Psi_{n}$ can be extended to a total model. Let ${\cal
P}=(P,{\mathbb{R}},d_{P})$ be a partial model of
${\mathcal{T}}_{d}={\mathcal{T}}_{0}\cup{\mathcal{K}}_{d}$ (where $P$ is the
support of sort p, ${\mathbb{R}}$ the support of sort num, and $d_{P}$ a
partial function from $P\times P$ to ${\mathbb{R}}$) satisfying the conditions
above. We construct a total function $d:P\times P\rightarrow{\mathbb{R}}$ as
follows:

$d(p,q)=\left\\{\begin{array}[]{ll}d_{P}(p,q)&\text{ if }d_{P}(p,q)\text{ is
defined}\\\ 0&\text{ if }d_{P}(p,q)\text{ is not defined and }p=q\\\ 1&\text{
if }d_{P}(p,q)\text{ is not defined and }p\neq q\\\ \end{array}\right.$

It is easy to check that $d$ satisfies all the axioms in ${\cal K}_{n}$. The
considerations in the previous proof (or Theorem 2) can be used also in this
case to show that embeddability implies locality in spite of the non-linearity
due to the choice of the closure operator. $\Box$

###### Theorem 7

Let ${\mathcal{T}}_{0}$ be the disjoint combination of the theory of pure
equality (sort ${\sf p}$) and linear real arithmetic (sort ${\sf num}$). The
following extensions of ${\mathcal{T}}_{0}$ with a function $d$ (sort ${\sf
p}{\times}{\sf p}{\rightarrow}{\sf num}$) are $\Psi$-local, with $\Psi$ being
the identity function.

  * (i)

${\mathcal{T}}^{u}_{d}$, the extension of ${\mathcal{T}}_{0}$ with an
uninterpreted function $d$.

  * (ii)

${\mathcal{T}}^{p}_{d}={\mathcal{T}}_{0}\cup{\mathcal{K}}_{p}$, where
${\mathcal{K}}_{p}=\forall x,y~{}d(x,y)\geq 0$.

The extension ${\mathcal{T}}^{s}_{d}={\mathcal{T}}_{0}\cup{\mathcal{K}}_{s}$,
where ${\mathcal{K}}_{s}=\forall x,y~{}d(x,y)=d(y,x)$ is $\Psi_{s}$-local,
where $\Psi_{s}(T)=T\cup\\{d(a,b)\mid d(b,a)\in T\\}$.

Proof. (i) and (ii) are a direct consequence of Theorem 3; the locality proof
for ${\mathcal{T}}^{s}_{d}$ is similar to the one for ${\mathcal{T}}^{n}_{d}$.
$\Box$

We present all the results together in the following theorem:

###### Theorem 8

Let ${\mathcal{T}}_{0}$ be the disjoint combination of the theory ${\cal E}$
of pure equality (sort ${\sf p}$) and linear real arithmetic (sort ${\sf
num}$). The following extensions of ${\mathcal{T}}_{0}$ with a function $d$
(sort ${\sf p}{\times}{\sf p}{\rightarrow}{\sf num}$) are $\Psi$-local for a
suitable closure operator $\Psi$:

  * (1)

${\mathcal{T}}^{m}_{d}={\mathcal{T}}_{0}\cup{\mathcal{K}}_{m}$, where
${\mathcal{K}}_{m}$ are axioms of a metric, is $\Psi_{m}$-local, where
$\Psi_{m}(T)=\\{d(a,b)\mid a,b\text{ constants of sort }{\sf p}\text{
occurring in }T\\}$.

  * (2)

${\mathcal{T}}^{n}_{d}={\mathcal{T}}_{0}\cup{\mathcal{K}}_{n}$, where
${\mathcal{K}}_{n}$ contains all axioms of a metric except for the triangle
inequality, is $\Psi_{n}$-local, where $\Psi_{n}(T)=T\cup\\{d(b,a)\mid
d(a,b)\in T\\}\cup\\{d(a,a)\mid a\text{ constant of sort }{\sf p}\text{
occurring in }T\\}$.

  * (3)

${\mathcal{T}}^{u}_{d}$, the extension of ${\mathcal{T}}_{0}$ with an
uninterpreted function $d$, and
${\mathcal{T}}^{p}_{d}={\mathcal{T}}_{0}\cup{\mathcal{K}}_{p}$, where
${\mathcal{K}}_{p}=\forall x,y~{}d(x,y)\geq 0$, are $\Psi$-local, where
$\Psi(T)=T$.

##  4 Property-directed symbol elimination and locality

In [41] we proposed a method for property-directed symbol elimination
described in Algorithm 1. We present a slight generalization.

Algorithm 1 Symbol elimination in theory extensions [40, 41]

Input: | Theory extension ${\mathcal{T}}_{0}\cup{\mathcal{K}}$ with signature $\Pi=\Pi_{0}\cup(\Sigma\cup\Sigma_{\sf par})$
---|---
| where $\Sigma_{\sf par}$ is a set of parameters
| Set $T$ of ground $\Pi^{C}$-terms
Output: |  $\forall{\overline{y}}\Gamma_{T}({\overline{y}})$ (universal $\Pi_{0}\cup\Sigma_{\sf par}$-formula)

Step 1

Purify ${\mathcal{K}}[T]\cup G$ as described in Theorem 4 (with set of
extension symbols $\Sigma_{1}$). Let ${\mathcal{K}}_{0}\cup G_{0}\cup{\sf
Con}_{0}$ be the set of $\Pi_{0}^{C}$-clauses obtained this way.

Step 2

Let $G_{1}={\mathcal{K}}_{0}\cup G_{0}\cup{\sf Con}_{0}$. Among the constants
in $G_{1}$, we identify

  1. (i)

the constants $c_{f}$, $f\in\Sigma_{\sf par}$, where $c_{f}$ is a constant
parameter or $c_{f}$ is introduced by a definition $c_{f}\approx
f(c_{1},\dots,c_{k})$ in the hierarchical reasoning method,

  2. (ii)

all constants ${\overline{c}_{p}}$ occurring as arguments of functions in
$\Sigma_{\sf par}$ in such definitions.

Replace all the other constants ${\overline{c}}$ with existentially quantified
variables ${\overline{x}}$ (i.e. replace
$G_{1}({\overline{c}_{p}},{\overline{c}_{f}},{\overline{c}})$ with
$\exists{\overline{x}}G_{1}({\overline{c}_{p}},{\overline{c}_{f}},{\overline{x}})$).

Step 3

Construct a formula $\Gamma_{1}({\overline{c}_{p}},{\overline{c}_{f}})$
equivalent to
$\exists{\overline{x}}G_{1}({\overline{c}_{p}},{\overline{c}_{f}},{\overline{x}})$
w.r.t. ${\mathcal{T}}_{0}$ using a method for quantifier elimination in
${\mathcal{T}}_{0}$.

Step 4

Replace each constant $c_{f}$ introduced by definition
$c_{f}=f(c_{1},\dots,c_{k})$ with the term $f(c_{1},\dots,c_{k})$ in
$\Gamma_{1}({\overline{c}_{p}},{\overline{c}_{f}})$. Let
$\Gamma_{2}({\overline{c}_{p}})$ be the formula obtained this way. Replace
${\overline{c}_{p}}$ with existentially quantified variables ${\overline{y}}$.

Step 5

Let $\forall{\overline{y}}\Gamma_{T}({\overline{y}})$ be
$\forall{\overline{y}}\neg\Gamma_{2}({\overline{y}})$.

######  Theorem 9 ([40, 41])

Let ${\cal T}_{0}$ be a $\Pi_{0}$-theory allowing quantifier elimination222If
${\mathcal{T}}_{0}$ does not allow QE but has a model completion
${\mathcal{T}}_{0}^{*}$ which does, and if we use QE in
${\mathcal{T}}_{0}^{*}$ in Algorithm 1,
${\mathcal{T}}_{0}\wedge\forall{\overline{x}}\Gamma_{T}({\overline{x}})\cup
G\models\bot$, but $\forall{\overline{x}}\Gamma_{T}({\overline{x}})$ might not
be the weakest universal formula $\Gamma$ with the property that
${\mathcal{T}}_{0}\cup\Gamma\cup{\mathcal{K}}\models\bot$. $\Sigma_{\sf par}$
be a set of parameters (function and constant symbols) and $\Pi=(S,\Sigma,{\sf
Pred})$ be such that $\Sigma\cap(\Sigma_{0}\cup\Sigma_{\sf par})=\emptyset$.
Let ${\cal K}$ be a set of clauses in the signature $\Pi_{0}{\cup}\Sigma_{\sf
par}{\cup}\Sigma$ in which all variables occur also below functions in
$\Sigma_{1}=\Sigma_{\sf par}\cup\Sigma$. Assume
${\mathcal{T}}\subseteq{\mathcal{T}}_{0}\cup{\mathcal{K}}$ satisfies condition
$({\sf Comp}^{\Psi}_{f})$ for a suitable closure operator $\Psi$ with ${\sf
est}(G)\subseteq\Psi_{{\mathcal{K}}}(G)$ for every set $G$ of ground
$\Pi^{C}$-clauses. Then, for $T=\Psi_{{\mathcal{K}}}(G)$, Algorithm 1 yields a
universal $\Pi_{0}\cup\Sigma_{\sf par}$-formula
$\forall{\overline{x}}\Gamma_{T}({\overline{x}})$ such that ${\cal
T}_{0}\cup\forall{\overline{x}}\Gamma_{T}({\overline{x}})\cup{\cal K}\cup
G\models\perp$ which is entailed by every universal formula $\Gamma$ with
${\cal T}_{0}\cup\Gamma\cup{\cal K}\cup G\models\perp$.

Proof: The fact that ${\mathcal{T}}_{0}\cup{\mathcal{K}}\cup\forall
x\Gamma_{T}(x)\models\perp$ was proved in [41]. We show that if
$T=\Psi_{{\mathcal{K}}}(G)$ then for every set $\Gamma$ of universal
constraints on the parameters, if
${\mathcal{T}}_{0}\cup\Gamma\cup{\mathcal{K}}\cup G$ is unsatisfiable then
every model of ${\mathcal{T}}_{0}\cup\Gamma$ is a model of
${\mathcal{T}}_{0}\cup\forall y\Gamma_{T}(y)$.

In [41] it is shown that if the extension
${\mathcal{T}}_{0}\subseteq{\mathcal{T}}_{0}\cup{\mathcal{K}}$ satisfies
condition $({\sf Comp}^{\Psi}_{f})$ then also the extension
${\mathcal{T}}_{0}\cup\Gamma\subseteq{\mathcal{T}}_{0}\cup\Gamma\cup{\mathcal{K}}$
satisfies condition $({\sf Comp}^{\Psi}_{f})$. If ${\mathcal{K}}$ is flat and
linear then the extension is $\Psi$-local. Let
$T=\Psi_{{\mathcal{K}}}(G)=\Psi({\sf est}({\mathcal{K}},G))$. By
$\Psi$-locality, ${\mathcal{T}}_{0}\cup\Gamma\cup{\mathcal{K}}\cup G$ is
unsatisfiable if and only if
${\mathcal{T}}_{0}\cup\Gamma\cup{\mathcal{K}}[T]\cup G$ is unsatisfiable, if
and only if (with the notations in Steps 1–5 of Algorithm 1)
${\mathcal{T}}_{0}\cup\Gamma\cup{\mathcal{K}}_{0}\cup G_{0}\cup{\sf
Con}_{0}\cup{\sf Def}$ is unsatisfiable. Let ${\mathcal{A}}$ be a model of
${\mathcal{T}}_{0}\cup\Gamma$. Then in ${\mathcal{A}}$ there are no possible
values for the constants
$G_{1}({\overline{c}_{p}},{\overline{c}_{f}},{\overline{c}})={\mathcal{K}}_{0}\cup
G_{0}\cup{\sf Con}_{0}\cup{\sf Def}$, for which
$G_{1}({\overline{c}_{p}},{\overline{c}_{f}},{\overline{c}})$ is true in
${\mathcal{A}}$. Hence,
${\mathcal{A}}\not\models\exists{\overline{x}}G_{1}({\overline{c}_{p}},{\overline{c}_{f}},{\overline{x}})$,
so (with the notation used when describing Steps 1–5)
${\mathcal{A}}\not\models\exists{\overline{y}}\Gamma_{2}({\overline{y}})$. It
follows that
${\mathcal{A}}\models\forall{\overline{y}}\Gamma_{T}({\overline{y}})$. $\Box$

This reduction method was implemented in sehpilot (for details cf. Section 7).

##  5 Second-order quantifier elimination

Let ${\mathcal{T}}$ be a theory with signature $\Pi=(S,\Sigma,{\sf Pred})$ and
$P_{1},\dots,P_{n},Q_{1},\dots,Q_{m}$ be predicate symbols which are not in
${\sf Pred}$. Let $\Pi^{\prime}=(S,\Sigma,{\sf
Pred}{\cup}\\{P_{1},\dots,P_{n}\\})$ and $\Pi^{\prime\prime}=(S,\Sigma,{\sf
Pred}{\cup}\\{Q_{1},\dots,Q_{m}\\})$; $F$ be a $\Pi^{\prime}$-formula and $G$
a $\Pi^{\prime\prime}$-formula.

A $\Pi$-structure $\mathcal{A}$ is a model of $\exists P_{1}\dots P_{n}~{}F$
(notation: $\mathcal{A}\models\exists P_{1}\dots P_{n}~{}F$) if there exists a
$\Pi^{\prime}$-structure ${\cal B}$ such that ${\cal B}\models F$ and ${\cal
B}_{|_{\Pi}}=\mathcal{A}$.

We say that $\exists P_{1}\dots P_{n}~{}F$ entails $\exists Q_{1}\dots
Q_{m}~{}G$ w.r.t. ${\mathcal{T}}$ (and use the notation: $\exists P_{1}\dots
P_{n}~{}F\models_{{\mathcal{T}}}\exists Q_{1}\dots Q_{m}~{}G$) iff for every
$\Pi$-structure ${\cal A}$ which is a model of ${\mathcal{T}}$, if
$\mathcal{A}\models\exists P_{1}\dots P_{n}~{}F$ then
$\mathcal{A}\models\exists Q_{1}\dots Q_{m}~{}G$.

If there exists a first-order formula $F_{0}$ over the signature $\Pi$ such
that for every model ${\cal A}$ of ${\mathcal{T}}$, ${\cal A}\models F_{0}$
iff ${\cal A}\models\exists P_{1}\dots P_{n}~{}F$, we say that $F_{0}$ and
$\exists P_{1}\dots P_{n}~{}F$ are equivalent w.r.t. ${\mathcal{T}}$ (and
write $F_{0}\equiv_{{\mathcal{T}}}\exists P_{1}\dots P_{n}~{}F$).

We consider here only the elimination of one predicate; for formulae of the
form $\exists P_{1}\dots P_{n}~{}F$ the process can be iterated. Let
${\mathcal{T}}$ be a theory with signature $\Pi=(S,\Sigma,{\sf Pred})$ and let
$\Pi^{\prime}=(S,\Sigma,{\sf Pred}\cup\\{P\\})$, where $P\not\in{\sf Pred}$.

Let $F$ be a universal first-order $\Pi^{\prime}$-formula. Our goal is to
compute, if possible, a first-order $\Pi$-formula $G$ such that
$G\equiv_{{\mathcal{T}}}\exists P~{}F$. We adapt the hierarchical
superposition calculus proposed in [8, 9] to this case.

We consider theories ${\mathcal{T}}$ over many-sorted signatures
$\Pi=(S,\Sigma,{\sf Pred})$, where the set of sorts $S=S_{i}\cup S_{u}$
consists of a set $S_{i}$ of interpreted sorts and a set $S_{u}$ of
uninterpreted sorts. The models of the theories are $\Pi$-structures
$\mathcal{A}=(\\{A_{s}\\}_{s\in
S},\\{f_{\mathcal{A}}\\}_{f\in\Sigma},\\{p_{A}\\}_{p\in{\sf Pred}})$, where
each support of interpreted sort is considered to be fixed. Following the
terminology used in [8, 9], we will refer to elements in the fixed domain of
sort $s\in S_{i}$ as domain elements of sort $s$.

Let $F$ be a universal first-order formula over signature
$\Pi^{\prime}=(S,\Sigma,{\sf Pred}\cup\\{P\\})$. We can assume, without loss
of generality, that $F$ is a set of clauses of the form
$\forall{\overline{x}}~{}D({\overline{x}})\vee C({\overline{x}})$, where
$D({\overline{x}})$ is a clause over the signature $\Pi$ and
$C({\overline{x}})$ is a clause containing literals of the form
$(\neg)P(x_{1},\dots,x_{n})$, where $x_{1},\dots,x_{n}$ are variables333We can
bring the clauses to this form using variable abstraction.. Such clauses can
also be represented as constrained clauses in the form
$\forall{\overline{x}}~{}\phi({\overline{x}})~{}||~{}C({\overline{x}}),\text{
where }\phi({\overline{x}}):=\neg D({\overline{x}}).$ We will refer to clauses
of this form as constrained $P$-clauses.

Let $\succ$ be a strict, well-founded ordering on terms that is compatible
with contexts and stable under substitutions. As in [9] we assume that $\succ$
has the following properties:444These conditions are satisfied by an LPO with
an operator precedence in which the predicate symbol $P$ (which can be
regarded as function symbol with output sort ${\sf bool}$) is larger than the
other operators and domain elements are minimal w.r.t. $\succ$ which is
supposed to be well-founded on the domain elements.

  * (i)

$\succ$ is total on ground terms,

  * (ii)

$t\succ d$ for every domain element $d$ of interpreted sort $s$ and every
ground term $t$ that is not a domain element.

Let $\mathit{HRes}^{P}_{\succ}$ be the calculus containing the following
ordered resolution and factorization rules for constrained $P$-clauses:

$\begin{array}[]{ll}\displaystyle{{\phi_{1}~{}||~{}P({\overline{x}})\vee
C\quad\quad\phi_{2}~{}||~{}\neg P({\overline{y}})\vee
D}\over{(\phi_{1}\wedge\phi_{2})\sigma~{}||~{}(C\vee
D)\sigma}}\quad\quad\quad\quad\quad\quad\displaystyle{{\phi~{}||~{}P({\overline{x}})\vee
P({\overline{y}})\vee C}\over{\phi\sigma~{}||~{}(P({\overline{x}})\vee
C)\sigma}}\end{array}$

where (i) | $\sigma={\sf mgu}(P({\overline{x}}),P({\overline{y}}))$ | (i) | $\sigma={\sf mgu}(P({\overline{x}}),P({\overline{y}}))$
---|---|---|---
(ii) |  $P({\overline{x}})\sigma$ is strictly maximal in $(P({\overline{x}})\vee C)\sigma$ | (ii) |  $P({\overline{x}})\sigma$ is maximal in
(iii) |  $\neg P({\overline{y}})\sigma$ is maximal in $(\neg P({\overline{y}})\vee D)\sigma.$ |  | $(P({\overline{x}})\vee C)\sigma$

Redundancy. The inference rules are supplemented by a redundancy criterion
${\cal R}=({\cal R}_{c},{\cal R}_{i})$ meant to specify:

  * •

a set ${\cal R}_{c}$ of redundant clauses (which can be removed), and

  * •

a set ${\cal R}_{i}$ of redundant inferences (which do not need to be
computed).

We say that a set of clauses $N^{*}$ is saturated up to ${\cal R}$-redundancy
w.r.t. $\mathit{HRes}^{P}_{\succ}$ if every $\mathit{HRes}^{P}_{\succ}$
inference with premises in $N^{*}$ is redundant (i.e. in ${\cal R}_{i}$).

The following notion of redundancy ${\cal R}^{0}_{c}$ for clauses is often
used: A (constrained) clause is redundant w.r.t. a set $N$ of clauses if all
its ground instances are entailed w.r.t. ${\mathcal{T}}$ by ground instances
of clauses in $N$ which are strictly smaller w.r.t. $\succ$. We will use the
following notion of redundancy for inferences: If ${\cal R}_{c}$ is a
redundancy criterion for clauses, we say that an inference $\iota$ on ground
clauses is redundant w.r.t. $N$ if either one of its premises is redundant
w.r.t. $N$ and ${\cal R}_{c}$ or, if $C_{0}$ is the conclusion of $\iota$ then
there exist clauses $C_{1},\dots,C_{n}\in N$ that are smaller w.r.t. $\succ$
than the maximal premise of $\iota$ and $C_{1},\dots,C_{n}\models C_{0}$.

A non-ground inference is redundant if all its ground instances are redundant.

######  Example 1 (Semantic ${\mathcal{T}}$-entailment; redundancy criterion
${\cal R}_{{\mathcal{T}}}$)

We say that a constrained $P$-clause
$\forall{\overline{x}}~{}(\phi({\overline{x}})~{}||~{}C({\overline{x}}))$ is
${\mathcal{T}}$-semantically entailed by
$\forall{\overline{x}}~{}(\psi({\overline{y}})~{}||~{}D({\overline{y}}))$ if
the following conditions hold:

  * (i)

$C=D$,

  * (ii)

${\mathcal{T}}\models\forall{\overline{x}}~{}\phi({\overline{x}})\rightarrow\psi({\overline{x}})$
and

  * (iii)

$\neg\phi({\overline{x}})\sigma\succ\neg\psi({\overline{y}})\sigma$ for every
ground substitution $\sigma$.

We say that a clause $C$ is ${\cal R}_{{\mathcal{T}}}$-redundant w.r.t. a set
$N$ of clauses if it is ${\mathcal{T}}$-semantically entailed by a clause in
$N$.

Note that if $C_{1}{=}(\phi({\overline{x}})||C({\overline{x}}))$ is
${\mathcal{T}}$-semantically entailed by
$C_{2}{=}(\psi({\overline{y}})||D({\overline{y}}))$ then $C_{1}\sigma\succ
C_{2}\sigma$ and $C_{2}\sigma\models_{{\mathcal{T}}}C_{1}\sigma$ for every
ground substitution $\sigma$, so ${\cal R}_{{\mathcal{T}}}$-redundant clauses
are ${\cal R}^{0}_{c}$-redundant.

We call the notion of redundancy induced on inferences also ${\cal
R}_{{\mathcal{T}}}$-redundancy.  $\blacksquare$

Let ${\cal R}=({\cal R}_{c},{\cal R}_{i})$ be a redundancy criterion with
${\cal R}_{c}\subseteq{\cal R}^{0}_{c}$. We want to prove that if $N$ is a set
of constrained $P$-clauses over background theory ${\mathcal{T}}$, $N^{*}$ its
saturation (up to ${\cal R}$-redundancy) under $\mathit{HRes}^{P}_{\succ}$,
and $N^{*}_{0}$ the set of clauses in $N^{*}$ not containing $P$, then for
every model $\mathcal{A}$ of ${\mathcal{T}}$, $\mathcal{A}$ is a model of
$N^{*}_{0}$ if and only if there exists a $\Pi^{\prime}$-structure ${\cal B}$
with $\mathcal{B}\models N$ and ${\cal B}_{|_{\Pi}}={\cal A}$. The proof of
this fact is very similar to the proof of the completeness of hierarchical
superposition. Since our goal is different, we present here all the details
just for the sake of completeness. (The results are probably known, already in
[5] it was mentioned that hierarchical superposition can be used for second-
order quantifier elimination.) We start with a lemma.

###### Lemma 10

Let $\Pi=(S,\Sigma,{\sf Pred})$, ${\mathcal{T}}$ be a theory with signature
$\Pi$ and let $\mathcal{A}=(\\{A_{s}\\}_{s\in
S},\\{f_{\mathcal{A}}\\}_{f\in\Sigma},\\{p_{\mathcal{A}}\\}_{p\in{\sf Pred}})$
be a $\Pi$-structure which is a model of ${\mathcal{T}}$. For every element
$a\in A_{s}$ we add a new constant of sort $s$ (which we denote $a$). Let
$C_{A}{=}\bigcup_{s\in S}A_{s}$ be the set of all constants introduced this
way, and ${\cal A}^{A}$ be the extension of ${\cal A}$ with constants from
$C_{A}$ which are interpreted in the usual way.

Let $N$ be a set of clauses over signature $\Pi$. Then the following are
equivalent:

  * (1)

${\cal A}$ is a model of $N$.

  * (2)

${\cal A}^{A}$ is a model of the set $N_{A}$ of all ground instances of $N$ in
which the variables are replaced with constants in $C_{A}$.

Proof: (1) $\Rightarrow$ (2): Assume that ${\cal A}$ is a model of $N$. Let
$C$ be a clause in $N_{A}$. Then $C$ is obtained from a clause $C^{\prime}\in
N$ by replacing every variable $x$ with a constant $a_{x}\in C_{A}$ (such that
if the variable $x$ has sort $s$ then $a_{x}\in A_{s}$). Let
$\beta:X\rightarrow{\cal A}$ be defined by $\beta(x)=a_{x}$ for every $x\in X$
occurring in $C^{\prime}$ and defined arbitrarily for all the other variables.
Since ${\cal A}$ is a model of $N$, the clause $C^{\prime}$ is true in ${\cal
A}$ in the valuation $\beta$. But ${\cal A}(\beta(C^{\prime}))$ is obtained by
evaluating the function and predicate symbols as in ${\cal A}$ and every
variable $x$ occurring in $C^{\prime}$ as $a_{x}$. This is exactly the value
of $C^{\prime}$ in ${\cal A}^{A}$, thus ${\cal A}^{A}$ is a model of $C$.

(2) $\Rightarrow$ (1): Assume that ${\cal A}^{A}$ is a model of $N_{A}$. Let
$C\in N$ and let $\beta:X\rightarrow{\cal A}$ be a valuation. For every $x\in
X$, let $a_{x}:=\beta(x)$. As discussed before, the value of $C$ in ${\cal A}$
w.r.t. $\beta$ is the same as the value of $C^{\prime}=C\sigma$ in ${\cal
A}^{A}$, where $\sigma$ is the substitution that associates with every
variable $x$ the constant $a_{x}\in C_{A}$. Since ${\cal A}^{A}$ is a model of
the set $N_{A}$ and $C^{\prime}\in N_{A}$, ${\cal A}^{A}$ is also a model of
$C^{\prime}$. It follows that $C$ is true in ${\cal A}$ w.r.t. $\beta$ for
every valuation $\beta$, i.e. that ${\cal A}$ is a model of $N$. $\Box$

###### Theorem 11

Let $N$ be a set of constrained $P$-clauses over background theory
${\mathcal{T}}$, $N^{*}$ its saturation (up to ${\cal R}$-redundancy) under
$\mathit{HRes}^{P}_{\succ}$, and $N^{*}_{0}$ the set of clauses in $N^{*}$ not
containing $P$. For every model $\mathcal{A}$ of ${\mathcal{T}}$ the following
are equivalent:

  * (1)

$\mathcal{A}$ is a model of $N^{*}_{0}$.

  * (2)

There exists a $\Pi^{\prime}$-structure ${\cal B}$ with $\mathcal{B}\models N$
and ${\cal B}_{|_{\Pi}}={\cal A}$.

Proof: First, note that for constrained $P$-clauses the hierarchical
superposition calculus specializes to $\mathit{HRes}^{P}_{\succ}$: With the
terminology used in [5, 8, 9], the background signature is $\Pi$; the only
foreground symbol is $P$. Since there are no “background”-sorted terms
starting with a “foreground” function symbol, sets of $P$-clauses are
sufficiently complete. (Even if we regard predicates as functions with values
in the domain $\\{0,1\\}$, since predicates can only take values 0 or 1
sufficient completeness is guaranteed.) Since in the special case we consider
there are no foreground terms, in this case all substitutions are simple as
well.

(2) $\Rightarrow$ (1) follows from the soundness of the hierarchical
superposition calculus.

(1) $\Rightarrow$ (2) is proved with a model construction similar to the one
used for proving completeness of hierarchical superposition. Let $\mathcal{A}$
be a model of $N^{*}_{0}$ and ${\mathcal{T}}$. Consider the extension
$\Pi^{A}$ of the signature $\Pi$ obtained by adding to $\Sigma$ a set
$C_{\mathcal{A}}$ containing a constant $a$ of sort $s$ for every element
$a\in A_{s}$.

Since $\mathcal{A}$ is a model of $N^{*}_{0}$, by Lemma 10, $\mathcal{A}^{A}$
is a model of the set ${N^{*}_{0}}_{A}$ of instances of $N^{*}_{0}$ in which
the variables are replaced with constants in $C_{A}$.

By Zermelo’s theorem, there exists a total well-founded strict order $\succ$
on the set of all constants in $\Pi$, and starting with this ordering we can
obtain a total well-founded strict ordering (which we denote again with
$\succ$) on the set of all ground terms over $\Pi^{A}$, which can be extended
in the usual way to the set of all ground clauses over the signature
${\Pi^{\prime}}^{A}=(S,\Sigma\cup C_{A},{\sf Pred}\cup\\{P\\})$, such that the
literals containing the predicate symbol $P$ are larger than the literals not
containing $P$.555This is compatible with regarding $P$ as a function symbol
with output sort ${\sf bool}$ and using an ordering in which $P$ is the
largest function symbol.

Consider the clauses in the set $N^{*}_{A}$ ordered increasingly according to
the clause ordering induced by the atom ordering. Since $N^{*}$ is saturated
w.r.t. $\mathit{HRes}^{P}_{\succ}$, $N^{*}_{A}$ is also saturated w.r.t.
$\mathit{HRes}^{P}_{\succ}$. We construct a model for $N^{*}_{A}$ using a
canonical model construction, similar to the one usually used for proving
completeness of ordered resolution. We sketch the construction here:

We start with an interpretation in which all atoms in the set
$\\{P(a_{1},\dots,a_{k})\mid i\in\\{1,\dots n\\},a_{j}\in C_{A}\text{ constant
of suitable sort, for all }j\in\\{1,\dots,k\\}\\}$ are false. The clauses in
$(N^{*}_{0})_{A}$ are smaller than the clauses containing the predicate symbol
$P$ and by assumption are all true in ${\cal A}$, hence also in the
interpretation that we start with (and will remain true in the process of
constructing $\mathcal{B}$). We therefore only need to consider the set
$N^{*}_{P}$ of all constrained $P$-clauses containing the predicate symbol
$P$. When considering a clause $C$, we assume that we already constructed a
partial interpretation ${\cal B}_{\prec C}$ that makes true all clauses
strictly smaller than $C$.

  * •

If $C$ is true in the partial interpretation ${\cal B}_{\prec C}$ nothing
needs to be done.

  * •

If $C$ is false in the partial interpretation ${\cal B}_{\prec C}$ we need to
change ${\cal B}_{\prec C}$ such that $C$ becomes true (such that the clauses
smaller than $C$ remain true).

We proceed as follows: If $C$ is false in ${\cal B}_{\prec C}$ and contains
exactly one maximal literal which is positive (which needs to start with $P$
and is for instance of the form $P({\overline{a}})$), we change the
interpretation of $P$ such that it contains the tuple ${\overline{a}}$, i.e.
such that $P({\overline{a}})$ becomes true. We denote this by setting
$\Delta_{C}:=\\{P({\overline{a}})\\}$. Otherwise we do not change the
interpretation, i.e. $\Delta_{C}:=\emptyset$.

The candidate model is the limit of all these changes, ${\cal B}:={\cal
A}\cup\bigcup_{C\in N_{1}}\Delta_{C}$.

We can show that the expansion ${\cal B}^{A}$ of ${\cal B}$ with the constants
in $C_{A}$ (with the usual interpretation) is a model of $(N^{*}_{P})_{A}$ in
the usual way: Assume that there exists a clause in $(N^{*}_{P})_{A}$ which is
not true in ${\cal B}^{A}$. Since the ordering on $(N^{*}_{P})_{A}$ is well-
founded, we consider without loss of generality the smallest clause in
$(N^{*}_{P})_{A}$ which is false in $\mathcal{B}^{A}$. We can show in the
usual way that using a resolution or a factorization step we can produce a
smaller clause false in $\mathcal{B}^{A}$, which is either in
$(N^{*}_{P})_{A}$ or in $(N^{*}_{0})_{A}$, so in both cases we obtain a
contradiction.

Since $\mathcal{B}^{A}$ is a model of $N^{*}_{A}$, and
$\mathcal{B}_{s}=\mathcal{A}_{s}$ for every sort $s$ (hence
$\mathcal{B}^{A}=\mathcal{B}^{B}$), it follows that $\mathcal{B}$ is a model
of $N^{*}=N^{*}_{0}\cup N^{*}_{P}$. $\Box$

###### Corollary 12

Let ${\mathcal{T}}$ be a theory, $N$ be a set of constrained $P$-clauses and
$N^{*}$ be a set of constrained $P$-clauses obtained by saturating $N$ in
$\mathit{HRes}^{P}_{\succ}$ up to redundancy. Let $\mathcal{A}$ be a
$\Pi$-structure which is a model of ${\mathcal{T}}$. Then $\mathcal{A}$ is a
model of $N^{*}_{0}$ if and only if there exists a $\Pi^{\prime}$-structure
${\cal B}$ with $\mathcal{B}\models N$ and ${\cal B}_{|_{\Pi}}={\cal A}$.

Proof: Follows from the fact that in the proof of Theorem 11 the clauses which
are redundant are entailed (w.r.t. ${\mathcal{T}}$) by clauses that are
smaller hence cannot be minimal counterexamples and cannot influence the way
model $\mathcal{B}$ is built because every redundant clause $C$ is true in
$\mathcal{B}_{\prec C}$. $\Box$

###  5.1 Case 1: Saturation is finite

If the saturation $N^{*}$ of $N$ under $\mathit{HRes}^{P}_{\succ}$ (up to
${\cal R}$-redundancy) is finite and $N^{*}_{0}$ is the set of clauses in
$N^{*}$ not containing $P$ then, by Theorem 11, the universal closure of the
conjunction of the clauses in $N^{*}_{0}$ is equivalent to $\exists P~{}N$.

###### Example 2

Consider a class of graphs described by the following set $N$ of constrained
$E$-clauses:

$\\{(1)\pi^{i}(u,v)||E(u,v),~{}~{}(2)\pi^{t}(u,w,v)||E(u,v)\rightarrow
E(u,w),~{}~{}(3)\pi^{e}(u,v)||\lnot E(u,v)\\}$

For arbitrary predicates $\pi^{i},\pi^{e}$ and $\pi^{t}$ we can generate with
$\mathit{HRes}^{E}_{\succ}$ an infinite set of clauses including, e.g., all
clauses of the form:

$(4_{n})~{}\pi^{i}(u,v)\land\pi^{t}(u,w_{1},v)\land\pi^{t}(u,w_{2},w_{1})\land\dots\land\pi^{t}(u,w_{n},w_{n-1})~{}||~{}E(u,w_{n})$

If we assume that $\pi^{i},\pi^{e},\pi^{t}$ satisfy the additional axioms
defining a theory ${\mathcal{T}}_{\pi}$:

$\begin{array}[]{lrrll}(c1)&\forall
u,v,w{}{}{}&\pi^{i}(u,v)\land\pi^{t}(u,w,v)&\rightarrow&\pi^{i}(u,w)\\\
(c2)&\forall
u,v,w{}{}{}&\pi^{e}(u,w)\land\pi^{t}(u,w,v)&\rightarrow&\pi^{e}(u,v)\\\
(c3)&\forall
u,v,w,x{}{}&\pi^{t}(u,w,v)\land\pi^{t}(u,x,w)&\rightarrow&\pi^{t}(u,x,v)\\\
\end{array}$

then all inferences by resolution between clauses (1) and (2), (2) and (3) are
${\mathcal{T}}_{\pi}$-redundant. The inferences between (2) and (2) are also
${\mathcal{T}}_{\pi}$-redundant: Consider a ground instance of such an
inference (the maximal literals are underlined):

$\pi^{t}(c_{1},c_{2},c_{3})||\underline{E(c_{1},c_{3})}\rightarrow
E(c_{1},c_{2})\quad\pi^{t}(c_{1},c_{3},c_{4})||E(c_{1},c_{4})\rightarrow\underline{E(c_{1},c_{3})}\over\pi^{t}(c_{1},c_{2},c_{3}),\pi^{t}(c_{1},c_{3},c_{4})||E(c_{1},c_{4})\rightarrow
E(c_{1},c_{2})$

The ground instance $C$ of (2)
$\pi^{t}(c_{1},c_{2},c_{4})||E(c_{1},c_{4})\rightarrow E(c_{1},c_{2})$ differs
from the conclusion of the inference above only in the background part and is
smaller than the first premise of the inference. If $(c3)$ holds then $C$
entails the conclusion of the inference above, which makes the inference
redundant w.r.t. ${\mathcal{T}}_{\pi}$.

Thus, only the inference of clauses (1) and (3) yields a non-redundant
resolvent:

$(4)\quad\pi^{i}(u,v,r_{1})\land\pi^{e}(u,v,r_{2})||\bot$

so $N^{*}=N\cup\\{(4)\\}$ is saturated up to ${\mathcal{T}}_{\pi}$-redundancy.
By Theorem 11, $N$ is satisfiable iff $\forall
u,v(\pi^{i}(u,v)\land\pi^{e}(u,v)\rightarrow\bot)$ is satisfiable w.r.t.
${\mathcal{T}}_{\pi}$.  $\blacksquare$

When modelling concrete situations, the predicates $\pi^{i},\pi^{e}$ and
$\pi^{t}$ might not be arbitrary, but might have definitions using other
symbols with given properties.

###### Example 3

The theory ${\mathcal{T}}_{\pi}$ might be actually described in a detailed
way. Let ${\bf C}(r_{1},r_{2})$ be a graph class described by the set $N$ of
axioms in Example 2, where $\pi^{i},\pi^{e},\pi^{t}$ are defined by the
axioms:

$\begin{array}[]{ll}{\sf Def}_{\pi}(r_{1},r_{2})=\\{&\forall
u,v~{}\pi^{i}(u,v)\leftrightarrow u{\neq}v\land d(u,v){\leq}r_{1}(u),\\\
&\forall u,v~{}\pi^{e}(u,v)\leftrightarrow d(u,v){>}r_{2}(u),\\\ &\forall
u,v,w~{}\pi^{t}(u,w,v)\leftrightarrow u{\neq}w\land
d(u,w){\leq}d(u,v)\\},\end{array}$

where $d$ is a distance or cost function. We can regard the theory extension
${\mathcal{T}}\subseteq{\mathcal{T}}_{\pi}={\mathcal{T}}\cup{\sf
Free}(r_{1},r_{2})\cup{\sf Def}_{\pi}$, where ${\mathcal{T}}$ is one of the
theories ${\mathcal{T}}^{u}_{d}$, $T^{p}_{d}$, ${\mathcal{T}}^{n}_{d}$ or
${\mathcal{T}}^{m}_{d}$ introduced in Theorem 8, and ${\sf Free}(r_{1},r_{2})$
the theory in which $r_{1},r_{2}$ are regarded as uninterpreted unary function
symbols. Therefore, ${\mathcal{T}}$ can be represented as a $\Psi$-local
extension of the disjoint combination of a theory of real numbers and of pure
equality, for a suitable closure operator. We can use the hierarchical
reduction in Theorem 4 to check that $(c1),(c2)$ and $(c3)$ are valid w.r.t.
${\mathcal{T}}$. $\blacksquare$

In applications we might not be interested in checking the satisfiability of
$N$ or the satisfiability of $\forall
u,v(\pi^{i}(u,v)\land\pi^{e}(u,v)\rightarrow\bot)$ w.r.t.
${\mathcal{T}}_{\pi}$, but in a specific model $\mathcal{A}$ satisfying
${\mathcal{T}}_{\pi}$ (we refer to it as “canonical model”).

This is the case, for instance, in the applications in wireless network theory
analyzed in Section 2: The vertices of the graphs considered in this context
are very often points in the Euclidian space, and the distance is a concrete
function which can be, for instance, the Euclidean metric, or a concrete cost
function – which might satisfy additional properties (for instance positivity
or symmetry). If we want to analyze such graph classes in full generality, we
might assume that some of the properties of some of the parameters are not
fully specified.

Let $\mathcal{A}$ be a model of a theory ${\mathcal{T}}$ describing properties
of function symbols in a set $\Sigma$ we want to model. We assume that
$\Sigma$ contains a set of “parameters” $\Sigma_{\sf par}$ (function symbols
whose properties are “underspecified” in ${\mathcal{T}}$). In some situations,
if we are given a set $N$ of constrained clauses, we might be interested in
obtaining (weakest) universal conditions $\Gamma$ on $\Sigma_{\sf par}$ such
that for every fixed model $\mathcal{A}$ of ${\mathcal{T}}$ which also
satisfies $\Gamma$, there exists an interpretation for $P$ in $\mathcal{A}$
for which $N$ is satisfied, i.e. $\mathcal{A}\models\exists P~{}N$. We present
a situation in which this is possible.

###### Theorem 13

Let ${\mathcal{T}}$ be a theory with signature $\Pi=(S,\Sigma,{\sf Pred})$,
$N$ a set of constrained $P$-clauses. Assume that the saturation $N^{*}$ of
$N$ up to ${\mathcal{T}}$-redundancy w.r.t. $\mathit{HRes}^{P}_{\succ}$ is
finite; let $N^{*}_{0}$ be the set of clauses in $N^{*}$ not containing $P$.

Let $\Sigma_{\sf par}\subseteq\Sigma$ be a set of parameters. Assume that one
of the following conditions holds:

  * (i)

${\mathcal{T}}$ allows quantifier elimination or

  * (ii)

${\mathcal{T}}_{0}\subseteq{\mathcal{T}}={\mathcal{T}}_{0}\cup{\mathcal{K}}$
is a local theory extension satisfying condition $({\sf Comp}^{\Psi}_{f})$ for
a suitable term closure operator $\Psi$ and ${\mathcal{T}}_{0}$ allows
quantifier elimination.

If (i) holds, we can use quantifier elimination and if (ii) holds then we can
use Algorithm 1 to obtain a (weakest) universal constraint $\Gamma$ on the
parameters such that every model $\mathcal{A}$ of ${\mathcal{T}}\cup\Gamma$ is
a model of (the universal closure of) $N^{*}_{0}$, hence
$\mathcal{A}\models\exists P~{}N$.

Proof: By the completeness of the hierarchical superposition calculus, $N$ is
satisfiable iff the set $N^{*}_{0}$ of clauses in $N^{*}$ which do not contain
$P$ is satisfiable. We denote by
$\forall{\overline{x}}N^{*}_{0}({\overline{x}})$ the formula represented by
the set of clauses $N^{*}_{0}$.

Let $\mathcal{A}$ be a model of ${\mathcal{T}}$. Assume that $\mathcal{A}$ is
not a model for $\forall{\overline{x}}N^{*}_{0}({\overline{x}})$. Then
$\exists{\overline{x}}\neg N^{*}_{0}({\overline{x}})$ is true in
$\mathcal{A}$. In particular, it follows that
${\mathcal{T}}\wedge\exists{\overline{x}}\neg N^{*}_{0}({\overline{x}})$ is
satisfiable. We can apply Algorithm 1 to construct a weakest universal formula
$\Gamma$ over the signature $\Sigma_{\sf par}$ with the property that
${\mathcal{T}}\cup\Gamma\cup\exists{\overline{x}}\neg
N^{*}_{0}({\overline{x}})$ is unsatisfiable, i.e. with the property that
${\mathcal{T}}\cup\Gamma\models\forall{\overline{x}}N^{*}_{0}({\overline{x}})$.
Then every model $\mathcal{B}$ of ${\mathcal{T}}$ which also satisfies the
constraints in $\Gamma$ is a model of
$\forall{\overline{x}}N^{*}_{0}({\overline{x}})$. $\Box$

###### Example 4

Consider again the situation described in Example 3. We show how one can use
Theorem 2 and Algorithm 1 to derive constraints $\Gamma$ on the parameters
$r_{1},r_{2}$ under which for every model $\mathcal{A}$ of
${\mathcal{T}}^{u}_{d}\cup\Gamma$

$\pi^{i}(u,v)\wedge\pi^{e}(u,v)=(u\neq v\land d(u,v)\leq
r_{1}(u))\wedge(d(u,v)>r_{2}(u))$

is unsatisfiable in $\mathcal{A}$ (we consider the case in which $d$ is an
uninterpreted function; other axioms for $d$ can be analyzed as well).

Note that the formula above is unsatisfiable in any model $\mathcal{A}$ of
${\mathcal{T}}^{u}_{d}$ whose support $A_{p}$ of sort ${\sf p}$ has
cardinality 1. If we only consider models $\mathcal{A}$ with $|A_{p}|\geq 2$
then we can proceed as follows:

Step 1: We purify the formula by introducing new constants:
$c_{d}:=d(u,v),c_{1}=r_{1}(u),c_{2}=r_{2}(u)$ and obtain: $(u\neq v\land
c_{d}\leq c_{1}\land c_{d}>c_{2})$.

Step 2: We quantify existentially all constants not denoting terms starting
with – or used as arguments of – $r_{1},r_{2}$ and obtain: $\exists v,\exists
c_{d}(u\neq v\land c_{d}\leq c_{1}\land c_{d}>c_{2})$.

Step 3: After quantifier elimination in a combination of ${\sf
LI}({\mathbb{R}})$ and the theory of sets with cardinality $\geq 2$ with
equality [36] we obtain $\Gamma_{1}(c_{1},c_{2},u):c_{2}<c_{1}$.666We can
consider only models $\mathcal{A}$ whose support of sort ${\sf p}$ is
infinite. The theory that formalizes this is the model completion of the
theory ${\cal E}$ of pure equality which allows quantifier elimination. We can
then use the method for quantifier elimination in combinations of theories
with QE described in [36].

Step 4: We replace the constants $c_{1},c_{2}$ with the terms they denote and
quantify the arguments existentially and obtain: $\exists
u(r_{2}(u)<r_{1}(u))$.

Step 5: We negate this condition and obtain: $\forall u(r_{1}(u)\leq
r_{2}(u))$. $\blacksquare$

###### Example 5

We find an axiomatization for the graph class ${\bf C}^{-}=\\{G^{-}\mid
G\in{\bf C}\\}$, when class ${\bf C}$ is described by the set $N$ of
constrained clauses in Example 2 and $\pi^{i},\pi^{e}$ and $\pi^{t}$ satisfy
conditions $(c1),(c2),(c3)$. Let $N^{*}=N\cup\\{(4)\\}$ be obtained by
saturating $N$ under $\mathit{HRes}^{E}_{\succ}$ up to redundancy. A graph
$H=(V,F)\in{\bf C}^{-}$ iff there exists a graph $G=(V,E)\in{\bf C}$ such that
$H=G^{-}$. This condition can be described by $M=N^{*}\cup{\sf Tr}(E,F)$,
where ${\sf Tr}(E,F)=\\{\forall x,y~{}(F(x,y)\leftrightarrow E(x,y)\wedge
E(y,x))\\}$, which can be written in the form of constrained clauses as:

${\sf Tr}(E,F)~{}=~{}\\{F(x,y)||E(x,y),~{}F(x,y)||E(y,x),~{}\neg F(x,y)||\neg
E(x,y)\lor\neg E(y,x)\\}$

To find an axiomatization for the class $\\{(V,F)\mid\exists(V,E)\in{\bf
C}\text{ with }(V,F)=(V,E)^{-}\\}$ we need to eliminate the second-order
quantifier from the formula $\exists E(N^{*}\cup{\sf Tr}(E,F))$.

The base theory is ${\mathcal{T}}\cup\mathit{UIF}_{F}$, the extension of
${\mathcal{T}}$ with the uninterpreted function symbol $F$, with signature
$\Pi_{F}=(\Sigma,{\sf Pred}\cup\\{F\\})$.

Since the background theory in this case is not arithmetic, and since the
method for second-order quantifier elimination implemented in SCAN [18] is
very similar to $\mathit{HRes}^{E}_{\succ}$, we used SCAN on the clause set
$N^{-}$:

$\begin{array}[]{llrl}(c1){}{}{}{}&\forall
u,v,w,x&\pi^{t}(u,w,v)\wedge\pi^{t}(u,x,w)&\rightarrow\pi^{t}(u,x,v)\\\
(c2)&\forall u,v,w&\pi^{i}(u,v)\land\pi^{t}(u,w,v)&\rightarrow\pi^{i}(u,w)\\\
(c3)&\forall
u,v,w&\pi^{e}(u,w)\land\pi^{t}(u,w,v)&\rightarrow\pi^{e}(u,v)\\\\[8.61108pt]
(1)&\forall u,v&\pi^{i}(u,v)&\rightarrow E(u,v)\\\ (2)&\forall
u,v&\pi^{e}(u,v)&\rightarrow\neg E(u,v)\\\ (3)&\forall
u,v,w&\pi^{t}(u,w,v)\land E(u,v)&\rightarrow E(u,w)\\\ (T1)&\forall
u,v&F(u,v)&\rightarrow E(u,v)\\\ (T2)&\forall u,v&F(u,v)&\rightarrow E(v,u)\\\
(T3)&\forall u,v&F(u,v)\wedge E(v,u)&\rightarrow F(u,v)\end{array}$

and obtained a set of clauses representing the formula containing axioms
$N_{{\mathcal{T}}}=\\{(c1),(c2),(c3),(4)\\}$, where

$(4)~{}~{}~{}~{}\forall u,v~{}\pi^{i}(u,v)\wedge\pi^{e}(u,v)\rightarrow\perp$

and axioms $N^{-}_{F}=\\{(F_{1}),\dots,(F_{6})\\}$:

$\begin{array}[]{llrl}(F_{1})&\forall x,y&F(x,y)&\rightarrow F(y,x)\\\
(F_{2})&\forall x,y&F(y,x)&\rightarrow\neg\pi^{e}(x,y)\\\ (F_{3})&\forall
x,y&F(x,y)&\rightarrow\neg\pi^{e}(x,y)\\\ (F_{4})&\forall
x,y&\pi^{i}(x,y)\land\pi^{i}(y,x)&\rightarrow F(y,x)\\\ (F_{5})&\forall
x,y,z&\pi^{i}(x,y)\land\pi^{t}(y,x,z)\land F(y,z)&\rightarrow F(x,y)\\\
(F_{6})&\forall x,y,z,u{}{}&\pi^{t}(x,y,z)\land F(x,z)\land\pi^{t}(y,x,u)\land
F(y,u)&\rightarrow F(y,x)\end{array}$

The universal closure $G$ of the conjunction of these clauses is equivalent
w.r.t. ${\mathcal{T}}\cup\mathit{UIF}_{F}$ to the formula $\exists
E(N^{*}\cup{\sf Tr}(E,F))$, and thus axiomatizes ${\bf C}^{-}$.

$\blacksquare$

###  5.2 Case 2: Finite representation of possibly infinite saturated sets

The saturation of a set $N$ of constrained $P$-clauses up to redundancy under
$\mathit{HRes}^{P}_{\succ}$ might be infinite. We here consider a very special
case under which a finite set of constrained $P$-clauses
$N=\\{\phi_{i}({\overline{x}})~{}||~{}C_{i}({\overline{x}})\mid
i=1,\dots,n\\}$ can have a saturation that can be finitely described: The
situation in which the set of clauses $\\{C_{1},\dots,C_{n}\\}$ can be
finitely saturated under ordered resolution.

###### Theorem 14

Let $N=\\{\phi_{i}({\overline{x}})||C_{i}({\overline{x}})\mid i=1,\dots,n\\}$
be a finite set of constrained $P$-clauses and
$N_{P}=\\{C_{1},\dots,C_{n}\\}$.

Assume that the saturation of $N_{P}$ under ordered resolution is finite,
$N_{P}^{*}=\\{C_{1},\dots,C_{n},C_{n+1},\dots,C_{n+k}\\}$, and the set ${\cal
I}_{P}$ of all possible inferences used for deriving these clauses is finite
and can be effectively described. If $\perp\not\in N_{P}^{*}$, then $\exists
P~{}N\equiv_{{\mathcal{T}}}\top$. Assume now that $\perp\in N_{P}^{*}$. Let
$\mathcal{A}$ be a model of ${\mathcal{T}}$, ${\mathcal{T}}_{\mathcal{A}}$ the
theory with $\mathcal{A}$ as canonical model (i.e.
${\mathcal{T}}_{\mathcal{A}}=Th(\mathcal{A})$). Let $N_{A}$ be the set of all
instances of $N$ in which the variables are replaced with elements in
$\mathcal{A}$ (seen as constants). Then:

  * (1)

The saturation $N^{*}_{A}$ of $N_{A}$ up to ${\cal
R}_{{\mathcal{T}}}$-redundancy can be described as
$N^{*}_{A}=\\{\mu^{\mathcal{A}}_{i}({\overline{a}})~{}||~{}C_{i}({\overline{a}})\mid
i=1,\dots,n+k,{\overline{a}}\text{ elements of }\mathcal{A}\\},$ where
$(\mu^{\mathcal{A}}_{i})_{i=1,n+k}$ are given by the minimal model of the
constrained Horn clauses777The definitions are presented in Appendix 0.C.
$CH_{N}$ w.r.t. ${\mathcal{T}}_{\mathcal{A}}$:

$\begin{array}[]{rl}CH_{N}=\\{&\phi_{i}({\overline{x}})\rightarrow\mu_{i}({\overline{x}})\mid
i\in\\{1,\dots,n\\}\\}\\\
\cup\\{&(\mu_{i}({\overline{x}})\wedge\mu_{j}({\overline{y}}))\sigma\rightarrow\mu_{k}({\overline{z}})\mid
C_{k}({\overline{z}})\text{ is obtained by a resolution }\\\ &\hskip
42.67912pt\text{ inference in }{\cal I}_{P}\text{ from
}C_{i}({\overline{x}})\text{ and }C_{j}({\overline{y}})\text{ with m.g.u.\
}\sigma\\}\\\
\cup\\{&\mu_{i}({\overline{x}})\sigma\rightarrow\mu_{k}({\overline{z}})\mid
C_{k}({\overline{z}})\text{ is obtained by a factorization inference }\\\
&\hskip 42.67912pt\text{ in }{\cal I}_{P}\text{ from
}C_{i}({\overline{x}})\text{ with m.g.u.\ }\sigma\\}.\end{array}$

  * (2)

Let $A^{\mu}$ be the extension of $\mathcal{A}$ with predicates
$(\mu_{i})_{i}$ whose interpretation is given by
$(\mu^{\mathcal{A}}_{i})_{i}$. Let $j$ be such that $\perp=C_{j}$. Then
$\mathcal{A}\models\exists P\,N$ iff
$CH_{N}{\cup}\\{{\neg}\mu_{j}({\overline{x}})\\}$ is satisfiable w.r.t.
${\mathcal{T}}_{\mathcal{A}}$.

Proof: Obviously, $CH_{N}$ is satisfiable (it has one trivial model, in which
all predicate symbols $\mu_{i}$ are true). If $\mathcal{A}$ is a model of
${\mathcal{T}}$, in this theorem we consider constrained Horn clauses over an
assertion language that has one canonical model, namely $\mathcal{A}$, i.e.
w.r.t. the corresponding theory ${\mathcal{T}}_{\mathcal{A}}$. In [12] it is
shown – using a canonical model construction – that every set $H$ of
constrained Horn clauses over an assertion language that has canonical models
has a unique least model.
This model is defined inductively by taking

$I_{0}{:=}\emptyset$ and

$I_{i+1}{:=}\\{r({\overline{a}}){\mid}{\sf body}(x){\rightarrow}r(x)\in
H,I_{i}\models_{\mathcal{A}}{\sf body}({\overline{a}}),{\overline{a}}\text{ is
a tuple of constants in }\mathcal{A}\\}$.

The construction stabilizes at the first limit ordinal $\omega$ with an
interpretation $I_{\omega}$; so the set of constrained Horn clauses $CH_{N}$
has a unique least model w.r.t. ${\mathcal{T}}_{\mathcal{A}}$.

This construction of this unique least model parallels the saturation process
for the set of ground instances of the clauses $N^{*}_{A}$; the saturated set
is:

$N^{*}_{A}=\bigcup_{i=1}^{n}\\{\xi^{k}_{i}({\overline{a}})||C_{i}({\overline{a}})\mid
k{\in}{\mathbb{N}},{\overline{a}}\text{ is a sequence of elements in
}\mathcal{A}\\}$

where $\xi^{k}_{i}({\overline{a}})||C_{i}({\overline{a}})$ are clauses in
$N_{A}$ or are obtained (in a finite number of steps) from clauses in $N_{A}$
using resolution and/or factorization. If we allow for potentially infinite
disjunctions it can be described as:

$N^{*}_{A}=\\{(\bigvee_{k\in{\mathbb{N}}}\xi^{k}_{i}({\overline{a}}))||C_{i}({\overline{a}}),i=1,{\dots},n+k,{\overline{a}}\text{
is a sequence of elements in }\mathcal{A}\\}$

and models for $\xi_{i}=\bigvee_{k\in{\mathbb{N}}}\xi^{k}_{i}$ can be built in
a similar way to the way the interpretations for $\mu_{i}$ in the minimal
model for $CH_{N}$ are built.

To prove (2) note that the following are equivalent:

>   1. (i)
>
> $\mathcal{A}\models\exists P~{}N$;
>
>   2. (ii)
>
> There exists a $\Pi^{\prime}$-structure $\mathcal{B}$ with
> $\mathcal{B}\models N$ and $\mathcal{B}_{|\Pi}=\mathcal{A}$;
>
>   3. (iii)
>
> $\mathcal{A}\models N^{*}_{0}$;
>
>   4. (iv)
>
> $\mathcal{A}^{A}\models(N^{*}_{0})_{A}=(N^{*}_{A})_{0}$;
>
>   5. (v)
>
>
> $\mathcal{A}^{A}\models\neg\bigvee_{k\in{\mathbb{N}}}\xi_{j}({\overline{a}})$
> for every sequence ${\overline{a}}$ of elements in $\mathcal{A}$;
>
>   6. (vi)
>
> $\mathcal{A}^{A}\models\neg\mu^{\mathcal{A}}_{j}({\overline{a}})$ for every
> sequence ${\overline{a}}$ of elements in $\mathcal{A}$;
>
>   7. (vii)
>
>
> $\mathcal{A}^{\mu}\models\forall{\overline{x}}~{}\neg\mu_{j}({\overline{x}})$;
>
>   8. (viii)
>
> $CH_{N}\cup\\{\neg\mu_{j}({\overline{x}})\\}$ is satisfiable w.r.t.
> ${\mathcal{T}}_{\mathcal{A}}$;
>
>

where $N^{*}_{0}$ ($N^{*}_{A})_{0}$ is the set of all clauses in $N^{*}$
($N^{*}_{A}$) which do not contain $P$.

(i) and (ii) are equivalent by definition; (ii) and (iii) by Theorem 11; (iii)
and (iv) by Lemma 10; (iv) and (v) by the fact that the conjunction of all
clauses of $(N^{*}_{A})_{0}$ can be succinctly represented by taking a
possibly infinite disjunction in the constraint in front of $\perp$; (v) and
(vi) are equivalent due to (1); (vi) and (vii) by definition.

(vii) $\Rightarrow$ (viii): By assumption (vii),
$\mathcal{A}^{\mu}\models\forall{\overline{x}}~{}\neg\mu_{j}({\overline{x}})$.
Since $(\mu^{\mathcal{A}}_{i}({\overline{x}}))_{i}$ are the interpretations of
$\mu_{i}$ in the least model for $CH_{N}$ w.r.t. ${\mathcal{T}}_{A}$ it
follows that $\mathcal{A}^{\mu}\models
CH_{N}\cup\\{\forall{\overline{x}}~{}\neg\mu_{j}({\overline{x}})\\}$, hence
$CH_{N}\cup\\{\forall{\overline{x}}~{}\neg\mu_{j}({\overline{x}})\\}$ is
satisfiable w.r.t. ${\mathcal{T}}_{\mathcal{A}}$.

(viii) $\Rightarrow$ (vii): Assume now that
$CH_{N}\cup\\{\forall{\overline{x}}~{}\neg\mu_{j}({\overline{x}})\\}$ is
satisfiable w.r.t. ${\mathcal{T}}_{\mathcal{A}}$, i.e. there exists an
expansion $\mathcal{B}$ of $\mathcal{A}$ with interpretations for the
predicates $\mu_{i}$ such that $\mathcal{B}\models
CH_{N}\cup\\{\forall{\overline{x}}~{}\neg\mu_{j}({\overline{x}})\\}$. Let
$M^{\mathcal{A}}$ be the least model of
$CH_{N}\cup\\{\neg\mu_{j}({\overline{x}})\\}$. It can be constructed with the
canonical construction explained before, by considering the set
$(CH_{N}\cup\\{\neg\mu_{j}({\overline{x}})\\})_{A}$ of instances of clauses in
$CH_{N}\cup\\{\neg\mu_{j}({\overline{x}})\\}$ with constants in $\mathcal{A}$
and marking $\mu_{i}({\overline{a}})$ as true if we have a rule ${\sf
body}(x)\rightarrow\mu_{i}(x)$. Note that $\\{\neg\mu_{j}({\overline{x}})\\}$
does not contribute to this model building process. This means that the least
model of $CH_{N}\cup\\{\neg\mu_{j}({\overline{x}})\\}$ is actually the least
model of $CH_{N}$, hence in the least model of $CH_{N}$ the formula
$\forall{\overline{x}}~{}\neg\mu_{j}({\overline{x}})$ is true, which means
that $A^{\mu}\models\forall{\overline{x}}~{}\neg\mu_{j}({\overline{x}})$.
$\Box$

If ${\mathcal{T}}$ has only one (canonical) model and is supported by $\mu Z$
[23], we can use $\mu Z$ for checking whether $N$ is satisfiable888If the set
$N$ of constrained $P$-clauses (hence the set of constrained Horn clauses
$CH_{N}$) contains at least one parameter then $\mu Z$ often returns
“unknown”. In addition, if $\mu Z$ can prove satisfiability of
$CH_{N}\cup\\{\neg\mu_{j}({\overline{x}})\\}$ for a non-parametric problem,
the model it returns is not guaranteed to be minimal in general, and cannot be
used for representing the saturated set of clauses. By Theorem 14 (2),
satisfiability of $CH_{N}\cup\\{\neg\mu_{j}({\overline{x}})\\}$ is sufficient
for proving the satisfiability of $N$ in this case..

###### Example 6

Consider the set $N$ consisting of the following constrained $P$-clauses:

$(1)~{}x=y||P(x,y),~{}~{}(2)~{}y=x+1||P(y,z)\rightarrow
P(x,z),~{}~{}(3)~{}n(x,y)||\neg P(x,y)$

over the theory of integers without multiplication with model $\mathbb{Z}$.
Saturating $N$ without any simplification strategy yields the infinite set
$N^{*}$ consisting of:

$\begin{array}[]{llllll}(1_{k})&\displaystyle{\bigwedge_{i=1}^{k}}x_{i}{=}x_{i-1}{+}1~{}||~{}P(x_{0},x_{k})&&(2_{k})&\displaystyle{\bigwedge_{i=1}^{k}}x_{i}{=}x_{i-1}{+}1~{}||~{}P(x_{k},z)\rightarrow
P(x_{0},z)&\\\
(3_{k})&n(x_{0},y)\wedge\displaystyle{\bigwedge_{i=1}^{k}}x_{i}{=}x_{i-1}{+}1~{}||~{}\neg
P(x_{k},y)&&(4_{k})&\displaystyle{\bigwedge_{i=1}^{k}}x_{i}{=}x_{i-1}{+}1\wedge
n(x_{0},x_{k})~{}||\perp,k\in{\mathbb{N}}\end{array}$

(i) We first show how Theorem 14 can be used in this case. Let
$N_{P}=\\{C_{1},C_{2},C_{3}\\}$, where
$C_{1}=P(x_{1},y_{1}),C_{2}=P(y_{2},z_{1})\rightarrow P(x_{1},z_{1}),$ and
$C_{3}=\neg P(x_{3},y_{3})$. We can saturate $N_{P}$ as follows: From $C_{1}$
and $C_{3}$ we can derive $C_{4}=\perp$; from $C_{1}$ and $C_{2}$ we can
derive a clause of type $C_{1}$, from $C_{2}$ and $C_{2}$ a clause of type
$C_{2}$ and from $C_{2}$ and $C_{3}$ a clause of type $C_{3}$. We obtain
$N_{P}^{*}=\\{C_{1},C_{2},C_{3},C_{4}\\}$. By Theorem 14, the saturation of
$N$ is $N^{*}$:

$\\{\mu_{1}(x,y)||P(x,y),\,\mu_{2}(x,y,z)||P(y,z){\rightarrow}P(x,z),\,\mu_{3}(x,y)||\neg
P(x,y),\,\mu_{4}(x,y)||\perp\\}$,

where $\mu_{1},\mu_{2},\mu_{3},\mu_{4}$ are given by the minimal model ${\sf
M}$ of $CH_{N}$:

$\begin{array}[]{r@{}c@{}l}CH_{N}&=\\{&x=y\rightarrow\mu_{1}(x,y),\quad
y=x+1\rightarrow\mu_{2}(x,y,z),\quad n(x,y)\rightarrow\mu_{3}(x,y),\\\
&&\mu_{1}(x,y)\wedge\mu_{2}(u,x,y)\rightarrow\mu_{1}(u,y),\quad\mu_{3}(x,y)\wedge\mu_{2}(x,u,y)\rightarrow\mu_{3}(u,y),\\\
&&\mu_{2}(x,y,z)\wedge\mu_{2}(u,x,z)\rightarrow\mu_{2}(u,y,z),\quad\mu_{1}(x,y)\wedge\mu_{3}(x,y)\rightarrow\mu_{4}(x,y)\\}\end{array}$

$\mu Z$ cannot check whether this set of Horn constraints is satisfiable
because of the parameter $n$. If we replace $n(x,y)$ with $x>y$ $\mu Z$ yields
the following solution:

$\mu_{1}(x,y)=x\leq
y,~{}\mu_{2}(x,y,z)=(y>z)\lor(x<z),~{}\mu_{3}(x,y)=x>y,~{}\mu_{4}=\perp$.

(ii) Alternatively, note that if we use the fact that $\exists x_{1}\dots
x_{k-1}~{}\bigwedge_{i=1}^{k}x_{i}{=}x_{i-1}{+}1\equiv_{{\mathcal{T}}}x_{k}=x_{0}+k$
we obtain an infinite set of clauses consisting of:

$\begin{array}[]{llllll}(1^{\prime}_{k})&y=x+k||P(x,y)&&(2^{\prime}_{k})&y=x+k||P(y,z)\rightarrow
P(x,z)&\\\ (3^{\prime}_{k})&n(x,y)\wedge z=x+k||\neg
P(z,y)&&(4^{\prime}_{k})&y=u+k\wedge
n(u,y)||\perp&k\in{\mathbb{N}}\end{array}$

If we regard $k$ in each clause as a universally quantified variable (with
additional condition $k\geq 0$) we obtain:

$\begin{array}[]{ll}N^{\prime}=\\{&y=x+k\wedge k\geq 0||P(x,y),~{}y=x+k\wedge
k\geq 0||P(y,z),\\\ &n(x,y)\wedge z=x+k\wedge k\geq 0||\neg
P(z,y),~{}y=u+k\wedge k\geq 0\wedge n(u,y)||\perp\\}.\end{array}$

If $\mathcal{A}=({\mathbb{Z}},n_{A})$, $\mathcal{A}\models\exists
P~{}N^{\prime}$ iff $\mathcal{A}\models\forall u,y,k~{}(k\geq 0\wedge
y=u+k\rightarrow\neg n(u,y))$.

Remark: In linear integer arithmetic the interpretations of $(\mu_{i})_{1\leq
i\leq 4}$ in the minimal model of $CH_{N}$ w.r.t. the model
$\mathcal{A}=({\mathbb{Z}},n_{A})$, for a fixed interpretation of $n$ (say as
$n_{A}(x,y)=(x>y)$) are: $\mu_{1}(x,y)=\mu_{2}(x,y,z)=\exists k(k\geq 0\wedge
y=x+k)$, $\mu_{3}(x,y)=\exists z\exists k(n(z,y)\wedge x=z+k)$ and
$\mu_{4}(x,y)=\mu_{1}(x,y)\wedge\mu_{3}(x,y)$.  $\blacksquare$

Example 6(ii) uses acceleration techniques, in particular the following
result:

######  Theorem 15 ([14, 17])

Let $N$ be a set of constrained clauses of the form:

$N=\\{\phi_{0}({\overline{x}})~{}||~{}R({\overline{x}}),\quad\phi({\overline{x}})\wedge{\overline{y}}=M\cdot{\overline{x}}+{\overline{v}}~{}||~{}R({\overline{x}})\rightarrow
R({\overline{y}})\\}$

where ${\overline{x}},{\overline{y}}$ describe vectors of $n$ variables,
${\overline{v}}$ a vector of $n$ constants in ${\mathbb{Z}}$, $\phi_{0}$ is a
condition expressible in Presburger arithmetic and $M=(m_{i,j})_{1\leq i,j\leq
n}$ is a $n\times n$ matrix over ${\mathbb{Z}}$, and
$\phi(x_{1},\dots,x_{n})=\bigwedge_{i=1}^{k}(\sum_{j=1}^{n}a_{ij}x_{j}\leq
b_{i})$, where $a_{ij},b_{i}\in{\mathbb{Z}}$.

The interpretation of $R$ in the minimal model of $N$ is Presburger definable
if $\left<M\right>=\\{M^{n}\mid n\in{\mathbb{N}}\\}$ is finite. If $\phi=\top$
then the interpretation of $R$ in the minimal model of $N$ is Presburger
definable if and only if $\left<M\right>=\\{M^{n}\mid n\in{\mathbb{N}}\\}$ is
finite.

Acceleration techniques have been investigated e.g. for fragments of theories
of arrays with read and write in the presence of iterators and selectors in
[4]. Similar ideas are used in the superposition calculus in [16, 27], and in
approaches which combine superposition and induction [31] or use solutions for
recurrences in loop invariant generation [33, 32]. We plan to analyze such
aspects in future work.

##  6 Checking Entailment

Let ${\mathcal{T}}$ be a theory with signature $\Pi=(S,\Sigma,{\sf Pred})$,
and let ${\overline{P}}_{1}=P^{1}_{1},\dots,P^{1}_{n_{1}}$ and
${\overline{P}}_{2}=P^{2}_{1},\dots,P^{2}_{n_{2}}$ be finite sequences of
different predicate symbols with $P^{i}_{j}\not\in{\sf Pred}$, and
$\Pi_{i}=(\Sigma,{\sf Pred}\cup\\{P^{i}_{j}\mid 1\leq j\leq n_{i}\\})$ for
$i=1,2$.

Let $F_{1}$ be a universal $\Pi_{1}$-formula and $F_{2}$ be a universal
$\Pi_{2}$-formula. We analyze the problem of checking whether
“$\exists{\overline{P}}_{1}~{}F_{1}$ entails
$\exists{\overline{P}}_{2}~{}F_{2}$ w.r.t. ${\mathcal{T}}$” holds.

###### Example 7

Such questions arise in the graph-theoretic problems discussed in Section 2.
Let ${\bf A}$ be a class of graphs described by axioms ${\sf Ax}_{A}$ and
${\bf B}$ be a class of graphs described by axioms ${\sf Ax}_{B}$. Let
${\mathcal{T}}$ be a theory used for expressing these axioms. Consider the
$\cdot^{+}$ and $\cdot^{-}$ transformations described in Section 2. Then ${\bf
A}^{+}\subseteq{\bf B}^{-}$ (i.e. for every graph $H=(V,F)\in{\bf A}^{+}$ we
have $H\in{\bf B}^{-}$) if and only if $\exists E_{A}~{}({\sf Ax}_{A}\wedge
Tr^{+}(E_{A},F))\models_{{\mathcal{T}}}\exists E_{B}~{}({\sf Ax}_{B}\wedge
Tr^{-}(E_{B},F))$.  $\blacksquare$

Assume that there exist $\Pi$-formulae $G_{1}$ and $G_{2}$ such that
$G_{1}\equiv_{{\mathcal{T}}}\exists{\overline{P}}_{1}F_{1}$ and
$G_{2}\equiv_{{\mathcal{T}}}\exists{\overline{P}}_{2}F_{2}$. Such formulae can
be found either by saturation999We can iterate the application of
$\mathit{HRes}^{P}_{\succ}$ for variables $P^{i}_{1},\dots,P^{i}_{n}$ (in this
order). This corresponds to a variant of ordered resolution which we denote by
$\mathit{HRes}^{P^{i}_{1},\dots,P^{i}_{n}}_{\succ}$; if saturation terminates
the conjunction of clauses not containing $P^{i}_{1},\dots,P^{i}_{n}$ is
equivalent to $\exists P^{i}_{1},\dots,P^{i}_{n}~{}N_{F_{i}}$, where
$N_{F_{i}}$ is the clause form of $F_{i}$. by successively eliminating
$P_{1},\dots,P_{n}$, or by using acceleration techniques or other methods. In
this case,
$\exists{\overline{P}}_{1}~{}F_{1}\models_{{\mathcal{T}}}\exists{\overline{P}}_{2}~{}F_{2}$
iff $G_{1}\models_{{\mathcal{T}}}G_{2}$ (which is the case iff
$G_{1}\wedge\neg G_{2}\models_{{\mathcal{T}}}\perp$).

The problem of checking whether $G_{1}\wedge\neg
G_{2}\models_{{\mathcal{T}}}\perp$ is in general undecidable, even if $G_{1}$
and $G_{2}$ are universal formulae and ${\mathcal{T}}$ is the extension of
Presburger arithmetic or real arithmetic with a new function or predicate
symbol (cf. [44]).

If $G_{1}\wedge\neg G_{2}$ is in a fragment of ${\mathcal{T}}$ for which
checking satisfiability is decidable, then we can effectively check whether
$\exists{\overline{P}}_{1}~{}F_{1}\models_{{\mathcal{T}}}\exists\overline{P}_{2}~{}F_{2}$.
This is obviously the case when ${\mathcal{T}}$ is a decidable theory. We will
show that a similar condition can be obtained for local theory extensions of
theories allowing quantifier elimination if $G_{1}$ and $G_{2}$ are universal
formulae and the extensions satisfy a certain “flatness property” which allows
finite complete instantiation and that in both cases we can also generate
constraints on “parameters” under which entailment holds.

###### Theorem 16

Assume that there exist $\Pi$-formulae $G_{1}$ and $G_{2}$ such that
$G_{1}\equiv_{{\mathcal{T}}}\exists{\overline{P}}_{1}F_{1}$ and
$G_{2}\equiv_{{\mathcal{T}}}\exists{\overline{P}}_{2}F_{2}$. If
${\mathcal{T}}$ is a decidable theory then we can effectively check whether
$\exists{\overline{P}}_{1}~{}F_{1}\models_{{\mathcal{T}}}\exists{\overline{P}}_{2}~{}F_{2}$.
If ${\mathcal{T}}$ has quantifier elimination and the formulae $F_{1},F_{2}$
contain parametric constants, we can use quantifier elimination in
${\mathcal{T}}$ to derive conditions on these parameters under which
$\exists{\overline{P}}_{1}\,F_{1}\models_{{\mathcal{T}}}\exists{\overline{P}}_{2}\,F_{2}$.

###### Theorem 17

Assume that there exist universal $\Pi$-formulae $G_{1}$ and $G_{2}$ such that
$G_{1}\equiv_{{\mathcal{T}}}\exists{\overline{P}}_{1}F_{1}$ and
$G_{2}\equiv_{{\mathcal{T}}}\exists{\overline{P}}_{2}F_{2}$, and that
${\mathcal{T}}={\mathcal{T}}_{0}\cup{\mathcal{K}}$, where ${\mathcal{T}}_{0}$
is a decidable theory with signature $\Pi_{0}=(S_{0},\Sigma_{0},{\sf
Pred}_{0})$ where $S_{0}$ is a set of interpreted sorts and ${\mathcal{K}}$ is
a set of (universally quantified) clauses over $\Pi=(S_{0}\cup
S_{1},\Sigma_{0}\cup\Sigma_{1},{\sf Pred}_{0}\cup{\sf Pred}_{1})$, where (i)
$S_{1}$ is a new set of uninterpreted sorts, (ii) $\Sigma_{1},{\sf Pred}_{1}$
are sets of new function, resp. predicate symbols which have only arguments of
uninterpreted sort $\in S_{1}$, and all function symbols in $\Sigma_{1}$ have
interpreted output sort $\in S_{0}$. Assume, in addition, that all variables
and constants of sort $\in S_{1}$ in ${\mathcal{K}},G_{1}$ and $\neg G_{2}$
occur below function symbols in $\Sigma_{1}$. Then:

  * (1)

We can use the decision procedure for ${\mathcal{T}}_{0}$ to effectively check
whether $G_{1}\wedge\neg G_{2}\models_{{\mathcal{T}}}\perp$ (hence if
$\exists{\overline{P}}_{1}~{}F_{1}\models_{{\mathcal{T}}}\exists{\overline{P}}_{2}~{}F_{2}$).

  * (2)

If ${\mathcal{T}}_{0}$ allows quantifier elimination and the formulae
$F_{1},F_{2}$ (hence also $G_{1},G_{2}$) contain parametric constants and
functions, we can use Algorithm 1 for obtaining constraints on the parameters
under which
$\exists{\overline{P}}_{1}~{}F_{1}\models_{{\mathcal{T}}}\exists{\overline{P}}_{2}~{}F_{2}$.

Proof: Let $C$ be the set of constants of uninterpreted sort $s\in S_{1}$
occurring in ${\mathcal{K}},G_{1}$ and $\neg G_{2}$. Note that
$G_{1}\wedge\neg G_{2}$ is satisfiable w.r.t.
${\mathcal{T}}={\mathcal{T}}_{0}\cup{\mathcal{K}}$ iff $({\mathcal{K}}\wedge
G_{1})^{[C]}\wedge\neg G_{2}$ is satisfiable, where $({\mathcal{K}}\wedge
G_{1})^{[C]}$ is the set of all instances of ${\mathcal{K}}\wedge G_{1}$ in
which the variables of sort $s\in S_{1}$ are replaced with constants of sort
$s$ in $C$. (1) The hierarchical reasoning method in Theorem 4 allows us to
reduce testing whether $G_{1}\wedge\neg G_{2}\models_{{\mathcal{T}}}\perp$ to
a satisfiability test w.r.t. ${\mathcal{T}}_{0}$. (2) If ${\mathcal{T}}_{0}$
allows QE we can use Theorem 2. $\Box$

###  6.1 Application: Checking class inclusion

We illustrate how Theorem 17 can be used for checking one of the class
inclusions mentioned in Section 2.

###### Example 8

Let ${\bf QUDG}(r)=({\bf MinDG}(r)\cap{\bf MaxDG}(1))^{-}$, be axiomatized by
${\sf MinDG}(r)\wedge{\sf MinDG}(1)\wedge{\sf Tr^{-}}(E,F)$, where:

$\begin{array}[]{llll}{\sf MinDG}(r):&\forall x,y&\pi^{i}(x,y,r)\rightarrow
E(x,y)&\quad\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\text{
where }\pi^{i}(x,y,r)=x\neq y\land d(x,y)\leq r(x)\\\ {\sf MaxDG}(1):&\forall
x,y&\pi^{e}(x,y)\rightarrow\lnot
E(x,y)&\quad\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\text{
where }\pi^{e}(x,y)=d(x,y)>1\\\ {\sf Tr^{-}}(E,F):&\forall
x,y&(F(x,y)\leftrightarrow E(x,y)\land E(y,x))&.\end{array}$

We want to check whether ${\bf A}(r)\subseteq{\bf B}(r)$, where ${\bf
A}(r)={\bf QUDG}(r)$ and ${\bf B}(r)=({\bf MinDG}(r)\cap{\bf MaxDG}(1))^{+}$
is described by ${\sf MinDG}(r)\wedge{\sf MinDG}(1)\wedge{\sf Tr^{+}}(E,F)$.

We obtain the axiomatization $G_{1}$ by eliminating $E$ from

$\exists E({\sf MinDG}(r)\wedge{\sf MinDG}(1)\wedge{\sf Tr^{-}}(E,F))$

and the axiomatization $G_{2}$ by eliminating $E$ from

$\exists E({\sf MinDG}(r)\wedge{\sf MinDG}(1)\wedge{\sf Tr^{+}}(E,F)).$

$\begin{array}[]{lll}&G_{1}&\\\ \hline\cr\forall
x,y{}&\pi^{i}(x,y,r)\land\pi^{e}(x,y)&\rightarrow~{}~{}\perp\\\ \forall
x,y&\pi^{i}(x,y)\land\pi^{i}(y,x)&\rightarrow~{}~{}F(y,x)\\\ \forall
x,y&\pi^{e}(x,y)&\rightarrow\neg F(x,y)\\\ \forall
x,y&\pi^{e}(x,y)&\rightarrow\neg F(y,x)\\\ \forall
x,y&F(x,y)&\rightarrow~{}~{}F(y,x)\\\ &&\end{array}$
$\begin{array}[]{lll}&G_{2}&\\\ \hline\cr\forall
x,y{}&\pi^{i}(x,y,r)\land\pi^{e}(x,y)&\rightarrow~{}~{}\perp\\\ \forall
x,y&\pi^{e}(x,y)\land\pi^{e}(y,x)&\rightarrow\neg F(y,x)\\\ \forall
x,y&\pi^{i}(x,y)&\rightarrow~{}~{}F(x,y)\\\ \forall
x,y&\pi^{i}(x,y)&\rightarrow~{}~{}F(y,x)\\\ \forall
x,y&F(x,y)&\rightarrow~{}~{}F(y,x)\\\ \forall x&\pi^{e}(x,x)&\rightarrow\neg
F(x,x)\end{array}$

We check whether $G_{1}\models_{{\mathcal{T}}}G_{2}$, i.e. whether
$G_{1}\wedge\neg G_{2}$ is unsatisfiable w.r.t. ${\mathcal{T}}$, where $\neg
G_{2}$ is the disjunction of the following ground formulae (we ignore the
negation of the first clause obviously implied by $G_{1}$):

$\begin{array}[]{llllllll}~{}(g_{1})&\pi^{e}(a,b)\wedge\pi^{e}(b,a)\wedge
F(b,a)&&(g_{2})&\pi^{e}(a,a)\wedge F(a,a)&&(g_{3})&F(a,b)\wedge\neg F(b,a)\\\
~{}(g_{4})&\pi^{i}(a,b)\wedge\neg F(a,b)&&(g_{5})&\pi^{i}(a,b)\wedge\neg
F(b,a)\\\ \end{array}$

By Theorem 17 (2), we can consider the set of all instances of $G_{1}$ in
which the variables of sort ${\sf p}$ are replaced with the constants $a,b$,
then use a method for checking ground satisfiability of $G_{1}[T]\wedge g_{i}$
w.r.t. ${\mathcal{T}}^{u}_{d}$ ($d$ is uninterpreted), ${\mathcal{T}}^{p}_{d}$
($d$ is positive), ${\mathcal{T}}^{s}_{d}$ ($d$ is symmetric) and
${\mathcal{T}}^{m}_{d}$ ($d$ is a metric). For this, we use H-PILoT [29] in
which we enforce the right instantiation by adding relevant instances to the
query. This allows us to check that $G_{1}[T]\wedge g_{i}$ is unsatisfiable
for $i\in\\{1,2,3\\}$, but satisfiable for $i\in\\{4,5\\}$ (this is so for all
four theories).

For cases 4 and 5 we use an implementation of Algorithm 1, sehpilot to derive
conditions on parameters under which $G_{1}[T]\wedge g_{i}$ is unsatisfiable.
We give here two examples:

(1) We consider $d$ and $r$ to be parameters, i.e. we eliminate only $F$ from
$G_{1}[T]\wedge g_{i}$. For ${\mathcal{T}}^{m}_{d}$ we get the condition

$C^{d,r}=\forall x,y(x\neq y\wedge d(x,y)\leq 1\wedge d(x,y)\leq
r(x)\rightarrow d(y,x)\leq r(y)).$

(2) We consider only $r$ to be a parameter, i.e. we eliminate the symbols $F$
and $d$. For ${\mathcal{T}}^{s}_{d}$ we obtain the condition

$C^{r}=\forall x,y(r(y)<1\wedge x\neq y\rightarrow r(y)\geq r(x)).$

This condition holds e.g. if $r(x)=r(y)$ for all $x,y$, i.e. if $r$ is a
constant function. Adding this as an additional condition we get
unsatisfiability of $G_{1}[T]\wedge g_{i}$ with $i\in\\{4,5\\}$ for
${\mathcal{T}}^{m}_{d}$ and ${\mathcal{T}}^{s}_{d}$, but not for
${\mathcal{T}}^{u}_{d}$ and ${\mathcal{T}}^{p}_{d}$.

Checking the other inclusion We now check whether ${\bf B}(r)\subseteq{\bf
A}(r)$, where ${\bf A}(r)={\bf QUDG}(r)$ and ${\bf B}(r)=({\bf
MinDG}(r)\cap{\bf MaxDG}(1))^{+}$. We have the axiomatizations $G_{1}$,
$G_{2}$ for the two classes.

We check whether $G_{2}\models_{{\mathcal{T}}}G_{1}$, i.e. whether
$G_{2}\wedge\neg G_{1}$ is unsatisfiable w.r.t. ${\mathcal{T}}$, where $\neg
G_{1}$ is the disjunction of the following ground formulae (we ignore the
negation of the first clause obviously implied by $G_{2}$):

$\begin{array}[]{llllllll}~{}(g_{1})&\pi^{i}(a,b)\wedge\pi^{i}(b,a)\wedge\neg
F(b,a)&&(g_{2})&\pi^{e}(a,b)\wedge F(a,b)\\\ ~{}(g_{3})&\pi^{i}(a,b)\wedge\neg
F(b,a)&&(g_{4})&F(a,b)\wedge\neg F(b,a)\\\ \end{array}$

We use H-PILoT for checking ground satisfiability of $G_{2}[T]\wedge g_{i}$
w.r.t.
${\mathcal{T}}\in\\{{\mathcal{T}}^{u}_{d},{\mathcal{T}}^{p}_{d},{\mathcal{T}}^{s}_{d},{\mathcal{T}}^{m}_{d}\\}$.
For $T_{s}$ and $T_{m}$ we obtain unsatisfiability of $G_{2}[T]\wedge g_{i}$
for $i\in\\{1,2,3,4\\}$, thus we have proved that the inclusion holds for
these two theories. For $T_{p}$ and $T_{u}$ we get satisfiability for cases 2
and 3. We use Algorithm 1 to obtain conditions on parameters such that
$G_{2}[T]\wedge g_{2}$ and $G_{2}[T]\wedge g_{3}$ is unsatisfiable.

If we consider $d$ and $r$ to be parameters, i.e. we eliminate only $F$ from
$G_{1}[T]\wedge g_{i}$ we obtain the condition

$C^{d,r}=\forall x,y(d(y,x)>1\lor d(x,y)\leq 1\lor d(x,y)\leq r(x)\lor x=y).$

It is easy to see that this condition holds if $d$ is symmetric.
$\blacksquare$

##  7 Tests

We tested the methods we proposed on several examples. We used various tools
for solving the various types of symbol elimination considered in this paper.

Second-order quantifier elimination. Since the implementations of the
hierarchical superposition calculus we are aware of have as background theory
linear arithmetic and in our examples we had more complex theories, we used a
form of abstraction first: We renamed the constraints over more complex
theories with new predicate symbols, and used SCAN [18] for second-order
quantifier elimination. SCAN performs second-order quantifier elimination in
first-order logic. It takes as input a formula of the form
$F(P_{1},\dots,P_{n})$ containing predicate symbols $P_{1},\dots,P_{n}$ and
applies a clause form transformation, ordered resolution and de-Skolemization
on this formula. In case of termination and if de-Skolemization is possible,
it returns a first-order formula equivalent to $\exists P_{1},\dots\exists
P_{n}F(P_{1},\dots,P_{n})$, which does not contain the predicate symbols
$P_{1},\dots,P_{n}$.

Satisfiability checking and property-directed symbol elimination. For
satisfiability checking we used H-PILoT [29] (after preparing the input such
that the instances that have to be used are clear for the prover). H-PILoT
carries out a hierarchical reduction to the base theory. Standard SMT provers
or specialized provers can be used for testing the satisfiability of the
formulae obtained after the reduction. H-PILoT uses eager instantiation and
the hierarchical reduction, so provers like CVC4 [6] or Z3 [13, 11] are in
general faster in proving unsatisfiability. The advantage of using H-PILoT is
that knowing the instances needed for a complete instantiation allows us to
correctly detect satisfiability (and generate models) in situations in which
e.g. CVC4 returns “unknown”, and use property-directed symbol elimination to
obtain additional constraints on parameters which ensure unsatisfiability.

For obtaining the constraints on parameters we used the method described in
Algorithm 1 proposed in [41] which was implemented in sehpilot for the case in
which the base theory is the theory of real-closed fields. sehpilot (Symbol
Elimination with H-PILoT) receives a list of parameters as a command line (and
possibly a list of already existing constraints on these parameters) and uses
H-PILoT for the hierarchical reduction to a problem in the base theory (Step 1
in Algorithm 1) and for generating a corresponding REDLOG file. The constants
are classified as required in Step 2 of Algorithm 1 and the REDLOG file is
changed accordingly such that only those symbols that are not a parameter or
argument of a parameter are considered to be existentially quantified. Redlog
is used for quantifier elimination (Step 3 of Algorithm 1); then the constants
contained in the obtained formula are replaced back with the terms they
represent (Step 4). Finally, the formula obtained this way is negated (Redlog
is used for further simplifications).

The way we used these tools is illustrated on some tests in Appendix 0.A.

##  8 Conclusions

In this paper, we analyzed possibilities of combining general second-order
symbol elimination and property-directed symbol elimination. For eliminating
existentially quantified predicates from universal first-order formulae we
used a constrained resolution calculus (obtained from specializing the
hierarchical superposition calculus). We analyzed situations in which
saturation terminates and two possibilities of obtaining finite
representations also in cases in which saturation might not terminate: (i)
Using an encoding of the constraints of the saturated set of clauses as
smallest fixpoints of certain families of constrained Horn clauses and (ii)
using acceleration. For checking the satisfiability of families of constrained
Horn clauses we used the fixpoint package of Z3 [23].

If the saturation terminates, or the infinite saturated set of clauses has a
finite representation, we can use the obtained set of clauses for checking
entailment. We proved a $\Psi$-locality property for a class of formulae; this
allowed us to use the prover H-PILoT (after preparing the input such that the
instances that have to be used are clear) for analyzing the satisfiability of
formulae w.r.t. models in a theory ${\mathcal{T}}$ and for checking entailment
between formulae. Property-based symbol elimination proved useful for
obtaining (weakest) constraints $\Gamma$ on “parameters” used in the
description of the theory ${\mathcal{T}}$ such that satisfiability or
entailment is guaranteed in models satisfying $\Gamma$.

In future work we would like to find possibilities of identifying situations
in which second-order quantifier elimination using resolution terminates and
study possibilities of using (and generalizing) methods based on constrained
Horn clauses or acceleration for obtaining finite representations of
potentially infinite clause sets. We would also like to analyze possibilities
of checking entailment when the second-order quantifier elimination method
returns a fixpoint and not a formula. (The main obstacle when working on this
problem was that $\mu Z$ returns “unknown” in the presence of parameters.)

Acknowledgments: We thank Hannes Frey and Lucas Böltz for the numerous
discussions we had on the problems in wireless networks discussed in Section
2, Renate Schmidt for maintaining a website where one can run SCAN online and
for sending us the executables and instructions for running them. We thank the
reviewers for their helpful comments.

## References

  * [1] M. Abdulaziz, K. Mehlhorn, and T. Nipkow.  Trustworthy graph algorithms (invited talk).  In P. Rossmanith, P. Heggernes, and J. Katoen, editors, Proc. 44th Int. Symposium on Mathematical Foundations of Computer Science (MFCS 2019), volume 138 of LIPIcs, pages 1:1–1:22. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019.
  * [2] W. Ackermann.  Untersuchungen über das Eliminationsproblem der mathematischen Logik.  Mathematische Annalen, 110:390––413, 1935.
  * [3] W. Ackermann.  Zum Eliminationsproblem der mathematischen Logik.  Mathematische Annalen, 111:61–63, 1935.
  * [4] F. Alberti, S. Ghilardi, and N. Sharygina.  Definability of accelerated relations in a theory of arrays and its applications.  In P. Fontaine, C. Ringeissen, and R. A. Schmidt, editors, Frontiers of Combining Systems - 9th International Symposium, FroCoS 2013, Nancy, France, September 18-20, 2013. Proceedings, LNCS 8152, pages 23–39. Springer, 2013.
  * [5] L. Bachmair, H. Ganzinger, and U. Waldmann.  Refutational theorem proving for hierarchic first-order theories.  Appl. Algebra Eng. Commun. Comput., 5:193–212, 1994.
  * [6] C. W. Barrett, C. L. Conway, M. Deters, L. Hadarean, D. Jovanovic, T. King, A. Reynolds, and C. Tinelli.  CVC4.  In G. Gopalakrishnan and S. Qadeer, editors, Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings, LNCS 6806, pages 171–177. Springer, 2011.
  * [7] L. Barrière, P. Fraigniaud, L. Narayanan, and J. Opatrny.  Robust position-based routing in wireless ad hoc networks with irregular transmission ranges.  Wireless Communications and Mobile Computing, 3(2):141–153, Mar 2003.
  * [8] P. Baumgartner and U. Waldmann.  Hierarchic superposition with weak abstraction.  In M. P. Bonacina, editor, Automated Deduction - CADE-24 - 24th International Conference on Automated Deduction, Proceedings, LNCS 7898, pages 39–57. Springer, 2013.
  * [9] P. Baumgartner and U. Waldmann.  Hierarchic superposition revisited.  In C. Lutz, U. Sattler, C. Tinelli, A. Turhan, and F. Wolter, editors, Description Logic, Theory Combination, and All That - Essays Dedicated to Franz Baader on the Occasion of His 60th Birthday, LNCS 11560, pages 15–56. Springer, 2019.
  * [10] H. Behmann.  Beiträge zur Algebra der Logik, insbesondere zum Entscheidungsproblem.  Mathematische Annalen, 86(3-4):163–229, 1922.
  * [11] N. Bjørner, L. de Moura, L. Nachmanson, and C. M. Wintersteiger.  Programming Z3.  In J. P. Bowen, Z. Liu, and Z. Zhang, editors, Engineering Trustworthy Software Systems - 4th International School, SETSS 2018, Chongqing, China, April 7-12, 2018, Tutorial Lectures, LNCS 11430, pages 148–201. Springer, 2019.
  * [12] N. Bjørner, A. Gurfinkel, K. L. McMillan, and A. Rybalchenko.  Horn clause solvers for program verification.  In L. D. Beklemishev, A. Blass, N. Dershowitz, B. Finkbeiner, and W. Schulte, editors, Fields of Logic and Computation II - Essays Dedicated to Yuri Gurevich on the Occasion of His 75th Birthday, LNCS 9300, pages 24–51. Springer, 2015.
  * [13] N. Bjørner and L. Nachmanson.  Navigating the universe of Z3 theory solvers.  In G. Carvalho and V. Stolz, editors, Formal Methods: Foundations and Applications - 23rd Brazilian Symposium, SBMF 2020, Ouro Preto, Brazil, November 25-27, 2020, Proceedings, LNCS 12475, pages 8–24. Springer, 2020.
  * [14] B. Boigelot.  Symbolic Methods for Exploring Infinite State Spaces.  PhD thesis, Université de Liège, 1998.
  * [15] B. Courcelle.  The expression of graph properties and graph transformations in monadic second-order logic.  In G. Rozenberg, editor, Handbook of Graph Grammars and Computing by Graph Transformations, Volume 1: Foundations, pages 313–400. World Scientific, 1997.
  * [16] A. Fietzke, E. Kruglov, and C. Weidenbach.  Automatic generation of invariants for circular derivations in SUP(LA).  In N. Bjørner and A. Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning - 18th International Conference, LPAR-18, Mérida, Venezuela, March 11-15, 2012. Proceedings, LNCS 7180, pages 197–211. Springer, 2012.
  * [17] A. Finkel and J. Leroux.  How to compose Presburger-accelerations: Applications to broadcast protocols.  In M. Agrawal and A. Seth, editors, FST TCS 2002: Foundations of Software Technology and Theoretical Computer Science, 22nd Conference, Proceedings, LNCS 2556, pages 145–156. Springer, 2002.
  * [18] D. M. Gabbay and H. J. Ohlbach.  Quantifier elimination in second–order predicate logic.  In B. Nebel, C. Rich, and W. Swartout, editors, Principles of Knowledge Representation and Reasoning (KR92), pages 425–435. Morgan Kaufmann, 1992.  Also published as a Technical Report MPI-I-92-231, Max-Planck-Institut für Informatik, Saarbrücken, and in the South African Computer Journal, 1992.
  * [19] D. M. Gabbay, R. A. Schmidt, and A. Szalas.  Second-Order Quantifier Elimination - Foundations, Computational Aspects and Applications, volume 12 of Studies in logic : Mathematical logic and foundations.  College Publications, 2008.
  * [20] H. Ganzinger.  Relating semantic and proof-theoretic concepts for polynominal time decidability of uniform word problems.  In 16th Annual IEEE Symposium on Logic in Computer Science, Proceedings, pages 81–90. IEEE Computer Society, 2001.
  * [21] R. Givan and D. A. McAllester.  Polynomial-time computation via local inference relations.  ACM Trans. Comput. Log., 3(4):521–541, 2002.
  * [22] V. Goranko, U. Hustadt, R. A. Schmidt, and D. Vakarelov.  SCAN is complete for all sahlqvist formulae.  In R. Berghammer, B. Möller, and G. Struth, editors, Relational and Kleene-Algebraic Methods in Computer Science: 7th International Seminar on Relational Methods in Computer Science and 2nd International Workshop on Applications of Kleene Algebra, LNCS 3051, pages 149–162. Springer, 2004.
  * [23] K. Hoder, N. Bjørner, and L. M. de Moura.  _$\mu$ Z_\- an efficient engine for fixed points with constraints.  In G. Gopalakrishnan and S. Qadeer, editors, Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings, LNCS 6806, pages 457–462. Springer, 2011.
  * [24] K. Hoder, L. Kovács, and A. Voronkov.  Interpolation and symbol elimination in Vampire.  In J. Giesl and R. Hähnle, editors, Automated Reasoning, 5th International Joint Conference, IJCAR 2010, Proceedings, LNCS 6173, pages 188–195. Springer, 2010.
  * [25] M. Horbach and V. Sofronie-Stokkermans.  Obtaining finite local theory axiomatizations via saturation.  In P. Fontaine, C. Ringeissen, and R. A. Schmidt, editors, Frontiers of Combining Systems - 9th International Symposium, FroCoS 2013, Proceedings, LNCS 8152, pages 198–213. Springer, 2013.
  * [26] M. Horbach and V. Sofronie-Stokkermans.  Locality transfer: From constrained axiomatizations to reachability predicates.  In S. Demri, D. Kapur, and C. Weidenbach, editors, Automated Reasoning - 7th International Joint Conference, IJCAR 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Proceedings, LNCS 8562, pages 192–207. Springer, 2014.
  * [27] M. Horbach and C. Weidenbach.  Deciding the inductive validity of $\forall\exists^{*}$ queries.  In E. Grädel and R. Kahle, editors, Computer Science Logic, 23rd international Workshop, CSL 2009, 18th Annual Conference of the EACSL, Proceedings, LNCS 5771, pages 332–347. Springer, 2009.
  * [28] C. Ihlemann, S. Jacobs, and V. Sofronie-Stokkermans.  On local reasoning in verification.  In C. R. Ramakrishnan and J. Rehof, editors, Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings, LNCS 4963, pages 265–281. Springer, 2008.
  * [29] C. Ihlemann and V. Sofronie-Stokkermans.  System description: H-PILoT.  In R. A. Schmidt, editor, Automated Deduction - CADE-22, 22nd International Conference on Automated Deduction, Montreal, Canada, August 2-7, 2009. Proceedings, LNCS 5663, pages 131–139. Springer, 2009.
  * [30] C. Ihlemann and V. Sofronie-Stokkermans.  On hierarchical reasoning in combinations of theories.  In J. Giesl and R. Hähnle, editors, Automated Reasoning, 5th International Joint Conference, IJCAR 2010, Proceedings, LNCS 6173, pages 30–45. Springer, 2010.
  * [31] A. Kersani and N. Peltier.  Combining superposition and induction: A practical realization.  In P. Fontaine, C. Ringeissen, and R. A. Schmidt, editors, Frontiers of Combining Systems - 9th International Symposium, FroCoS 2013, Proceedings, LNCS 8152, pages 7–22. Springer, 2013.
  * [32] L. Kovács.  Invariant generation for p-solvable loops with assignments.  In E. A. Hirsch, A. A. Razborov, A. L. Semenov, and A. Slissenko, editors, Computer Science - Theory and Applications, Third International Computer Science Symposium in Russia, CSR 2008, Proceedings, LNCS 5010, pages 349–359. Springer, 2008.
  * [33] L. Kovács.  Reasoning algebraically about p-solvable loops.  In C. R. Ramakrishnan and J. Rehof, editors, Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Proceedings, LNCS 4963, pages 249–264. Springer, 2008.
  * [34] L. Kovács and A. Voronkov.  Interpolation and symbol elimination.  In R. A. Schmidt, editor, Automated Deduction - CADE-22, 22nd International Conference on Automated Deduction, Proceedings, LNCS 5663, pages 199–213. Springer, 2009.
  * [35] F. Kuhn, R. Wattenhofer, and A. Zollinger.  Ad hoc networks beyond unit disk graphs.  Wireless Networks, 14(5):715–729, Oct 2008.
  * [36] D. Peuter and V. Sofronie-Stokkermans.  On invariant synthesis for parametric systems.  In P. Fontaine, editor, Automated Deduction - CADE 27 - 27th International Conference on Automated Deduction, Proceedings, LNCS 11716, pages 385–405. Springer, 2019.
  * [37] D. Peuter and V. Sofronie-Stokkermans.  Symbol elimination and applications to parametric entailment problems.  In Proceedings of FroCoS 2021. Springer, 2021.  To appear.
  * [38] V. Sofronie-Stokkermans.  Hierarchic reasoning in local theory extensions.  In R. Nieuwenhuis, editor, Automated Deduction - CADE-20, 20th International Conference on Automated Deduction, Proceedings, LNCS 3632, pages 219–234. Springer, 2005.
  * [39] V. Sofronie-Stokkermans.  Hierarchic reasoning in local theory extensions.  In Proceedings of the 20th International Conference on Automated Deduction (CADE), LNCS 3632, pages 219–234, Jul 2005.
  * [40] V. Sofronie-Stokkermans.  On interpolation and symbol elimination in theory extensions.  In N. Olivetti and A. Tiwari, editors, Automated Reasoning - 8th International Joint Conference, IJCAR 2016, Proceedings, LNCS 9706, pages 273–289. Springer, 2016.
  * [41] V. Sofronie-Stokkermans.  On interpolation and symbol elimination in theory extensions.  Log. Methods Comput. Sci., 14(3), 2018.
  * [42] V. Sofronie-Stokkermans.  On interpolation and symbol elimination in theory extensions.  Log. Methods Comput. Sci., 14(3), 2018.
  * [43] M. Voigt.  Towards elimination of second-order quantifiers in the separated fragment.  In P. Koopmann, S. Rudolph, R. A. Schmidt, and C. Wernhard, editors, Proceedings of the Workshop on Second-Order Quantifier Elimination and Related Topics (SOQE 2017), Dresden, Germany, December 6-8, 2017, volume 2013 of CEUR Workshop Proceedings, pages 67–81. CEUR-WS.org, 2017.
  * [44] M. Voigt.  Decidable fragments of first-order logic and of first-order linear arithmetic with uninterpreted predicates.  PhD thesis, Saarland University, Saarbrücken, Germany, 2019.

##  Appendix 0.A Tests

We here present some of the tests we made for the examples in the paper. We
show how we used the tools on these examples including the corresponding input
and output files.

###  0.A.1 Tests for Example 3

We used H-PILoT to check that $(c1)$, $(c2)$ and $(c3)$ from Example 2 are
valid w.r.t. ${\mathcal{T}}={\mathcal{T}}_{d}^{m}\cup{\sf Free}(r_{1},r_{2})$.
For this we show, one after the other, that the negation of each of these
formulae is unsatisfiable w.r.t. ${\mathcal{T}}$. We start with $(c1)$. In the
input file for H-PILoT we have the axioms for a metric specified under Clauses
and the negation of $(c1)$ is the Query.

⬇

Base_functions:={(+,2), (-,2), (*,2)}

Extension_functions:={(r1, 1, 1), (r2, 1, 1), (d, 2, 1)}

Relations:={(<=, 2), (<, 2), (>=, 2), (>, 2)}

Clauses := (FORALL x,y). d(x,y) = _0 –> x = y;

(FORALL x,y). x = y –> d(x,y) = _0;

(FORALL x,y). d(x,y) = d(y,x);

(FORALL x,y,z). d(x,y) <= d(x,z) + d(z,y);

Query := NOT(u = v);

d(u,v) <= r1(u);

NOT(u = w);

d(u,w) <= d(u,v);

OR(u = w, d(u,w) > r1(u));

H-PILoT performs the hierarchical reduction described in Theorem 10, then
hands the reduced problem over to a prover to check for satisfiability. We
here used Z3, which is also the default prover used by H-PILoT. We obtain the
following output from H-PILoT:

⬇

Reduced problem written to

example4-check_redundancy_1.smt.

unsat

H-PILoT spent 0.013423s on the problem.

The prover needed 0.012652s for the problem.

Total running time: 0.026075s.

The answer is “unsat” (unsatisfiable), so we have proved that $(c1)$ is valid
w.r.t. ${\mathcal{T}}={\mathcal{T}}_{d}^{m}\cup{\sf Free}(r_{1},r_{2})$. In
the same way we can prove validity of $(c2)$ and $(c3)$ w.r.t.
${\mathcal{T}}_{d}^{m}\cup{\sf Free}(r_{1},r_{2})$, and also the validity of
the three formulae w.r.t. ${\mathcal{T}}_{d}^{u}\cup{\sf Free}(r_{1},r_{2})$,
${\mathcal{T}}_{d}^{p}\cup{\sf Free}(r_{1},r_{2})$ and
${\mathcal{T}}_{d}^{n}\cup{\sf Free}(r_{1},r_{2})$.

Remark. The encoding in H-PILoT presented above did not use two different
sorts ${\sf p}$ and ${\sf num}$ as described in the theoretical
considerations. Since in our case the sort ${\sf p}$ can be considered to be
uninterpreted and there are no function symbols of arity ${\sf
p}^{k}\rightarrow{\sf p}$, the following holds: Let $G$ be a flat ground
formula over a signature containing a binary function $d$ and a unary function
$r_{1}$ with the property that the only constraints on the constants used as
arguments for $d$ and $r_{1}$ are equalities and disequalities. Then the
following are equivalent:

  * (1)

$G$ is satisfiable w.r.t. the extension of ${\mathbb{R}}$ with a binary
function $d$ satisfying the metric axioms and a unary free function symbol
$r_{1}$.

  * (2)

$G$ is satisfiable w.r.t. the extension of the two-sorted theory
${\mathcal{T}}^{m}_{d}$ with the free function $r_{1}$.

Indeed, from every model
$\mathcal{A}=({\mathbb{R}},d_{A}:{\mathbb{R}}^{2}\rightarrow{\mathbb{R}},{r_{1}}_{A}:{\mathbb{R}}\rightarrow{\mathbb{R}})$
of $G$ w.r.t. the extension of ${\mathbb{R}}$ with a binary function $d$
satisfying the metric axioms and a unary free function symbol $r_{1}$, we can
define a model