1721 LABEL:LastPageMay 07, 2020Apr. 12, 2021

Extended version of Bentkamp et al., “Superposition for lambda-free higher-
order logic” [BBCW18]

# Superposition for Lambda-Free Higher-Order Logic

Alexander Bentkampa  ,  Jasmin Blanchettea  aVrije Universiteit Amsterdam,
Department of Computer Science, De Boelelaan 1111, 1081 HV Amsterdam, The
Netherlands<EMAIL_ADDRESS><EMAIL_ADDRESS>,  Simon Cruanesb
bAesthetic Integration, 600 Congress Ave., Austin, Texas, 78701, USA
<EMAIL_ADDRESS>and  Uwe Waldmannc  cMax-Planck-Institut für Informatik,
Saarland Informatics Campus, Saarbrücken, Germany<EMAIL_ADDRESS>
###### Abstract.

We introduce refutationally complete superposition calculi for intentional and
extensional clausal $\lambda$-free higher-order logic, two formalisms that
allow partial application and applied variables. The calculi are parameterized
by a term order that need not be fully monotonic, making it possible to employ
the $\lambda$-free higher-order lexicographic path and Knuth–Bendix orders. We
implemented the calculi in the Zipperposition prover and evaluated them on
Isabelle/HOL and TPTP benchmarks. They appear promising as a stepping stone
towards complete, highly efficient automatic theorem provers for full higher-
order logic.

###### Key words and phrases:

superposition calculus, Boolean-free lambda-free higher-order logic,
refutational completeness

##  1\. Introduction

Superposition is a highly successful calculus for reasoning about first-order
logic with equality. We are interested in _graceful_ generalizations to
higher-order logic: calculi that, as much as possible, coincide with standard
superposition on first-order problems and that scale up to arbitrary higher-
order problems.

As a stepping stone towards full higher-order logic, in this article we
restrict our attention to a clausal $\lambda$-free fragment of polymorphic
higher-order logic that supports partial application and application of
variables (

##  2\.

9). This formalism is expressive enough to permit the axiomatization of
higher-order combinators such as
${\mathsf{pow}}:\mathsf{\Pi}\alpha.\;{{\mathsf{nat}}}\to(\alpha\to\alpha)\to\alpha\to\alpha$
(intended to denote the iterated application $h^{n}\>x$):

$\displaystyle{\mathsf{pow}}{\langle\alpha\rangle}\;{\mathsf{Zero}}\;h$
$\displaystyle\approx{\mathsf{id}}{\langle\alpha\rangle}$
$\displaystyle{\mathsf{pow}}{\langle\alpha\rangle}\;({\mathsf{Succ}}\;n)\;h\;x$
$\displaystyle\approx h\;({\mathsf{pow}}{\langle\alpha\rangle}\;n\;h\;x)$

Conventionally, functions are applied without parentheses and commas, and
variables are italicized. Notice the variable number of arguments to
${\mathsf{pow}}{\langle\alpha\rangle}$ and the application of $h.$ The
expressiveness of full higher-order logic can be recovered by introducing
${\mathsf{SK}}$-style combinators to represent $\lambda$-abstractions and
proxies for the logical symbols [Ker91, Rob70].

A widespread technique to support partial application and application of
variables in first-order logic is to make all symbols nullary and to represent
application of functions by a distinguished binary symbol
${\mathsf{app}}:\mathsf{\Pi}\alpha,\beta.\;{{\mathsf{fun}}}(\alpha,\beta)\times\alpha\to\beta$,
where ${{\mathsf{fun}}}$ is an uninterpreted binary type constructor.
Following this scheme, the higher-order term
${\mathsf{f}}\>(h\;{\mathsf{f}})$, where
${\mathsf{f}}:\kappa\to\kappa^{\prime}$, is translated to
${\mathsf{app}}({\mathsf{f}},{\mathsf{app}}(h,{\mathsf{f}}))$—or rather
${\mathsf{app}}{\langle\kappa,\kappa^{\prime}\rangle}({\mathsf{f}},{\mathsf{app}}{\langle{{\mathsf{fun}}}(\kappa,\kappa^{\prime}),\kappa\rangle}(h,{\mathsf{f}}))$
if we specify the type arguments. We call this the _applicative encoding._ The
existence of such a reduction to first-order logic explains why $\lambda$-free
higher-order terms are also called “applicative first-order terms.” Unlike for
full higher-order logic, most general unifiers are unique for our
$\lambda$-free fragment, just as they are for applicatively encoded first-
order terms.

Although the applicative encoding is complete [Ker91] and is employed
fruitfully in tools such as HOLyHammer and Sledgehammer [BKPU16], it suffers
from a number of weaknesses, all related to its gracelessness. Transforming
all the function symbols into constants considerably restricts what can be
achieved with term orders; for example, argument tuples cannot easily be
compared using different methods for different symbols [Kop12,

##  3\.

2.3.1] . In a prover, the encoding also clutters the data structures, slows
down the algorithms, and neutralizes the heuristics that look at the terms’
root symbols. But our chief objection is the sheer clumsiness of encodings and
their poor integration with interpreted symbols. And they quickly accumulate;
for example, using the traditional encoding of polymorphism relying on a
distinguished binary function symbol ${\mathsf{t}}$ [BBPS16,

##  4\.

3.3] in conjunction with the applicative encoding, the term
${\mathsf{Succ}}\;{\mathit{x}}$ becomes
${\mathsf{t}}({\mathsf{nat}},\allowbreak{\mathsf{app}}({\mathsf{t}}({\mathsf{fun}}({\mathsf{nat}},\allowbreak{\mathsf{nat}}),\allowbreak{\mathsf{Succ}}),\allowbreak{\mathsf{t}}({\mathsf{nat}},{\mathit{x}})))$.
The term’s simple structure is lost in translation.

Hybrid schemes have been proposed to strengthen the applicative encoding: If a
given symbol always occurs with at least $k$ arguments, these can be passed
directly [MP08]. However, this relies on a closed-world assumption: that all
terms that will ever be compared arise in the initial problem. This
noncompositionality conflicts with the need for complete higher-order calculi
to synthesize arbitrary terms during proof search [BM14]. As a result, hybrid
encodings are not an ideal basis for higher-order automated reasoning.

Instead, we propose to generalize the superposition calculus to _intensional_
and _extensional_ clausal $\lambda$-free higher-order logic. For the
extensional version of the logic, the property $\kern 0.83328pt(\forall
x.\;h\>x\approx
k\>x)\mathrel{{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color<EMAIL_ADDRESS>to0.0pt{\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}$\blacksquare$\hss}\kern-3.87495pt}\joinrel{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rightarrow}}h\approx
k\kern 0.83328pt$ holds for all functions $h{,}\>k$ of the same type. For each
logic, we present two calculi (

##  5\.

12). The intentional calculi perfectly coincide with standard superposition on
first-order clauses; the extensional calculi depend on an extra axiom.

Superposition is parameterized by a term order, which is used to prune the
search space. If we assume that the term order is a simplification order
enjoying totality on ground terms (i.e., terms containing no term or type
variables), the standard calculus rules and completeness proof can be lifted
verbatim. The only necessary changes concern the basic definitions of terms
and substitutions. However, there is one monotonicity property that is hard to
obtain unconditionally:  _compatibility with arguments_. It states that
$s^{\prime}\succ s$ implies $s^{\prime}\>t\succ s\;t$ for all terms
$s{,}\>s^{\prime}\\!{,}\>t$ such that $s\;t$ and $s^{\prime}\;t$ are well
typed. Blanchette, Waldmann, and colleagues recently introduced graceful
generalizations of the lexicographic path order (LPO) [BWW17] and the
Knuth–Bendix order (KBO) [BBWW17] with argument coefficients, but they both
lack this property. For example, given a KBO with
${\mathsf{g}}\succ{\mathsf{f}}$, it may well be that
${\mathsf{g}}\;{\mathsf{a}}\prec{\mathsf{f}}\;{\mathsf{a}}$ if ${\mathsf{f}}$
has a large enough multiplier on its argument.

Our superposition calculi are designed to be refutationally complete for such
nonmonotonic orders (

##  6\.

16). To achieve this, they include an inference rule for argument congruence,
which derives $C\mathrel{\lor}s\;{\mathit{x}}\approx t\;{\mathit{x}}$ from
$C\mathrel{\lor}s\approx t$. The redundancy criterion is defined in such a way
that the larger, derived clause is not subsumed by the premise. In the
completeness proof, the most difficult case is the one that normally excludes
superposition at or below variables using the induction hypothesis. With
nonmonotonicity, this approach no longer works, and we propose two
alternatives: Either perform some superposition inferences into higher-order
variables or “purify” the clauses to circumvent the issue. We refer to the
corresponding calculi as _nonpurifying_ and _purifying._

The calculi are implemented in the Zipperposition prover [Cru17] (

##  7\.

20). We evaluate them on first- and higher-order Isabelle/HOL [BN10] and TPTP
benchmarks [SSCB12, SBBT09] and compare them with the applicative encoding (

##  8\.

21). We find that there is a substantial cost associated with the applicative
encoding, that the nonmonotonicity is not particularly expensive, and that the
nonpurifying calculi outperform the purifying calculi.

An earlier version of this work was presented at IJCAR 2018 [BBCW18]. This
article extends the conference paper with detailed soundness and completeness
proofs and more explanations. Because of too weak selection restrictions on
the purifying calculi, our claim of refutational completeness in the
conference version was not entirely correct. We now strengthened the selection
restrictions accordingly. Moreover, we extended the logic with polymorphism,
leading to minor modifications to the calculus. We also simplified the
presentation of the clausal fragment of the logic that interests us. In
particular, we removed mandatory arguments. The redundancy criterion also
differs slightly from the conference version. Finally, we updated the
empirical evaluation to reflect recent improvements in the Zipperposition
prover.

Since the publication of the conference paper, two research groups have built
on our work. Bhayat and Reger [BR20] extended our intensional nonpurifying
calculus to a version of higher-order logic with combinators. They use it with
a nonmonotonic order that orients the defining equations of
${\mathsf{SK}}$-style combinators. Bentkamp et al. [BBT+21] extended our
extensional nonpurifying calculus to a calculus on $\lambda$-terms. For them,
support for nonmonotonic orders is crucial as well because no ground-total
simplification order exists for $\lambda$-terms up to $\beta$-conversion.
Based on these two extensions of our calculi, the provers Zipperposition and
Vampire achieved first and third place, respectively, in the higher-order
category of the 2020 edition of the CADE ATP System Competition (CASC-J10).

##  9\. Logic

Our logic is intended as an intermediate step on the way towards full higher-
order logic (also called simple type theory) [Chu40, GM93]. Refutational
completeness of calculi for higher-order logic is usually stated in terms of
Henkin semantics [Hen50, BM14], in which the universes used to interpret
functions need only contain the functions that can be expressed as terms.
Since the terms of $\lambda$-free higher-order logic exclude
$\lambda$-abstractions, in “$\lambda$-free Henkin semantics” the universes
interpreting functions can be even smaller. In that sense, our semantics
resemble Henkin prestructures [Lei94,

##  10\.

5.4] . In contrast to other higher-order logics [Vää19], there are no
comprehension principles, and we disallow nesting of Boolean formulas inside
terms.

###  10.1. Syntax

We fix a set $\mathrm{\Sigma}_{\mathsf{ty}}$ of type constructors with arities
and a set $\mathcalx{V}_{\mathsf{ty}}$ of type variables. We require at least
one nullary type constructor and a binary type constructor ${\rightarrow}$ to
be present in $\mathrm{\Sigma}_{\mathsf{ty}}$. We inductively define a
$\lambda$-free higher-order type to be either a type variable
$\alpha\in\mathcalx{V}_{\mathsf{ty}}$ or of the form $\kappa(\bar{\tau}_{n})$
for an $n$-ary type constructor $\kappa\in\mathrm{\Sigma}_{\mathsf{ty}}$ and
types $\bar{\tau}_{n}$. Here and elsewhere, we write $\bar{a}_{n}$ or
$\bar{a}$ to abbreviate the tuple $(a_{1},\dots,a_{n})$ or product
$a_{1}\times\dots\times a_{n}$, for $n\geq 0$. We write $\kappa$ for
$\kappa()$ and $\tau\rightarrow\upsilon$ for ${\rightarrow}(\tau,\upsilon)$. A
type declaration is an expression of the form
$\mathsf{\Pi}\bar{\alpha}_{m}.\;\tau$ (or simply $\tau$ if $m=0$), where all
type variables occurring in $\tau$ belong to $\bar{\alpha}_{m}$.

We fix a set $\mathrm{\Sigma}$ of symbols with type declarations, written as
${\mathsf{f}}:\mathsf{\Pi}\bar{\alpha}_{m}.\;\tau$ or ${\mathsf{f}}$, and a
set $\mathcalx{V}$ of typed variables, written as ${\mathit{x}}:\tau$ or
${\mathit{x}}$. We require $\mathrm{\Sigma}$ to contain a symbol with type
declaration $\mathsf{\Pi}\alpha.\;\alpha$, to ensure that the (Herbrand)
domain of every type is nonempty. The sets
$(\mathrm{\Sigma}_{\mathsf{ty}},\mathrm{\Sigma})$ form the logic’s signature.
We reserve the letters $s,t,u,v,w$ for terms and $x,y,z$ for variables and
write ${:}\;\tau$ to indicate their type. The set of $\lambda$-free higher-
order terms is defined inductively as follows. Every variable
$x:\tau\in\mathcalx{V}$ is a term. If
${\mathsf{f}}:\mathsf{\Pi}\bar{\alpha}_{m}.\;\tau$ is a symbol and
$\bar{\upsilon}_{m}$ are types, then
${\mathsf{f}}{\langle\bar{\upsilon}_{m}\rangle}:\tau\\{\bar{\alpha}_{m}\mapsto\bar{\upsilon}_{m}\\}$
is a term. If $t:\tau\rightarrow\upsilon$ and $u:\tau$, then $t\;u:\upsilon$
is a term, called an _application_. Nonapplication terms are called _heads_.
Application is left-associative, and correspondingly the function type
constructor $\rightarrow$ is right-associative. Using the spine notation
[CP03], terms can be decomposed in a unique way as a head $t$ applied to zero
or more arguments: $t\>s_{1}\dots s_{n}$ or $t\>\bar{s}_{n}$ (abusing
notation). A term is _ground_ if it is built without using type or term
variables.

Substitution and unification are generalized in the obvious way, without the
difficulties caused by $\lambda$-abstractions. A substitution has the form
$\\{\bar{\alpha}_{m},\bar{x}_{n}\mapsto\bar{\upsilon}_{m},\bar{s}_{n}\\}$,
where each $x_{\\!j}$ has type $\tau_{\\!j}$ and each $s_{\\!j}$ has type
$\tau_{\\!j}\\{\bar{\alpha}_{m}\mapsto\bar{\upsilon}_{m}\\}$, mapping $m$ type
variables to $m$ types and $n$ term variables to $n$ terms. A unifier of two
terms $s$ and $t$ is a substitution $\rho$ such that $s\rho=t\rho$. A most
general unifier $\operatorname{mgu}(s,t)$ of two terms $s$ and $t$ is a
unifier $\sigma$ of $s$ and $t$ such that for every other unifier $\theta$,
there exists a substitution $\rho$ such that $\alpha\theta=\alpha\sigma\rho$
and $x\theta=x\sigma\rho$ for all $\alpha\in\mathcalx{V}_{\mathsf{ty}}$ and
all $x\in\mathcalx{V}$. As in first-order logic, the most general unifier is
unique up to variable renaming. For example,
$\operatorname{mgu}(x\>{\mathsf{b}}\>z,\>{\mathsf{f}}\>{\mathsf{a}}\>y\>{\mathsf{c}})=\\{x\mapsto{\mathsf{f}}\>{\mathsf{a}}{,}\>y\mapsto{\mathsf{b}}{,}\>z\mapsto{\mathsf{c}}\\}$,
and
$\operatorname{mgu}(y\>({\mathsf{f}}\>{\mathsf{a}}),\>{\mathsf{f}}\>(y\>{\mathsf{a}}))=\\{y\mapsto{\mathsf{f}}\\}$,
assuming that the types of the unified subterms are equal.

An equation $s\approx t$ is formally an unordered pair of terms $s$ and $t$ of
the same type. A literal is an equation or a negated equation, written
$s\not\approx t$. A clause $L_{1}\lor\dots\lor L_{n}$ is a finite multiset of
literals $L_{j}$. The empty clause is written as $\bot$.

###  10.2. Semantics

A _type interpretation_
$\mathcal{I}_{\mathsf{ty}}=(\mathcalx{U},\mathcalx{J}_{\mathsf{ty}})$ is
defined as follows. The set $\mathcalx{U}$ is a nonempty collection of
nonempty sets, called _universes_. The function $\mathcalx{J}_{\mathsf{ty}}$
associates a function
$\mathcalx{J}_{\mathsf{ty}}(\kappa):\mathcalx{U}^{n}\rightarrow\mathcalx{U}$
with each $n$-ary type constructor $\kappa$. A _type valuation_ $\xi$ is a
function that maps every type variable to a universe. The _denotation_ of a
type for a type interpretation $\mathcal{I}_{\mathsf{ty}}$ and a type
valuation $\xi$ is defined by
$\smash{\llbracket\alpha\rrbracket_{\mathcal{I}_{\mathsf{ty}}}^{\smash{\xi}}}=\xi(\alpha)$
and
$\smash{\llbracket\kappa(\bar{\tau})\rrbracket_{\mathcal{I}_{\mathsf{ty}}}^{\smash{\xi}}}=\mathcalx{J}_{\mathsf{ty}}(\kappa)(\smash{\llbracket\bar{\tau}\rrbracket_{\mathcal{I}_{\mathsf{ty}}}^{\smash{\xi}}})$.
Here and elsewhere, we abuse notation by applying an operation on a tuple when
it must be applied elementwise; thus,
$\smash{\llbracket\bar{\tau}_{n}\rrbracket_{\mathcal{I}_{\mathsf{ty}}}^{\smash{\xi}}}$
stands for
$\smash{\llbracket\tau_{1}\rrbracket_{\mathcal{I}_{\mathsf{ty}}}^{\smash{\xi}}},\dots,\smash{\llbracket\tau_{n}\rrbracket_{\mathcal{I}_{\mathsf{ty}}}^{\smash{\xi}}}$.

A type valuation $\xi$ can be extended to be a _valuation_ by additionally
assigning an element
$\xi(x)\in\smash{\llbracket\tau\rrbracket_{\mathcal{I}_{\mathsf{ty}}}^{\smash{\xi}}}$
to each variable $x:\tau$. An _interpretation function_ $\mathcalx{J}$ for a
type interpretation $\mathcal{I}_{\mathsf{ty}}$ associates with each symbol
${\mathsf{f}}:\mathsf{\Pi}\bar{\alpha}_{m}.\;\tau$ and universe tuple
$\bar{U}_{m}\in\mathcalx{U}^{m}$ a value
$\mathcalx{J}({\mathsf{f}},\bar{U}_{m})\in\smash{\llbracket\tau\rrbracket_{\mathcal{I}_{\mathsf{ty}}}^{\smash{\xi}}}$,
where $\xi$ is the type valuation that maps each $\alpha_{i}$ to $U_{i}$.
Loosely following Fitting [Fit02,

##  11\.

2.5] , an _extension function_ $\mathcalx{E}$ associates to any pair of
universes $U_{1},U_{2}\in\mathcalx{U}$ a function
$\mathcalx{E}_{U_{1},U_{2}}:\mathcalx{J}_{\mathsf{ty}}({\rightarrow})(U_{1},U_{2})\rightarrow\allowbreak(U_{1}\rightarrow
U_{2})$. Together, a type interpretation, an interpretation function, and an
extension function form an _interpretation_
$\mathcal{I}=(\mathcalx{U},\mathcalx{J}_{\mathsf{ty}},\mathcalx{J},\mathcalx{E})$.

An interpretation is _extensional_ if $\mathcalx{E}_{U_{1},U_{2}}$ is
injective for all $U_{1},U_{2}$. Both intensional and extensional logics are
widely used for interactive theorem proving; for example, Coq’s calculus of
inductive constructions is intensional [BC04], whereas Isabelle/HOL is
extensional [NPW02]. The semantics is _standard_ if
$\mathcalx{E}_{U_{1},U_{2}}$ is bijective for all $U_{1},U_{2}$.

For an interpretation
$\mathcal{I}=(\mathcalx{U},\mathcalx{J}_{\mathsf{ty}},\mathcalx{J},\mathcalx{E})$
and a valuation $\xi$, the denotation of a term is defined as follows: For
variables $x$, let $\smash{\llbracket
x\rrbracket_{\mathcal{I}}^{\smash{\xi}}}=\xi(x)$. For symbols ${\mathsf{f}}$,
let
$\smash{\llbracket{\mathsf{f}}{\langle\bar{\tau}\rangle}\rrbracket_{\mathcal{I}}^{\smash{\xi}}}=\mathcalx{J}({\mathsf{f}},\smash{\llbracket\bar{\tau}\rrbracket_{\mathcal{I}_{\mathsf{ty}}}^{\smash{\xi}}})$.
For applications $s\;t$ of a term $s:\tau\rightarrow\upsilon$ to a term
$t:\tau$, let
$U_{1}=\smash{\llbracket\tau\rrbracket_{\mathcal{I}_{\mathsf{ty}}}^{\smash{\xi}}}$,
$U_{2}=\smash{\llbracket\upsilon\rrbracket_{\mathcal{I}_{\mathsf{ty}}}^{\smash{\xi}}}$,
and $\smash{\llbracket
s\;t\rrbracket_{\mathcal{I}}^{\smash{\xi}}}=\mathcalx{E}_{U_{1},U_{2}}(\smash{\llbracket
s\rrbracket_{\mathcal{I}}^{\smash{\xi}}})(\smash{\llbracket
t\rrbracket_{\mathcal{I}}^{\smash{\xi}}})$. If $t$ is a ground term, we also
write $\smash{\llbracket t\rrbracket_{\mathcal{I}}^{\smash{}}}$ for the
denotation of $t$ because it does not depend on the valuation.

An equation $s\approx t$ is true in $\mathcal{I}$ for $\xi$ if
$\smash{\llbracket s\rrbracket_{\mathcal{I}}^{\smash{\xi}}}=\smash{\llbracket
t\rrbracket_{\mathcal{I}}^{\smash{\xi}}}$; otherwise, it is false. A
disequation $s\not\approx t$ is true if $s\approx t$ is false. A clause is
true if at least one of its literals is true. The interpretation $\mathcal{I}$
is a model of a clause $C$, written $\mathcal{I}\models C$, if $C$ is true in
$\mathcal{I}$ for all valuations $\xi$. It is a model of a set of clauses if
it is a model of all contained clauses.

For example, given the signature
$(\\{\kappa,\rightarrow\\},\\{{\mathsf{a}}:\kappa\\})$ and a variable
$h:\kappa\rightarrow\kappa$, the clause
${\mathit{h}}\;{\mathsf{a}}\not\approx{\mathsf{a}}$ has an extensional model
with $\mathcalx{U}=\\{U_{1},U_{2}\\}$, $U_{1}=\\{a,b\\}$ ($a\not=b$),
$U_{2}=\\{f\\}$, $\mathcalx{J}_{\mathsf{ty}}(\kappa)=U_{1}$,
$\mathcalx{J}_{\mathsf{ty}}({\rightarrow})(U_{1},U_{1})=U_{2}$,
$\mathcalx{J}({\mathsf{a}})=a$,
$\mathcalx{E}_{U_{1},U_{1}}(f)(a)=\mathcalx{E}_{U_{1},U_{1}}(f)(b)=b$.

##  12\. The Calculi

We introduce four versions of the _Boolean-free $\lambda$-free higher-order
superposition calculus_, articulated along two axes: intentional versus
extensional, and nonpurifying versus purifying. To avoid repetitions, our
presentation unifies them into a single framework.

###  12.1. The Inference Rules

To support nonmonotonic term orders, we restrict superposition inferences to
_green subterms_ , which are defined inductively as follows:

######  Definition  (Green subterms and contexts).

A term $t^{\prime}$ is a _green subterm_ of $t$ if $t=t^{\prime}$ or if
$t=s\;\bar{u}$ and $t^{\prime}$ is a green subterm of $u_{i}$ for some $i$. We
write
$s\begin{picture}(5.0,7.0)\put(1.1,3.0){\rotatebox{45.0}{\line(1,0){6.0}}}
\put(1.1,3.0){\rotatebox{315.0}{\line(1,0){6.0}}} \end{picture}\kern
0.83328ptu\begin{picture}(5.0,7.0)\put(0.1,3.0){\rotatebox{135.0}{\line(1,0){6.0}}}
\put(0.1,3.0){\rotatebox{225.0}{\line(1,0){6.0}}} \end{picture}\,$ to indicate
that the subterm $u$ of $s[u]$ is a green subterm. Correspondingly, we call
the context
$s\begin{picture}(5.0,7.0)\put(1.1,3.0){\rotatebox{45.0}{\line(1,0){6.0}}}
\put(1.1,3.0){\rotatebox{315.0}{\line(1,0){6.0}}} \end{picture}\kern
0.83328pt\phantom{.}\begin{picture}(5.0,7.0)\put(0.1,3.0){\rotatebox{135.0}{\line(1,0){6.0}}}
\put(0.1,3.0){\rotatebox{225.0}{\line(1,0){6.0}}} \end{picture}\,$ around a
green subterm a _green context_.

By this definition, ${\mathsf{f}}$ and ${\mathsf{f}}\;{\mathsf{a}}$ are
subterms of ${\mathsf{f}}\;{\mathsf{a}}\;{\mathsf{b}}$, but not green
subterms. The green subterms of ${\mathsf{f}}\;{\mathsf{a}}\;{\mathsf{b}}$ are
${\mathsf{a}}$, ${\mathsf{b}}$, and
${\mathsf{f}}\;{\mathsf{a}}\;{\mathsf{b}}$. Thus,
$[\phantom{i}]\;{\mathsf{a}}\;{\mathsf{b}}$ and $[\phantom{i}]\;{\mathsf{b}}$
are not green contexts, but ${\mathsf{f}}\;[\phantom{i}]\;{\mathsf{b}}$,
${\mathsf{f}}\;{\mathsf{a}}\;[\phantom{i}]$, and $[\phantom{i}]$ are.

The calculi are parameterized by a partial order $\succ$ on terms that

  * –

is well founded on ground terms;

  * –

is total on ground terms;

  * –

has the subterm property on ground terms;

  * –

is _compatible with green contexts_ on ground terms: $t^{\prime}\succ t$
implies
$s\begin{picture}(5.0,7.0)\put(1.1,3.0){\rotatebox{45.0}{\line(1,0){6.0}}}
\put(1.1,3.0){\rotatebox{315.0}{\line(1,0){6.0}}} \end{picture}\kern
0.83328ptt^{\prime}\begin{picture}(5.0,7.0)\put(0.1,3.0){\rotatebox{135.0}{\line(1,0){6.0}}}
\put(0.1,3.0){\rotatebox{225.0}{\line(1,0){6.0}}} \end{picture}\,\succ
s\begin{picture}(5.0,7.0)\put(1.1,3.0){\rotatebox{45.0}{\line(1,0){6.0}}}
\put(1.1,3.0){\rotatebox{315.0}{\line(1,0){6.0}}} \end{picture}\kern
0.83328ptt\begin{picture}(5.0,7.0)\put(0.1,3.0){\rotatebox{135.0}{\line(1,0){6.0}}}
\put(0.1,3.0){\rotatebox{225.0}{\line(1,0){6.0}}} \end{picture}\,$;

  * –

is stable under grounding substitutions: $t\succ s$ implies $t\theta\succ
s\theta$ for all substitutions $\theta$ grounding $t$ and $s$.

The order need not be _compatible with arguments_ : $s^{\prime}\succ s$ need
not imply $s^{\prime}\>{t}\succ s\;{t}$, even on ground terms. The literal and
clause orders are defined from $\succ$ as multiset extensions in the standard
way [BG94]. Despite their names, the term, literal, and clause orders need not
be transitive on nonground entities.

The $\lambda$-free higher-order generalizations of LPO [BWW17] and KBO
[BBWW17] as well as EPO [Ben18] fulfill these requirements, with the caveat
that they are defined on untyped terms. To use them on polymorphic terms, we
can encode type arguments as term arguments and ignore the remaining type
information.

Literal selection is supported. The selection function maps each clause $C$ to
a subclause of $C$ consisting of negative literals. A literal $L$ is
(_strictly_) _eligible_ w.r.t. a substitution $\sigma$ in $C$ if it is
selected in $C$ or there are no selected literals in $C$ and $L\sigma$ is
(strictly) maximal in $C\sigma.$ If $\sigma$ is the identity substitution, we
leave it implicit.

The following four rules are common to all four calculi. We regard positive
and negative superposition as two cases of the same rule

$\prftree[r]{\small{\textsc{Sup}}}{\overbrace{D^{\prime}\mathrel{\lor}{t\approx
t^{\prime}}}^{\vphantom{\cdot}\smash{D}}\quad\overbrace{C^{\prime}\mathrel{\lor}s\begin{picture}(5.0,7.0)\put(1.1,3.0){\rotatebox{45.0}{\line(1,0){6.0}}}
\put(1.1,3.0){\rotatebox{315.0}{\line(1,0){6.0}}} \end{picture}\kern
0.83328ptu\begin{picture}(5.0,7.0)\put(0.1,3.0){\rotatebox{135.0}{\line(1,0){6.0}}}
\put(0.1,3.0){\rotatebox{225.0}{\line(1,0){6.0}}}
\end{picture}\,\mathrel{\dot{\approx}}s^{\prime}}^{\smash{C}}}{(D^{\prime}\mathrel{\lor}C^{\prime}\mathrel{\lor}s\begin{picture}(5.0,7.0)\put(1.1,3.0){\rotatebox{45.0}{\line(1,0){6.0}}}
\put(1.1,3.0){\rotatebox{315.0}{\line(1,0){6.0}}} \end{picture}\kern
0.83328ptt^{\prime}\begin{picture}(5.0,7.0)\put(0.1,3.0){\rotatebox{135.0}{\line(1,0){6.0}}}
\put(0.1,3.0){\rotatebox{225.0}{\line(1,0){6.0}}}
\end{picture}\,\mathrel{\dot{\approx}}s^{\prime})\sigma}$

where $\mathrel{\dot{\approx}}$ denotes $\approx$ or $\not\approx$ and the
following conditions are fulfilled:

  1. 1.

$\sigma=\operatorname{mgu}(t,u)$; 2. $t\sigma\not\preceq t^{\prime}\sigma$; 3.
$s\begin{picture}(5.0,7.0)\put(1.1,3.0){\rotatebox{45.0}{\line(1,0){6.0}}}
\put(1.1,3.0){\rotatebox{315.0}{\line(1,0){6.0}}} \end{picture}\kern
0.83328ptu\begin{picture}(5.0,7.0)\put(0.1,3.0){\rotatebox{135.0}{\line(1,0){6.0}}}
\put(0.1,3.0){\rotatebox{225.0}{\line(1,0){6.0}}}
\end{picture}\,\sigma\not\preceq s^{\prime}\sigma$ ;

  2. 4.

$t\approx t^{\prime}$ is strictly eligible w.r.t. $\sigma$ in $D$; 5.
$C\sigma\not\preceq D\sigma$;

  3. 6.

$s\begin{picture}(5.0,7.0)\put(1.1,3.0){\rotatebox{45.0}{\line(1,0){6.0}}}
\put(1.1,3.0){\rotatebox{315.0}{\line(1,0){6.0}}} \end{picture}\kern
0.83328ptu\begin{picture}(5.0,7.0)\put(0.1,3.0){\rotatebox{135.0}{\line(1,0){6.0}}}
\put(0.1,3.0){\rotatebox{225.0}{\line(1,0){6.0}}}
\end{picture}\,\mathrel{\dot{\approx}}s^{\prime}$ is eligible w.r.t. $\sigma$
in $C$ and, if positive, even strictly eligible;

  4. 7.

the _variable condition_ must hold, which is specified individually for each
calculus below.

In each calculus, we will define the variable condition to coincide with the
condition “$u\not\in\mathcalx{V}$” if the premises are first-order.

The equality resolution and equality factoring rules are almost identical to
their standard counterparts:

$\prftree[r]{\small{\textsc{ERes}}}{\overbrace{C^{\prime}\mathrel{\lor}{s\not\approx
s^{\prime}}}^{C}}{C^{\prime}\sigma}$

where

  1. 1.

$\sigma=\operatorname{mgu}(s,s^{\prime})$; 2. $s\not\approx s^{\prime}$ is
eligible w.r.t. $\sigma$ in $C$.

$\prftree[r]{\small{\textsc{EFact}}}{\overbrace{C^{\prime}\mathrel{\lor}{s^{\prime}}\approx
t^{\prime}\mathrel{\lor}{s}\approx
t}^{C}}{(C^{\prime}\mathrel{\lor}t\not\approx t^{\prime}\mathrel{\lor}s\approx
t^{\prime})\sigma}$

where

  1. 1.

$\sigma=\operatorname{mgu}(s,s^{\prime})$; 2. $s\sigma\not\preceq t\sigma$; 3.
$s\approx t$ is eligible w.r.t. $\sigma$ in $C$.

The following _argument congruence_ rule compensates for the limitation that
the superposition rule applies only to green subterms:

$\prftree[r]{\small{\textsc{ArgCong}}}{\overbrace{C^{\prime}\mathrel{\lor}s\approx
s^{\prime}}^{C}}{C^{\prime}\sigma\lor s\sigma\;\bar{x}\approx
s^{\prime}\sigma\>\bar{x}}$

where

  1. 1.

$s\approx s^{\prime}$ is strictly eligible w.r.t. $\sigma$ in $C$;

  2. 2.

$\bar{x}$ is a nonempty tuple of distinct fresh variables;

  3. 3.

$\sigma$ is the most general type substitution that ensures well-typedness of
the conclusion.

In particular, if $s$ takes $m$ arguments, there are $m$ ArgCong conclusions
for this literal, for which $\sigma$ is the identity and $\bar{x}$ is a tuple
of 1, …, $m-1$, or $m$ variables. If the result type of $s$ is a type
variable, we have in addition infinitely many ArgCong conclusions, for which
$\sigma$ instantiates the type variable in the result type of $s$ with
$\bar{\alpha}_{k}\rightarrow\beta$ for some $k>0$ and fresh type variables
$\bar{\alpha}_{k}$ and $\beta$ and for which $\bar{x}$ is a tuple of $m+k$
variables. In practice, the enumeration of the infinitely many conclusions
must be interleaved with other inferences via some form of dovetailing.

For the intensional nonpurifying calculus, the variable condition of the Sup
rule is as follows:

> Either $u\notin\mathcalx{V}$ or there exists a grounding substitution
> $\theta$ with $t\sigma\theta\succ t^{\prime}\sigma\theta$ and
> $C\sigma\theta\prec C\\{u\mapsto t^{\prime}\\}\sigma\theta$.

This condition generalizes the standard condition that
$u\notin\mathcalx{V}\\!$. The two coincide if $C$ is first-order or if the
term order is monotonic. In some cases involving nonmonotonicity, the variable
condition effectively mandates Sup inferences at variable positions of the
right premise, but never below. We will call theses inferences _at variables_.

For the extensional nonpurifying calculus, the variable condition uses the
following definition.

######  Definition .

A term of the form $x\;\bar{s}_{n}$, for $n\geq 0$, _jells_ with a literal
$t\approx t^{\prime}\in D$ if $t=\tilde{t}\;\bar{y}_{n}$ and
$t^{\prime}=\tilde{t}\kern 0.83328pt^{\prime}\>\bar{y}_{n}$ for some terms
$\tilde{t}$, $\tilde{t}\kern 0.83328pt^{\prime}$ and distinct variables
$\bar{y}_{n}$ that do not occur elsewhere in $D.$

Using the naming convention from Definition 12.1 for $\tilde{t}\kern
0.83328pt^{\prime}$, the variable condition can be stated as follows:

> If $u$ has a variable head $x$ and jells with the literal $t\approx
> t^{\prime}\in D$, there must exist a grounding substitution $\theta$ with
> $t\sigma\theta\succ t^{\prime}\sigma\theta$ and $C\sigma\theta\prec
> C^{\prime\prime}\sigma\theta$, where
> $C^{\prime\prime}=C\\{x\mapsto\tilde{t}\kern 0.83328pt^{\prime}\\}$.

If $C$ is first-order, this amounts to $u\notin\mathcalx{V}\\!$. Since the
order is compatible with green contexts, the substitution $\theta$ can exist
only if $x$ occurs applied in $C$.

Moreover, the extensional nonpurifying calculus has one additional rule, the
positive extensionality rule, and one axiom, the extensionality axiom. The
rule is

$\prftree[r]{\small{\textsc{PosExt}}}{C^{\prime}\mathrel{\lor}s\;\bar{x}\approx
s^{\prime}\>\bar{x}}{C^{\prime}\mathrel{\lor}s\approx s^{\prime}}$

where

  1. 1.

$\bar{x}$ is a tuple of distinct variables that do not occur in $C^{\prime}$,
$s$, or $s^{\prime}$

  2. 2.

$s\;\bar{x}\approx s^{\prime}\>\bar{x}$ is strictly eligible in the premise.

The extensionality axiom uses a polymorphic Skolem symbol
$\mathsf{diff}:\mathsf{\Pi}\alpha,\beta.\;{(\alpha\rightarrow\beta)}^{2}\rightarrow{\alpha}$
characterized by the axiom

$\displaystyle x\;(\mathsf{diff}{\langle\alpha,\beta\rangle}\;x\;y)\not\approx
y\>(\mathsf{diff}{\langle\alpha,\beta\rangle}\;x\;y)\mathrel{\lor}x\approx y$
(Ext)

Unlike the nonpurifying calculi, the purifying calculi never perform
superposition at variables. Instead, they rely on purification [Bra75, DH86,
SS89, SL91] (also called abstraction) to circumvent nonmonotonicity. The idea
is to rename apart problematic occurrences of a variable $x$ in a clause to
$x_{1},\dots,x_{n}$ and to add _purification literals_ $x_{1}\not\approx x$,
…, $x_{n}\not\approx x$ to connect the new variables to $x$. We must then
ensure that all clauses are purified, by processing the initial clause set and
the conclusion of every inference or simplification.

In the intensional purifying calculus, the purification
$\operatorname{\operatorname{\mathcalx{pure}}}(C)$ of clause $C$ is defined as
the result of the following procedure. Choose a variable $x$ that occurs
applied in $C$ and also unapplied in a literal of $C$ that is not of the form
$x\not\approx y$. If no such variable exists, terminate. Otherwise, replace
all unapplied occurrences of $x$ in $C$ by a fresh variable $x^{\prime}$ and
add the purification literal $x^{\prime}\not\approx x$. Then repeat these
steps with another variable. The procedure terminates because the number of
variables that can be chosen reduces with each step. For example,

$\operatorname{\operatorname{\mathcalx{pure}}}(x\;{\mathsf{a}}\approx
x\;{\mathsf{b}}\mathrel{\lor}{\mathsf{f}}\;x\approx{\mathsf{g}}\;x)\kern
0.83328pt=\kern 0.83328ptx\;{\mathsf{a}}\approx
x\;{\mathsf{b}}\mathrel{\lor}{\mathsf{f}}\;x^{\prime}\approx{\mathsf{g}}\;x^{\prime}\mathrel{\lor}x\not\approx
x^{\prime}$

The variable condition is standard:

> The term $u$ is not a variable.

The conclusion $C$ of ArgCong is changed to
$\operatorname{\operatorname{\mathcalx{pure}}}(C)$; the other rules preserve
purity of their premises.

In the extensional purifying calculus,
$\operatorname{\operatorname{\mathcalx{pure}}}(C)$ is defined as follows.
Choose a variable $x$ occurring in green subterms $x\;\bar{u}$ and
$x\;\bar{v}$ in literals of $C$ that are not of the form $x\not\approx y$,
where $\bar{u}$ and $\bar{v}$ are distinct (possibly empty) term tuples. If no
such variable exists, terminate. Otherwise, replace all green subterms
$x\;\bar{v}$ with $x^{\prime}\>\bar{v}$, where $x^{\prime}$ is fresh, and add
the purification literal $x^{\prime}\not\approx x$. Then repeat the procedure
until no variable fulfilling the requirements is left. The procedure
terminates because the number of variables fulfilling the requirements does
not increase and with each step, the number of distinct tuples $\bar{u}$ and
$\bar{v}$ fulfilling the requirements decreases for the chosen variable $x$.
For example,

$\operatorname{\operatorname{\mathcalx{pure}}}(x\;{\mathsf{a}}\approx
x\;{\mathsf{b}}\mathrel{\lor}{\mathsf{f}}\;x\approx{\mathsf{g}}\;x)\kern
0.83328pt=\kern 0.83328ptx\;{\mathsf{a}}\approx
x^{\prime}\;{\mathsf{b}}\mathrel{\lor}{\mathsf{f}}\;x^{\prime\prime}\approx{\mathsf{g}}\;x^{\prime\prime}\mathrel{\lor}x^{\prime}\not\approx
x\mathrel{\lor}x^{\prime\prime}\not\approx x$

Like the extensional nonpurifying calculus, this calculus also contains the
PosExt rule and axiom (Ext) introduced above. The variable condition is as
follows:

> Either $u$ has a nonvariable head or $u$ does not jell with the literal
> $t\approx t^{\prime}\in D.$

The conclusion $E$ of each rule is changed to
$\operatorname{\operatorname{\mathcalx{pure}}}(E)$, except for PosExt, which
preserves purity.

Finally, we impose further restrictions on literal selection. In the
nonpurifying calculi, a literal must not be selected if $x\;\bar{u}$ is a
maximal term of the clause and the literal contains a green subterm
$x\;\bar{v}$ with $\bar{v}\neq\bar{u}$. In the purifying calculi, a literal
must not be selected if it contains a variable of functional type. These
restrictions are needed in our completeness proof to show that superposition
inferences below variables are redundant. For the purifying calculi, the
restriction is also needed to avoid inferences whose conclusion is identical
to their premise, such as

$\prftree[r]{\small{\textsc{{ERes}}}}{z\>{\mathsf{a}}\approx{\mathsf{b}}\mathrel{\lor}z\not\approx
x\mathrel{\lor}{\mathsf{f}}\not\approx
x}{z\>{\mathsf{a}}\approx{\mathsf{b}}\mathrel{\lor}z^{\prime}\not\approx{\mathsf{f}}\mathrel{\lor}z^{\prime}\not\approx
z}$

where ${\mathsf{f}}\not\approx x$ is selected. For the nonpurifying calculi,
it might be possible to avoid the restriction at the cost of a more elaborate
argument.

######  Example .

We illustrate the different variable condition with a few examples. Consider a
left-to-right LPO [BWW17] instance with precedence
${\mathsf{h}}\succ{\mathsf{g}}\succ{\mathsf{f}}\succ{\mathsf{c}}\succ{\mathsf{b}}\succ{\mathsf{a}}$.
Given the clauses $D$ and $C$ of a superposition inference in which the grayed
subterms are unified, we list below whether each calculus’s variable condition
is fulfilled (✓) or not.

$D$ $C$ XXintensional nonpurifying Xextensional nonpurifying Xintensional
purifying Xextensional purifying $\smash{\hbox{\pagecolor{light-
gray}$\vphantom{(^{\prime}q}{{\mathsf{h}}}$}}\approx{\mathsf{g}}$
${\mathsf{f}}\>\smash{\hbox{\pagecolor{light-
gray}$\vphantom{(^{\prime}q}{y}$}}\approx{\mathsf{c}}$
$\smash{\hbox{\pagecolor{light-
gray}$\vphantom{(^{\prime}q}{{\mathsf{f}}\;({\mathsf{h}}\;{\mathsf{a}})}$}}\approx{\mathsf{h}}$
${\mathsf{g}}\;\smash{\hbox{\pagecolor{light-
gray}$\vphantom{(^{\prime}q}{{\mathit{y}}}$}}\approx{\mathit{y}}\;{\mathsf{b}}$
✓ ✓ $\smash{\hbox{\pagecolor{light-
gray}$\vphantom{(^{\prime}q}{{\mathsf{h}}\;{\mathit{x}}}$}}\approx{\mathsf{f}}\>{\mathit{x}}$
${\mathsf{g}}\;(\smash{\hbox{\pagecolor{light-
gray}$\vphantom{(^{\prime}q}{{\mathit{y}}\;{\mathsf{b}}}$}})\;{\mathit{y}}\approx{\mathsf{a}}$
✓ ✓ $x\approx{\mathsf{c}}\mathrel{\lor}\smash{\hbox{\pagecolor{light-
gray}$\vphantom{(^{\prime}q}{{\mathsf{h}}\;{\mathit{x}}}$}}\approx{\mathsf{f}}\>{\mathit{x}}$
${\mathsf{g}}\;(\smash{\hbox{\pagecolor{light-
gray}$\vphantom{(^{\prime}q}{{\mathit{y}}\;{\mathsf{b}}}$}})\;{\mathit{y}}\approx{\mathsf{a}}$
✓ ✓ ✓ ✓

For the purifying calculi, the clauses would actually undergo purification
first, but this has no impact on the variable conditions. In the last row, the
term $y\>{\mathsf{b}}$ does not jell with
${\mathsf{h}}\>x\approx{\mathsf{f}}\>x\in D$ because $x$ occurs also in the
first literal of $D$.

######  Remark .

In descriptions of first-order logic with equality, the property $y\approx
y^{\prime}\mathrel{{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color<EMAIL_ADDRESS>to0.0pt{\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}$\blacksquare$\hss}\kern-3.87495pt}\joinrel{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rightarrow}}{\mathsf{f}}(\bar{x},y,\bar{z})\approx{\mathsf{f}}(\bar{x},y^{\prime}\\!,\bar{z})$
is often referred to as “function congruence.” It seems natural to use the
same label for the higher-order version $t\approx
t^{\prime}\mathrel{{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color<EMAIL_ADDRESS>to0.0pt{\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}$\blacksquare$\hss}\kern-3.87495pt}\joinrel{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rightarrow}}s\;t\approx
s\;t^{\prime}$ and to call the companion property $s\approx
s^{\prime}\mathrel{{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color<EMAIL_ADDRESS>to0.0pt{\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}$\blacksquare$\hss}\kern-3.87495pt}\joinrel{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rightarrow}}s\;t\approx
s^{\prime}\>t$ “argument congruence,” whence the name ArgCong for our
inference rule. This nomenclature is far from universal; for example, the
Isabelle/HOL theorem fun_cong captures argument congruence and arg_cong
captures function congruence.

###  12.2. Rationale for the Inference Rules

A key restriction of all four calculi is that they superpose only at green
subterms, mirroring the term order’s compatibility with green contexts. The
ArgCong rule then makes it possible to simulate superposition at nongreen
subterms. However, in conjunction with the Sup rules, ArgCong can exhibit an
unpleasant behavior, which we call _argument congruence explosion_ :

$\displaystyle\prftree[l]{\small{\textsc{Sup}}}{\prftree[l]{\small{\textsc{ArgCong}}}{{\mathsf{g}}\approx{\mathsf{f}}}{{\mathsf{g}}\;{\mathit{x}}\approx{\mathsf{f}}\>{\mathit{x}}}}{{\mathit{h}}\;{\mathsf{a}}\not\approx{\mathsf{b}}}{{\mathsf{f}}\;{\mathsf{a}}\not\approx{\mathsf{b}}}\kern
17.50002pt\prftree[l]{\small{\textsc{Sup}}}{\prftree[l]{\small{\textsc{ArgCong}}}{{\mathsf{g}}\approx{\mathsf{f}}}{{\mathsf{g}}\;{\mathit{x}}\;{\mathit{y}}\;{\mathit{z}}\approx{\mathsf{f}}\>{\mathit{x}}\;{\mathit{y}}\;{\mathit{z}}}}{{\mathit{h}}\;{\mathsf{a}}\not\approx{\mathsf{b}}}{{\mathsf{f}}\>{\mathit{x}}\;{\mathit{y}}\;{\mathsf{a}}\not\approx{\mathsf{b}}}$

In both derivation trees, the higher-order variable ${\mathit{h}}$ is
effectively the target of a Sup inference. Such derivations essentially amount
to superposition at variable positions (as shown on the left) or even
superposition below variable positions (as shown on the right), both of which
can be extremely prolific. In standard superposition, the explosion is averted
by the condition on the Sup rule that $u\notin\mathcalx{V}\kern-0.83328pt.$ In
the extensional purifying calculus, the variable condition tests that either
$u$ has a nonvariable head or $u$ does not jell with the literal $t\approx
t^{\prime}\in D,$ which prevents derivations such as the above. In the
corresponding nonpurifying calculus, some such derivations may need to be
performed when the term order exhibits nonmonotonicity for the terms of
interest.

In the intensional calculi, the explosion can arise because the variable
conditions are weaker. The following example shows that the intensional
nonpurifying calculus would be incomplete if we used the variable condition of
the extensional nonpurifying calculus.

######  Example .

Consider a left-to-right LPO [BWW17] instance with precedence
${\mathsf{h}}\succ{\mathsf{g}}\succ{\mathsf{f}}\succ{\mathsf{b}}\succ{\mathsf{a}}$,
and consider the following unsatisfiable clause set:

$\displaystyle{\mathsf{h}}\;{\mathit{x}}$
$\displaystyle\approx{\mathsf{f}}\>{\mathit{x}}$
$\displaystyle{\mathsf{g}}\;({\mathit{x}}\;{\mathsf{b}})\;{\mathit{x}}$
$\displaystyle\approx{\mathsf{a}}$
$\displaystyle{\mathsf{g}}\;({\mathsf{f}}\;{\mathsf{b}})\;{\mathsf{h}}$
$\displaystyle\not\approx{\mathsf{a}}$

The only possible inference is a Sup inference of the first into the second
clause, but the variable condition of the extensional nonpurifying calculus is
not met.

It is unclear whether the variable condition of the intensional purifying
calculus could be strengthened, but our completeness proof suggests that it
cannot.

The variable conditions in the extensional calculi are designed to prevent the
argument congruence explosion shown above, but since they consider only the
shape of the clauses, they might also block Sup inferences whose side premises
do not originate from ArgCong. This is why we need the PosExt rule.

######  Example .

In the following unsatisfiable clause set, the only possible inference from
these clauses in the extensional nonpurifying calculus is PosExt, showing its
necessity:

$\displaystyle{\mathsf{g}}\;{\mathit{x}}$
$\displaystyle\approx{\mathsf{f}}\>{\mathit{x}}$ $\displaystyle{\mathsf{g}}$
$\displaystyle\not\approx{\mathsf{f}}$ $\displaystyle
x\;(\mathsf{diff}{\langle\alpha,\beta\rangle}\;x\;y)\not\approx
y\>(\mathsf{diff}{\langle\alpha,\beta\rangle}\;x\;y)\mathrel{\lor}x\approx y$

The same argument applies for the purifying calculus with the difference that
the third clause must be purified.

Due to nonmonotonicity, for refutational completeness we need either to purify
the clauses or to allow some superposition at variable positions, as mandated
by the respective variable conditions. Without either of these measures, at
least the extensional calculi and presumably also the intensional calculi
would be incomplete, as the next example demonstrates.

######  Example .

Consider the following clause set:

$\begin{gathered}{\mathsf{k}}\;({\mathsf{g}}\;{\mathit{x}})\approx{\mathsf{k}}\;({\mathit{x}}\;{\mathsf{b}})\quad{\mathsf{k}}\;({\mathsf{f}}\;({\mathsf{h}}\;{\mathsf{a}})\;{\mathsf{b}})\not\approx{\mathsf{k}}\;({\mathsf{g}}\;{\mathsf{h}})\quad{\mathsf{f}}\;({\mathsf{h}}\;{\mathsf{a}})\approx{\mathsf{h}}\quad{\mathsf{f}}\;({\mathsf{h}}\;{\mathsf{a}})\;{\mathit{x}}\approx{\mathsf{h}}\;{\mathit{x}}\\\
x\;(\mathsf{diff}{\langle\alpha,\beta\rangle}\;x\;y)\not\approx
y\>(\mathsf{diff}{\langle\alpha,\beta\rangle}\;x\;y)\mathrel{\lor}x\approx
y\end{gathered}$

Using a left-to-right LPO [BWW17] instance with precedence
${\mathsf{k}}\succ{\mathsf{h}}\succ{\mathsf{g}}\succ{\mathsf{f}}\succ{\mathsf{b}}\succ{\mathsf{a}}$,
this clause set is saturated w.r.t. the extensional purifying calculus when
omitting purification. It also quickly saturates using the extensional
nonpurifying calculus when omitting Sup inferences at variables. By contrast,
the intensional calculi derive $\bot$, even without purification and without
Sup inferences at variables, because of the less restrictive variable
conditions.

This raises the question as to whether the intensional calculi actually need
to purify or to perform Sup inferences at variables. We conjecture that
omitting purification and Sup inferences at variables in the intensional
calculi is complete when redundant clauses are kept but that it is incomplete
in general.

We initially considered inference rules instead of axiom (Ext). However, we
did not find a set of inference rules that is complete and leads to fewer
inferences than (Ext). We considered the PosExt rule described above in
combination with the following rule:

$\displaystyle\prftree[r]{\small{\textsc{NegExt}}}{C\mathrel{\lor}s\not\approx
t}{C\mathrel{\lor}s\>({\mathsf{sk}}{\langle\bar{\alpha}\rangle}\>\bar{x}_{n})\not\approx
t\>({\mathsf{sk}}{\langle\bar{\alpha}\rangle}\>\bar{x}_{n})}$

where ${\mathsf{sk}}$ is a fresh Skolem symbol and $\bar{\alpha}$ and
$\bar{x}_{n}$ are the type and term variables occurring free in the literal
$s\not\approx t$. However, these two rules do not suffice for a refutationally
complete calculus, as the following example demonstrates:

######  Example .

Consider the clause set

$\displaystyle{\mathsf{f}}\;x\approx{\mathsf{a}}$
$\displaystyle{\mathsf{g}}\;x\approx{\mathsf{a}}$
$\displaystyle{\mathsf{h}}\;{\mathsf{f}}\approx{\mathsf{b}}$
$\displaystyle{\mathsf{h}}\;{\mathsf{g}}\not\approx{\mathsf{b}}$

Assuming that all four equations are oriented from left to right, this set is
saturated w.r.t. the extensional calculi if (Ext) is replaced by NegExt; yet
it is unsatisfiable in an extensional logic.

######  Example .

A significant advantage of our calculi over the use of standard superposition
on applicatively encoded problems is the flexibility they offer in orienting
equations. The following equations provide two definitions of addition on
Peano numbers:

$\displaystyle{\mathsf{add_{L}}}\,{\mathsf{Zero}}\;{\mathit{y}}$
$\displaystyle\approx{\mathit{y}}$
$\displaystyle{\mathsf{add_{R}}}\;{\mathit{x}}\;{\mathsf{Zero}}$
$\displaystyle\approx{\mathit{x}}$
$\displaystyle{\mathsf{add_{L}}}\,({\mathsf{Succ}}\;x)\;{\mathit{y}}$
$\displaystyle\approx{\mathsf{add_{L}}}\,x\;({\mathsf{Succ}}\;{\mathit{y}})$
$\displaystyle{\mathsf{add_{R}}}\;{\mathit{x}}\;({\mathsf{Succ}}\;{\mathit{y}})$
$\displaystyle\approx{\mathsf{add_{R}}}\;({\mathsf{Succ}}\;{\mathit{x}})\;y$

Let
${\mathsf{add_{L}}}\,(\smash{{\mathsf{Succ}}^{100}}\;{\mathsf{Zero}})\;{\mathsf{n}}\not\approx{\mathsf{add_{R}}}\;{\mathsf{n}}\;(\smash{{\mathsf{Succ}}^{100}}\;{\mathsf{Zero}})$
be the negated conjecture. With LPO, we can use a left-to-right comparison for
${\mathsf{add_{L}}}$’s arguments and a right-to-left comparison for
${\mathsf{add_{R}}}$’s arguments to orient all four equations from left to
right. Then the negated conjecture can be simplified to
${\mathsf{Succ}}^{100}\,{\mathsf{n}}\not\approx{\mathsf{Succ}}^{100}\,{\mathsf{n}}$
by simplification (demodulation), and $\bot$ can be derived with a single
inference. If we use the applicative encoding instead, there is no instance of
LPO or KBO that can orient both recursive equations from left to right. For at
least one of the two sides of the negated conjecture, simplification is
replaced by 100 Sup inferences, which is much less efficient, especially in
the presence of additional axioms.

###  12.3. Soundness

To show the inferences’ soundness, we need the substitution lemma for our
logic:

######  Lemma  (Substitution lemma).

Let
$\mathcal{I}=(\mathcalx{U},\mathcalx{J}_{\mathsf{ty}},\mathcalx{J},\mathcalx{E})$
be a $\lambda$-free higher-order interpretation. Then

$\smash{\llbracket\tau\kern-0.83328pt\rho\rrbracket_{\mathcal{I}_{\mathsf{ty}}}^{\smash{\xi}}}=\smash{\llbracket\tau\rrbracket_{\mathcal{I}_{\mathsf{ty}}}^{\smash{\xi^{\prime}}}}\text{
and }\smash{\llbracket
t\rho\rrbracket_{\mathcal{I}}^{\smash{\xi}}}=\smash{\llbracket
t\rrbracket_{\mathcal{I}}^{\smash{\xi^{\prime}}}}$

for all terms $t$, all types $\tau$, and all substitutions $\rho$, where
$\xi^{\prime}(\alpha)=\smash{\llbracket\alpha\rho\rrbracket_{\mathcal{I}_{\mathsf{ty}}}^{\smash{\xi}}}$
for all type variables $\alpha$ and $\xi^{\prime}(x)=\smash{\llbracket
x\rho\rrbracket_{\mathcal{I}}^{\smash{\xi}}}$ for all term variables $x$.

###### Proof.

First, we prove that
$\smash{\llbracket\tau\kern-0.83328pt\rho\rrbracket_{\mathcal{I}_{\mathsf{ty}}}^{\smash{\xi}}}=\smash{\llbracket\tau\rrbracket_{\mathcal{I}_{\mathsf{ty}}}^{\smash{\xi^{\prime}}}}$
by induction on the structure of $\tau$. If $\tau=\alpha$ is a type variable,

$\smash{\llbracket\alpha\rho\rrbracket_{\mathcal{I}_{\mathsf{ty}}}^{\smash{\xi}}}=\xi^{\prime}(\alpha)=\smash{\llbracket\alpha\rrbracket_{\mathcal{I}_{\mathsf{ty}}}^{\smash{\xi^{\prime}}}}$

If $\tau=\kappa(\bar{\upsilon})$ for some type constructor $\kappa$ and types
$\bar{\upsilon}$,

$\smash{\llbracket\kappa(\bar{\upsilon})\rho\rrbracket_{\mathcal{I}_{\mathsf{ty}}}^{\smash{\xi}}}=\mathcalx{J}_{\mathsf{ty}}(\kappa)(\smash{\llbracket\bar{\upsilon}\rho\rrbracket_{\mathcal{I}_{\mathsf{ty}}}^{\smash{\xi}}})\overset{\smash{\scriptscriptstyle\text{IH}}}{=}\mathcalx{J}_{\mathsf{ty}}(\kappa)(\smash{\llbracket\bar{\upsilon}\rrbracket_{\mathcal{I}_{\mathsf{ty}}}^{\smash{\xi^{\prime}}}})=\smash{\llbracket\kappa(\bar{\upsilon})\rrbracket_{\mathcal{I}_{\mathsf{ty}}}^{\smash{\xi^{\prime}}}}$

Next, we prove $\smash{\llbracket
t\rho\rrbracket_{\mathcal{I}}^{\smash{\xi}}}=\smash{\llbracket
t\rrbracket_{\mathcal{I}}^{\smash{\xi^{\prime}}}}$ by structural induction on
$t$. If $t=y$, then by the definition of the denotation of a variable

$\smash{\llbracket
y\rho\rrbracket_{\mathcal{I}}^{\smash{\xi}}}=\xi^{\prime}(y)=\smash{\llbracket
y\rrbracket_{\mathcal{I}}^{\smash{\xi^{\prime}}}}$

If $t={\mathsf{f}}{\langle\bar{\tau}\rangle}$, then by the definition of the
term denotation

$\smash{\llbracket{\mathsf{f}}{\langle\bar{\tau}\rangle}\rho\rrbracket_{\mathcal{I}}^{\smash{\xi}}}=\mathcalx{J}({\mathsf{f}},\smash{\llbracket\bar{\tau}\rho\rrbracket_{\mathcal{I}_{\mathsf{ty}}}^{\smash{\xi}}})=\mathcalx{J}({\mathsf{f}},\smash{\llbracket\bar{\tau}\rrbracket_{\mathcal{I}_{\mathsf{ty}}}^{\smash{\xi^{\prime}}}})=\smash{\llbracket{\mathsf{f}}{\langle\bar{\tau}\rangle}\rrbracket_{\mathcal{I}}^{\smash{\xi^{\prime}}}}$

If $t=u\>v$, then by the definition of the term denotation

$\smash{\llbracket(u\>v)\rho\rrbracket_{\mathcal{I}}^{\smash{\xi}}}=\mathcalx{E}_{U_{1},U_{2}}(\smash{\llbracket
u\rho\rrbracket_{\mathcal{I}}^{\smash{\xi}}})(\smash{\llbracket
v\rho\rrbracket_{\mathcal{I}}^{\smash{\xi}}})\overset{\smash{\scriptscriptstyle\text{IH}}}{=}\mathcalx{E}_{U_{1},U_{2}}(\smash{\llbracket
u\rrbracket_{\mathcal{I}}^{\smash{\xi^{\prime}}}})(\smash{\llbracket
v\rrbracket_{\mathcal{I}}^{\smash{\xi^{\prime}}}})=\smash{\llbracket
u\>v\rrbracket_{\mathcal{I}}^{\smash{\xi^{\prime}}}}$

where $u$ is of type $\tau\rightarrow\upsilon$,
$U_{1}=\smash{\llbracket\tau\kern-0.83328pt\rho\rrbracket_{\mathcal{I}_{\mathsf{ty}}}^{\smash{\xi}}}=\smash{\llbracket\tau\rrbracket_{\mathcal{I}_{\mathsf{ty}}}^{\smash{\xi^{\prime}}}}$,
and
$U_{2}=\smash{\llbracket\upsilon\rho\rrbracket_{\mathcal{I}_{\mathsf{ty}}}^{\smash{\xi}}}=\smash{\llbracket\upsilon\rrbracket_{\mathcal{I}_{\mathsf{ty}}}^{\smash{\xi^{\prime}}}}$.
∎

######  Lemma .

If $\mathcal{I}\models C$ for some interpretation $\mathcal{I}$ and some
clause $C$, then $\mathcal{I}\models C\rho$ for all substitutions $\rho$.

###### Proof.

We need to show that $C\rho$ is true in $\mathcal{I}$ for all valuations
$\xi$. Given a valuation $\xi$, define $\xi^{\prime}$ as in Lemma 12.3. Then,
by Lemma 12.3, a literal in $C\rho$ is true in $\mathcal{I}$ for $\xi$ if and
only if the corresponding literal in $C$ is true in $\mathcal{I}$ for
$\xi^{\prime}$. There must be at least one such literal because
$\mathcal{I}\models C$ and hence $C$ is in particular true in $\mathcal{I}$
for $\xi^{\prime}$. Therefore, $C\rho$ is true in $\mathcal{I}$ for $\xi$. ∎

######  Theorem  (Soundness of the intensional calculi).

The inference rules Sup, ERes, EFact, and ArgCong are sound (even without the
variable condition and the side conditions on order and eligibility).

###### Proof.

We fix an inference and an interpretation $\mathcal{I}$ that is a model of the
premises. We need to show that it is also a model of the conclusion.

From the definition of the denotation of a term, it is obvious that congruence
holds at all subterms in our logic. By Lemma 12.3, $\mathcal{I}$ is a model of
the $\sigma$-instances of the premises as well, where $\sigma$ is the
substitution used for the inference. Fix a valuation $\xi$. By making case
distinctions on the truth in $\mathcal{I}$ under $\xi$ of the literals of the
$\sigma$-instances of the premises, using the conditions that $\sigma$ is a
unifier, and applying congruence, it follows that the conclusion is also true
in $\mathcal{I}$ under $\xi$. ∎

######  Theorem  (Soundness of the extensional calculi).

The inference rules Sup, ERes, EFact, ArgCong, and PosExt are sound w.r.t.
extensional interpretations (even without the variable condition and the side
conditions on order and eligibility).

###### Proof.

We only need to prove PosExt sound. For the other rules, we can proceed as in
Theorem 12.3. By induction on the length of $\bar{x}$, it suffices to prove
PosExt sound for one variable $x$ instead of a tuple $\bar{x}$. We fix an
inference and an extensional interpretation $\mathcal{I}$ that is a model of
the premise $C^{\prime}\mathrel{\lor}s\>x\approx s^{\prime}\>x$. We need to
show that it is also a model of the conclusion
$C^{\prime}\mathrel{\lor}s\approx s^{\prime}$.

Let $\xi$ be a valuation. If $C^{\prime}$ is true in $\mathcal{I}$ under
$\xi$, the conclusion is clearly true as well. Otherwise $C^{\prime}$ is false
in $\mathcal{I}$ under $\xi$, and also under $\xi[x\mapsto a]$ for all $a$
because $x$ does not occur in $C^{\prime}$. Since the premise is true in
$\mathcal{I}$, $s\>x=s^{\prime}\>x$ must be true in $\mathcal{I}$ under
$\xi[x\mapsto a]$ for all $a$. Hence, for appropriate universes $U_{1},U_{2}$,
we have $\mathcalx{E}_{U_{1},U_{2}}(\smash{\llbracket
s\rrbracket_{\mathcal{I}}^{\smash{\xi[x\mapsto a]}}})(a)=\smash{\llbracket
s\>x\rrbracket_{\mathcal{I}}^{\smash{\xi[x\mapsto a]}}}=\smash{\llbracket
s^{\prime}\>x\rrbracket_{\mathcal{I}}^{\smash{\xi[x\mapsto
a]}}}=\mathcalx{E}_{U_{1},U_{2}}(\smash{\llbracket
s^{\prime}\rrbracket_{\mathcal{I}}^{\smash{\xi[x\mapsto a]}}})(a)$. Since $s$
and $s^{\prime}$ do not contain $x$, $\smash{\llbracket
s\rrbracket_{\mathcal{I}}^{\smash{\xi[x\mapsto a]}}}$ and $\smash{\llbracket
s^{\prime}\rrbracket_{\mathcal{I}}^{\smash{\xi[x\mapsto a]}}}$ do not depend
on $a$. Thus, $\mathcalx{E}_{U_{1},U_{2}}(\smash{\llbracket
s\rrbracket_{\mathcal{I}}^{\smash{\xi}}})=\mathcalx{E}_{U_{1},U_{2}}(\smash{\llbracket
s^{\prime}\rrbracket_{\mathcal{I}}^{\smash{\xi}}})$. Since $\mathcal{I}$ is
extensional, $\mathcalx{E}_{U_{1},U_{2}}$ is injective and hence
$\smash{\llbracket s\rrbracket_{\mathcal{I}}^{\smash{\xi}}}=\smash{\llbracket
s^{\prime}\rrbracket_{\mathcal{I}}^{\smash{\xi}}}$. It follows that $s\approx
s^{\prime}$ is true in $\mathcal{I}$ under $\xi$, and so is the entire
conclusion of the inference. ∎

A problem expressed in higher-order logic must be transformed into clausal
normal form before the calculi can be applied. This process works as in the
first-order case, except for skolemization. The issue is that skolemization,
when performed naively, is unsound for higher-order logic with a Henkin
semantics [Mil87,

##  13\.

6] , because it introduces new functions that can be used to instantiate
variables.

The core of this article is not affected by this because the problems are
given in clausal form. For the implementation, we claim soundness only w.r.t.
models that satisfy the axiom of choice, which is the semantics mandated by
the TPTP THF format [SBBT09]. By contrast, refutational completeness holds
w.r.t. arbitrary models as defined above. Alternatively, skolemization can be
made sound by introducing mandatory arguments as described by Miller [Mil87,

##  14\.

6] and in the conference version of this article [BBCW18].

This issue also affects axiom (Ext) because it contains the Skolem symbol
$\mathsf{diff}$. As a consequence, (Ext) does not hold in all extensional
interpretations. The extensional calculi are thus only sound w.r.t.
interpretations in which (Ext) holds. However, we can prove that (Ext) is
compatible with our logic:

######  Theorem .

Axiom (Ext) is satisfiable.

###### Proof.

For a given signature, let
$(\mathcalx{U},\mathcalx{J}_{\mathsf{ty}},\mathcalx{J},\mathcalx{E})$ be an
Herbrand interpretation. That is, we define $\mathcalx{U}$ to contain the set
$\mathcalx{U}_{\tau}$ of all terms of type $\tau$ for each ground type $\tau$,
we define $\mathcalx{J}_{\mathsf{ty}}$ by
$\mathcalx{J}_{\mathsf{ty}}(\kappa)(\bar{\tau})=\kappa(\bar{\tau})$, we define
$\mathcalx{J}$ by
$\mathcalx{J}({\mathsf{f}},\mathcalx{U}_{\bar{\tau}})={\mathsf{f}}{\langle\bar{\tau}\rangle}$,
and we define $\mathcalx{E}$ by
$\mathcalx{E}_{U_{\tau},U_{\upsilon}}({\mathsf{f}})({\mathsf{a}})={\mathsf{f}}\>{\mathsf{a}}$.
Then $\mathcalx{E}_{U_{\tau},U_{\upsilon}}$ is clearly injective and hence
$\mathcal{I}$ is extensional. To show that $\mathcal{I}\models(\textsc{Ext})$,
we need to show that (Ext) is true under all valuations. Let $\xi$ be a
valuation. If $x\approx y$ is true under $\xi$, (Ext) is also true. Otherwise
$x\approx y$ is false under $\xi$, and hence $\xi(x)\not=\xi(y)$. Then we have
$\smash{\llbracket
x\;(\mathsf{diff}{\langle\alpha,\beta\rangle}\;x\;y)\rrbracket_{\mathcal{I}}^{\smash{\xi}}}=(\xi(x))\;(\mathsf{diff}{\langle\alpha,\beta\rangle}\;(\xi(x))\;(\xi(y)))\not=(\xi(y))\;(\mathsf{diff}{\langle\alpha,\beta\rangle}\;(\xi(x))\;(\xi(y)))=\smash{\llbracket
y\>(\mathsf{diff}{\langle\alpha,\beta\rangle}\;x\;y)\rrbracket_{\mathcal{I}}^{\smash{\xi}}}$.
Therefore, $x\;(\mathsf{diff}{\langle\alpha,\beta\rangle}\;x\;y)\not\approx
y\>(\mathsf{diff}{\langle\alpha,\beta\rangle}\;x\;y)$ is true in $\mathcal{I}$
under $\xi$ and so is (Ext). ∎

###  14.1. The Redundancy Criterion

For our calculi, a redundant clause cannot simply be defined as a clause whose
ground instances are entailed by smaller ($\prec$) ground instances of
existing clauses, because this would make all ArgCong inferences redundant.
Our solution is to base the redundancy criterion on a weaker ground
logic—ground monomorphic first-order logic—in which argument congruence does
not hold. This logic also plays a central role in our refutational
completeness proof.

We employ an encoding $\mathcalx{F}$ to translate ground $\lambda$-free
higher-order terms into ground first-order terms. It indexes each symbol
occurrence with its type arguments and its term argument count. Thus,
$\mathcalx{F}({\mathsf{f}})={\mathsf{f}}_{0}$,
$\mathcalx{F}({\mathsf{f}}\>{\mathsf{a}})={\mathsf{f}}_{1}({\mathsf{a}}_{0})$,
and
$\mathcalx{F}({\mathsf{g}}{\langle\kappa\rangle})={\mathsf{g}}_{0}^{\kappa}$.
This is enough to disable argument congruence; for example,
$\\{{\mathsf{f}}\approx{\mathsf{h}}{,}\;{\mathsf{f}}\>{\mathsf{a}}\not\approx{\mathsf{h}}\>{\mathsf{a}}\\}$
is unsatisfiable, whereas its encoding
$\\{{\mathsf{f}}_{0}\approx{\mathsf{h}}_{0}{,}\allowbreak\;{\mathsf{f}}_{1}({\mathsf{a}}_{0})\not\approx{\mathsf{h}}_{1}({\mathsf{a}}_{0})\\}$
is satisfiable. For clauses built from fully applied ground terms, the two
logics are isomorphic, as we would expect from a graceful generalization.

Given a $\lambda$-free higher-order signature
$(\mathrm{\Sigma}_{\mathsf{ty}},\mathrm{\Sigma})$, we define a first-order
signature $(\mathrm{\Sigma}_{\mathsf{ty}},\mathrm{\Sigma}_{\mathrm{GF}})$ as
follows. The type constructors $\mathrm{\Sigma}_{\mathsf{ty}}$ are the same in
both signatures, but $\rightarrow$ is uninterpreted in first-order logic. For
each symbol
${\mathsf{f}}:\mathsf{\Pi}\bar{\alpha}_{m}.\;\tau_{1}\rightarrow\cdots\rightarrow\tau_{n}\rightarrow\tau$
in $\mathrm{\Sigma}$, where $\tau$ is not functional, we introduce symbols
${\mathsf{f}}_{l}^{\bar{\upsilon}_{m}}\in\mathrm{\Sigma}_{\mathrm{GF}}$ with
argument types $\bar{\tau}_{l}\sigma$ and return type
$(\tau_{l+1}\rightarrow\cdots\rightarrow\tau_{n}\rightarrow\tau)\sigma$, where
$\sigma=\\{\bar{\alpha}_{m}\mapsto\bar{\upsilon}_{m}\\}$, for each tuple of
ground types $\bar{\upsilon}_{m}$ and each $l\in\\{0,\dots,n\\}$.

For example, let
$\mathrm{\Sigma}=\\{{\mathsf{a}}:\kappa{,}\;{\mathsf{g}}:\kappa\rightarrow\kappa\rightarrow\kappa\\}$.
The corresponding first-order signature is
$\mathrm{\Sigma}_{\mathrm{GF}}=\\{{\mathsf{a}}_{0}:{\kappa}{,}\;{\mathsf{g}}_{0}:{\kappa\rightarrow\kappa\rightarrow\kappa}{,}\;{\mathsf{g}}_{1}:{\kappa\Rightarrow\kappa\rightarrow\kappa}{,}\;{\mathsf{g}}_{2}:{\kappa^{2}\Rightarrow\kappa}\\}$
where ${\mathsf{f}}:{\bar{\tau}\Rightarrow\upsilon}$ denotes a first-order
function symbol ${\mathsf{f}}$ with argument types $\bar{\tau}$ and return
type $\upsilon$, and $\rightarrow$ is an uninterpreted binary type
constructor. The term
$\mathcalx{F}({\mathsf{g}}\;{\mathsf{a}}\;{\mathsf{a}})={\mathsf{g}}_{2}({\mathsf{a}}_{0},{\mathsf{a}}_{0})$
has type ${\kappa}$, and
$\mathcalx{F}({\mathsf{g}}\;{\mathsf{a}})={\mathsf{g}}_{1}({\mathsf{a}}_{0})$
has type ${\kappa\rightarrow\kappa}$.

Thus, we consider three levels of logics: the $\lambda$-free higher-order
level ${\mathrm{H}}$ over a given signature
$(\mathrm{\Sigma}_{\mathsf{ty}},\allowbreak\mathrm{\Sigma})$, the ground
$\lambda$-free higher-order level ${\mathrm{GH}}$, corresponding to
${\mathrm{H}}$’s ground fragment, and the ground monomorphic first-order level
${\mathrm{GF}}$ over the signature
$(\mathrm{\Sigma}_{\mathsf{ty}},\allowbreak\mathrm{\Sigma}_{\mathrm{GF}})$
defined above. We use $\mathcalx{T}_{\mathrm{H}}$,
$\mathcalx{T}_{\mathrm{GH}}$, and $\mathcalx{T}_{\mathrm{GF}}$ to denote the
respective sets of terms, $\mathcalx{Ty}_{\mathrm{H}}$,
$\mathcalx{Ty}_{\mathrm{GH}}$, and $\mathcalx{Ty}_{\mathrm{GF}}$ to denote the
respective sets of types, and $\mathcalx{C}_{\mathrm{H}}$,
$\mathcalx{C}_{\mathrm{GH}}$, and $\mathcalx{C}_{\mathrm{GF}}$ to denote the
respective sets of clauses. In the purifying calculi, we exceptionally let
$\mathcalx{C}_{\mathrm{H}}$ denote the set of purified clauses. Each of the
three levels has an entailment relation $\models$. A clause set $N_{1}$
entails a clause set $N_{2}$, denoted $N_{1}\models N_{2}$, if any model of
$N_{1}$ is also a model of $N_{2}$. On ${\mathrm{H}}$ and ${\mathrm{GH}}$, we
use $\lambda$-free higher-order models for the intensional calculi and
extensional $\lambda$-free higher-order models for the extensional calculi; on
${\mathrm{GF}}$, we use first-order models. This machinery may seem excessive,
but it is essential to define redundancy of clauses and inferences properly,
and it will play an important role in the refutational completeness proof
(Section 16).

The three levels are connected by two functions, $\mathcalx{G}$ and
$\mathcalx{F}$:

######  Definition  (Grounding function ${\mathcalx{G}}$ on terms and
clauses).

The grounding function $\mathcalx{G}$ maps terms
$t\in\mathcalx{T}_{\mathrm{H}}$ to the set of their ground instances—i.e., the
set of all $t\theta\in\mathcalx{T}_{\mathrm{GH}}$ where $\theta$ is a
substitution. It also maps clauses $C\in\mathcalx{C}_{\mathrm{H}}$ to the set
of their ground instances—i.e., the set of all
$C\theta\in\mathcalx{C}_{\mathrm{GH}}$ where $\theta$ is a substitution.

######  Definition  (Encoding ${\mathcalx{F}}$ on terms and clauses).

The encoding
$\mathcalx{F}:\mathcalx{T}_{\mathrm{GH}}\rightarrow\mathcalx{T}_{\mathrm{GF}}$
is recursively defined as
$\mathcalx{F}({\mathsf{f}}{\langle\bar{\upsilon}_{m}\rangle}\;\bar{u}_{l})={\mathsf{f}}_{l}^{\bar{\upsilon}_{m}}({\mathcalx{F}(\bar{u}_{l})})$.
The encoding $\mathcalx{F}$ is extended to map from
$\mathcalx{C}_{\mathrm{GH}}$ to $\mathcalx{C}_{\mathrm{GF}}$ by mapping each
literal and each side of a literal individually.

The encoding $\mathcalx{F}$ is bijective with inverse $\mathcalx{F}^{-1}$.
Using $\mathcalx{F}^{-1}$, the clause order $\succ$ on
$\mathcalx{T}_{\mathrm{GH}}$ can be transferred to
$\mathcalx{T}_{\mathrm{GF}}$ by defining $t\succ s$ as equivalent to
$\mathcalx{F}^{-1}(t)\succ\mathcalx{F}^{-1}(s)$. The property that $\succ$ on
clauses is the multiset extension of $\succ$ on literals, which in turn is the
multiset extension of $\succ$ on terms, is maintained because
$\mathcalx{F}^{-1}$ maps the multiset representations elementwise.

Schematically, the three levels are connected as follows:

pt${\mathrm{H}}$higher-orderpt${\mathrm{GH}}$ground higher-
orderpt${\mathrm{GF}}$ground first-order$\mathcalx{F}$$\mathcalx{G}$

Crucially, green subterms in $\mathcalx{T}_{\mathrm{GH}}$ correspond to
subterms in $\mathcalx{T}_{\mathrm{GF}}$ (Lemma 14.1), whereas nongreen
subterms in $\mathcalx{T}_{\mathrm{GH}}$ are not subterms at all in
$\mathcalx{T}_{\mathrm{GF}}$. For example, ${\mathsf{a}}$ is a green subterm
of ${\mathsf{f}}\>{\mathsf{a}}$, and correspondingly
$\mathcalx{F}({\mathsf{a}})={\mathsf{a}}_{0}$ is a subterm of
$\mathcalx{F}({\mathsf{f}}\>{\mathsf{a}})={\mathsf{f}}_{1}({\mathsf{a}}_{0})$.
On the other hand, ${\mathsf{f}}$ is not a green subterm of
${\mathsf{f}}\>{\mathsf{a}}$, and correspondingly
$\mathcalx{F}({\mathsf{f}})={\mathsf{f}}_{0}$ is not a subterm of
$\mathcalx{F}({\mathsf{f}}\>{\mathsf{a}})={\mathsf{f}}_{1}({\mathsf{a}}_{0})$.

To state the correspondence between green subterms in
$\mathcalx{T}_{\mathrm{GH}}$ and subterms in $\mathcalx{T}_{\mathrm{GF}}$
explicitly, we define positions of green subterms as follows. A term
$s\in\mathcalx{T}_{\mathrm{H}}$ is a green subterm at position $\epsilon$ of
$s$. If a term $s\in\mathcalx{T}_{\mathrm{H}}$ is a green subterm at position
$p$ of $u_{i}$ for some $1\leq i\leq n$, then $s$ is a green subterm at
position $i.p$ of ${\mathsf{f}}{\langle\bar{\tau}\kern
0.83328pt\rangle}\;\bar{u}_{n}$ and of $x\;{\bar{u}}_{n}$. For
$\mathcalx{T}_{\mathrm{GF}}$, positions are defined as usual in first-order
logic.

######  Lemma .

Let $s,t\in\mathcalx{T}_{\mathrm{GH}}$. We have
$\mathcalx{F}(t\begin{picture}(5.0,7.0)\put(1.1,3.0){\rotatebox{45.0}{\line(1,0){6.0}}}
\put(1.1,3.0){\rotatebox{315.0}{\line(1,0){6.0}}} \end{picture}\kern
0.83328pts\begin{picture}(5.0,7.0)\put(0.1,3.0){\rotatebox{135.0}{\line(1,0){6.0}}}
\put(0.1,3.0){\rotatebox{225.0}{\line(1,0){6.0}}}
\end{picture}\,_{p})=\mathcalx{F}(t)[\mathcalx{F}(s)]_{p}$. In other words,
$s$ is a green subterm of $t$ at position $p$ if and only if $\mathcalx{F}(s)$
is a subterm of $\mathcalx{F}(t)$ at position $p$.

###### Proof.

By induction on $p$. If $p=\varepsilon$, then $s=t[s]_{p}$. Hence
$\mathcalx{F}(t[s]_{p})=\mathcalx{F}(s)=\mathcalx{F}(t)\begin{picture}(5.0,7.0)\put(1.1,3.0){\rotatebox{45.0}{\line(1,0){6.0}}}
\put(1.1,3.0){\rotatebox{315.0}{\line(1,0){6.0}}} \end{picture}\kern
0.83328pt\mathcalx{F}(s)\begin{picture}(5.0,7.0)\put(0.1,3.0){\rotatebox{135.0}{\line(1,0){6.0}}}
\put(0.1,3.0){\rotatebox{225.0}{\line(1,0){6.0}}} \end{picture}\,_{p}$. If
$p=i.p^{\prime}$, then
$t[s]_{p}={\mathsf{f}}{{\langle\bar{\tau}\rangle}}\;\bar{u}_{n}$ with
$u_{i}=u_{i}[s]_{p^{\prime}}$. Applying $\mathcalx{F}$, we obtain by the
induction hypothesis that
$\mathcalx{F}(u_{i})=\mathcalx{F}(u_{i})\begin{picture}(5.0,7.0)\put(1.1,3.0){\rotatebox{45.0}{\line(1,0){6.0}}}
\put(1.1,3.0){\rotatebox{315.0}{\line(1,0){6.0}}} \end{picture}\kern
0.83328pt\mathcalx{F}(s)\begin{picture}(5.0,7.0)\put(0.1,3.0){\rotatebox{135.0}{\line(1,0){6.0}}}
\put(0.1,3.0){\rotatebox{225.0}{\line(1,0){6.0}}}
\end{picture}\,_{p^{\prime}}$. Therefore,
$\mathcalx{F}(t[s]_{p})={\mathsf{f}}_{n}^{\bar{\tau}}(\mathcalx{F}(u_{1}),\dots,\allowbreak\mathcalx{F}(u_{i-1}),\allowbreak\mathcalx{F}(u_{i})\begin{picture}(5.0,7.0)\put(1.1,3.0){\rotatebox{45.0}{\line(1,0){6.0}}}
\put(1.1,3.0){\rotatebox{315.0}{\line(1,0){6.0}}} \end{picture}\kern
0.83328pt\mathcalx{F}(s)\begin{picture}(5.0,7.0)\put(0.1,3.0){\rotatebox{135.0}{\line(1,0){6.0}}}
\put(0.1,3.0){\rotatebox{225.0}{\line(1,0){6.0}}}
\end{picture}\,_{p^{\prime}},\mathcalx{F}(u_{i+1}),\dots,\mathcalx{F}(u_{n}))$.
It follows that
$\mathcalx{F}(t[s]_{p})=\mathcalx{F}(t)\begin{picture}(5.0,7.0)\put(1.1,3.0){\rotatebox{45.0}{\line(1,0){6.0}}}
\put(1.1,3.0){\rotatebox{315.0}{\line(1,0){6.0}}} \end{picture}\kern
0.83328pt\mathcalx{F}(s)\begin{picture}(5.0,7.0)\put(0.1,3.0){\rotatebox{135.0}{\line(1,0){6.0}}}
\put(0.1,3.0){\rotatebox{225.0}{\line(1,0){6.0}}} \end{picture}\,_{p}$. ∎

######  Corollary .

Given $s,t\in\mathcalx{T}_{\mathrm{GF}}$, we have
$\mathcalx{F}^{-1}(t[s]_{p})=\mathcalx{F}^{-1}(t)\begin{picture}(5.0,7.0)\put(1.1,3.0){\rotatebox{45.0}{\line(1,0){6.0}}}
\put(1.1,3.0){\rotatebox{315.0}{\line(1,0){6.0}}} \end{picture}\kern
0.83328pt\mathcalx{F}^{-1}(s)\begin{picture}(5.0,7.0)\put(0.1,3.0){\rotatebox{135.0}{\line(1,0){6.0}}}
\put(0.1,3.0){\rotatebox{225.0}{\line(1,0){6.0}}} \end{picture}\,_{p}$.

######  Lemma .

Well-foundedness, totality, compatibility with contexts, and the subterm
property hold for $\succ$ on $\mathcalx{T}_{\mathrm{GF}}$.

###### Proof.

Compatibility with contexts: We must show that $s\succ s^{\prime}$ implies
$t[s]_{p}\succ t[s^{\prime}]_{p}$ for terms
$t,s,s^{\prime}\in\mathcalx{T}_{\mathrm{GF}}$. Assuming $s\succ s^{\prime}$,
we have $\mathcalx{F}^{-1}(s)\succ\mathcalx{F}^{-1}(s^{\prime})$. By
compatibility with green contexts on $\mathcalx{T}_{\mathrm{GH}}$, it follows
that
$\mathcalx{F}^{-1}(t)\begin{picture}(5.0,7.0)\put(1.1,3.0){\rotatebox{45.0}{\line(1,0){6.0}}}
\put(1.1,3.0){\rotatebox{315.0}{\line(1,0){6.0}}} \end{picture}\kern
0.83328pt\mathcalx{F}^{-1}(s)\begin{picture}(5.0,7.0)\put(0.1,3.0){\rotatebox{135.0}{\line(1,0){6.0}}}
\put(0.1,3.0){\rotatebox{225.0}{\line(1,0){6.0}}}
\end{picture}\,_{p}\succ\mathcalx{F}^{-1}(t)\begin{picture}(5.0,7.0)\put(1.1,3.0){\rotatebox{45.0}{\line(1,0){6.0}}}
\put(1.1,3.0){\rotatebox{315.0}{\line(1,0){6.0}}} \end{picture}\kern
0.83328pt\mathcalx{F}^{-1}(s^{\prime})\begin{picture}(5.0,7.0)\put(0.1,3.0){\rotatebox{135.0}{\line(1,0){6.0}}}
\put(0.1,3.0){\rotatebox{225.0}{\line(1,0){6.0}}} \end{picture}\,_{p}$. By
Corollary 14.1, we have $t[s]_{p}\succ t[s^{\prime}]_{p}$.

Well-foundedness: Assume that there exists an infinite descending chain
$t_{1}\succ t_{2}\succ\cdots$ in $\mathcalx{T}_{\mathrm{GF}}$. By applying
$\mathcalx{F}^{-1}$, we then obtain the chain
$\mathcalx{F}^{-1}(t_{1})\succ\mathcalx{F}^{-1}(t_{2})\succ\cdots$ in
$\mathcalx{T}_{\mathrm{GH}}$, contradicting well-foundedness on
$\mathcalx{T}_{\mathrm{GH}}$.

Totality: Let $s,t\in\mathcalx{T}_{\mathrm{GF}}$. Then $\mathcalx{F}^{-1}(t)$
and $\mathcalx{F}^{-1}(s)$ must be comparable by totality in
$\mathcalx{T}_{\mathrm{GH}}$. Hence, $t$ and $s$ are comparable.

Subterm property: By Corollary 14.1 and the subterm property on
$\mathcalx{T}_{\mathrm{GH}}$, we have
$\mathcalx{F}^{-1}(t[s]_{p})=\mathcalx{F}^{-1}(t)\begin{picture}(5.0,7.0)\put(1.1,3.0){\rotatebox{45.0}{\line(1,0){6.0}}}
\put(1.1,3.0){\rotatebox{315.0}{\line(1,0){6.0}}} \end{picture}\kern
0.83328pt\mathcalx{F}^{-1}(s)\begin{picture}(5.0,7.0)\put(0.1,3.0){\rotatebox{135.0}{\line(1,0){6.0}}}
\put(0.1,3.0){\rotatebox{225.0}{\line(1,0){6.0}}}
\end{picture}\,_{p}\succ\mathcalx{F}^{-1}(s)$. Hence, $t[s]_{p}\succ s$. ∎

In standard superposition, redundancy relies on the entailment relation
$\models$ on ground clauses. We will define redundancy on ${\mathrm{GH}}$ and
${\mathrm{H}}$ in the same way, but using ${\mathrm{GF}}$’s entailment
relation. This notion of redundancy gracefully generalizes the first-order
notion, without making all ArgCong inferences redundant.

The standard redundancy criterion for standard superposition cannot justify
subsumption deletion. Following Waldmann et al. [WTRB20], we incorporate
subsumption into the redundancy criterion. A clause $C$ _subsumes_ $D$ if
there exists a substitution $\sigma$ such that $C\sigma\subseteq D$. A clause
$C$ _strictly subsumes_ $D$ if $C$ subsumes $D$ but $D$ does not subsume $C$.
Let $\sqsupset$ stand for “is strictly subsumed by”. Using the applicative
encoding, it is easy to show that $\sqsupset$ is well founded because strict
subsumption is well founded in first-order logic.

We define the sets of redundant clauses w.r.t. a given clause set as follows:

  * –

Given $C\in\mathcalx{C}_{\mathrm{GF}}$ and
$N\subseteq\mathcalx{C}_{\mathrm{GF}}$, let
$C\in\mathit{GFRed}_{\mathrm{C}}(N)$ if $\\{D\in N\mid D\prec C\\}\models C$.

  * –

Given $C\in\mathcalx{C}_{\mathrm{GH}}$ and
$N\subseteq\mathcalx{C}_{\mathrm{GH}}$, let
$C\in\mathit{GHRed}_{\mathrm{C}}(N)$ if
$\mathcalx{F}(C)\in\mathit{GFRed}_{\mathrm{C}}(\mathcalx{F}(N))$.

  * –

Given $C\in\mathcalx{C}_{\mathrm{H}}$ and
$N\subseteq\mathcalx{C}_{\mathrm{H}}$, let
$C\in{\mathit{HRed}_{\mathrm{C}}}(N)$ if for every $D\in\mathcalx{G}(C)$, we
have $D\in\mathit{GHRed}_{\mathrm{C}}(\mathcalx{G}(N))$ or there exists
$C^{\prime}\in N$ such that $C\sqsupset C^{\prime}$ and
$D\in\mathcalx{G}(C^{\prime})$.

Along with the three levels of logics, we consider three inference systems:
$\mathit{HInf}$, $\mathit{GHInf}$ and $\mathit{GFInf}$. $\mathit{HInf}$ is one
of the four variants of the inference system described in

##  15\.

12.1. For uniformity, we regard axiom (Ext) as a premise-free inference rule
Ext whose conclusion is (Ext). In the purifying calculi, the conclusion of Ext
must be purified. $\mathit{GHInf}$ consists of all Sup, ERes, and EFact
inferences from $\mathit{HInf}$ whose premises and conclusion are ground, a
premise-free rule GExt whose infinitely many conclusions are the ground
instances of (Ext), and the following ground variant of ArgCong:

$\prftree[r]{\small{\textsc{GArgCong}}}{C^{\prime}\mathrel{\lor}s\approx
s^{\prime}}{C^{\prime}\mathrel{\lor}s\>\bar{u}_{n}\approx
s^{\prime}\>\bar{u}_{n}}$

where $s\approx s^{\prime}$ is strictly eligible in the premise and
$\bar{u}_{n}$ is a nonempty tuple of ground terms. $\mathit{GFInf}$ contains
all Sup, ERes, and EFact inferences from $\mathit{GHInf}$ translated by
$\mathcalx{F}$. It coincides exactly with standard first-order superposition.
Given a Sup, ERes, or EFact inference $\iota\in\mathit{GHInf}$, let
$\mathcalx{F}(\iota)$ denote the corresponding inference in $\mathit{GFInf}$.

Each of the three inference systems is parameterized by a selection function.
For $\mathit{HInf}$, we globally fix a selection function $\mathit{HSel}$. For
$\mathit{GHInf}$ and $\mathit{GFInf}$, we need to consider different selection
functions $\mathit{GHSel}$ and $\mathit{GFSel}$. We write
$\mathit{GHInf}^{\mathit{GHSel}}$ for $\mathit{GHInf}$ and
$\mathit{GFInf}^{\mathit{GFSel}}$ for $\mathit{GFInf}$ to make the dependency
on the respective selection functions explicit. Let
$\mathcalx{G}(\mathit{HSel})$ denote the set of all selection functions on
$\mathcalx{C}_{\mathrm{GH}}$ such that for each clause in
$C\in\mathcalx{C}_{\mathrm{GH}}$, there exists a clause
$D\in\mathcalx{C}_{\mathrm{H}}$ with $C\in\mathcalx{G}(D)$ and corresponding
selected literals. For each selection function $\mathit{GHSel}$ on
$\mathcalx{C}_{\mathrm{GH}}$, via the bijection $\mathcalx{F}$, we obtain a
corresponding selection function on $\mathcalx{C}_{\mathrm{GF}}$, which we
denote by $\mathcalx{F}(\mathit{GHSel})$.

######  Notation .

Given an inference $\iota$, we write $\mathit{prems}(\iota)$ for the tuple of
premises, $\mathit{mprem}(\iota)$ for the main (i.e., rightmost) premise,
$\mathit{preconcl}(\iota)$ for the conclusion before purification, and
$\mathit{concl}(\iota)$ for the conclusion after purification. For the
nonpurifying calculi, $\mathit{preconcl}(\iota)=\mathit{concl}(\iota)$ simply
denotes the conclusion.

######  Definition  (Encoding $\mathcalx{F}$ on inferences).

Given a Sup, ERes, or EFact inference $\iota\in\mathit{GHInf}$, let
$\mathcalx{F}(\iota)\in\mathit{GFInf}$ denote the inference defined by
$\mathit{prems}(\mathcalx{F}(\iota))=\mathcalx{F}(\mathit{prems}(\iota))$ and
$\mathit{concl}(\mathcalx{F}(\iota))=\mathcalx{F}(\mathit{concl}(\iota))$.

######  Definition  (Grounding function $\mathcalx{G}$ on inferences).

Given a selection function $\mathit{GHSel}\in\mathcalx{G}(\mathit{HSel})$, and
a non-PosExt inference $\iota\in\mathit{HInf}$, we define the set
$\mathcalx{G}^{\mathit{GHSel}}(\iota)$ of ground instances of $\iota$ to be
all inferences $\iota^{\prime}\in\mathit{GHInf}^{\mathit{GHSel}}$ such that
$\mathit{prems}(\iota^{\prime})=\mathit{prems}(\iota)\theta$ and
$\mathit{concl}(\iota^{\prime})=\mathit{preconcl}(\iota)\theta$ for some
grounding substitution $\theta$. For PosExt inferences $\iota$, which cannot
be grounded, we let $\mathcalx{G}^{\mathit{GHSel}}(\iota)=\mathit{undef}$.

This will map Sup to Sup, EFact to EFact, ERes to ERes, Ext to GExt, and
ArgCong to GArgCong inferences, but it is also possible that
$\mathcalx{G}^{\mathit{GHSel}}(\iota)$ is the empty set for some inferences
$\iota$.

We define the sets of redundant inferences w.r.t. a given clause set as
follows:

  * –

Given $\iota\in\mathit{GFInf}^{\mathit{GFSel}}$ and
$N\subseteq\mathcalx{C}_{\mathrm{GF}}$, let
$\iota\in\mathit{GFRed}_{\mathrm{I}}^{\mathit{GFSel}}(N)$ if
$\mathit{prems}(\iota)\mathrel{\cap}\mathit{GFRed}_{\mathrm{C}}(N)\not=\varnothing$
or $\\{D\in N\mid D\prec\mathit{mprem}(\iota)\\}\models\mathit{concl}(\iota)$.

  * –

Given $\iota\in\mathit{GHInf}^{\mathit{GHSel}}$ and
$N\subseteq\mathcalx{C}_{\mathrm{GH}}$, let
$\iota\in\mathit{GHRed}_{\mathrm{I}}^{\mathit{GHSel}}(N)$ if

    * –

$\iota$ is not a GArgCong or GExt inference and
$\mathcalx{F}(\iota)\in\smash{\mathit{GFRed}_{\mathrm{I}}^{\mathcalx{F}(\mathit{GHSel})}}(\mathcalx{F}(N))$;
or

    * –

the calculus is nonpurifying and $\iota$ is a GArgCong or GExt inference and
$\mathit{concl}(\iota)\in N\mathrel{\cup}\mathit{GHRed}_{\mathrm{C}}(N)$; or

    * –

the calculus is purifying and $\iota$ is a GArgCong or GExt inference and
$\mathcalx{F}(N)\models\mathcalx{F}(\mathit{concl}(\iota))$.

  * –

Given $\iota\in\mathit{HInf}$ and $N\subseteq\mathcalx{C}_{\mathrm{H}}$, let
$\iota\in\mathit{HRed}_{\mathrm{I}}(N)$ if

    * –

$\iota$ is not a PosExt inference and
$\mathcalx{G}^{\mathit{GHSel}}(\iota)\subseteq\mathit{GHRed}_{\mathrm{I}}(\mathcalx{G}(N))$
for all $\mathit{GHSel}\in\mathcalx{G}(\mathit{HSel})$; or

    * –

$\iota$ is a PosExt inference and
$\mathcalx{G}(\mathit{concl}(\iota))\subseteq\mathcalx{G}(N)\mathrel{\cup}\mathit{GHRed}_{\mathrm{C}}(\mathcalx{G}(N))$.

Occasionally, we omit the selection function in the notation when it is
irrelevant. A clause set $N$ is _saturated_ w.r.t. an inference system and a
redundancy criterion $(\mathit{Red}_{\mathrm{I}},\mathit{Red}_{\mathrm{C}})$
if every inference from clauses in $N$ is in $\mathit{Red}_{\mathrm{I}}(N).$

###  15.1. Simplification Rules

The redundancy criterion
$(\mathit{HRed}_{\mathrm{I}},{\mathit{HRed}_{\mathrm{C}}})$ is strong enough
to support most of the simplification rules implemented in Schulz’s first-
order prover E [Sch02, Sections 2.3.1 and 2.3.2], some only with minor
adaptions. Deletion of duplicated literals, deletion of resolved literals,
syntactic tautology deletion, negative simplify-reflect, and clause
subsumption adhere to our redundancy criterion.

Positive simplify-reflect and equality subsumption are supported by our
criterion if they are applied in green contexts. Semantic tautology deletion
can be applied as well, but we must use the entailment relation of the GF
level—i.e., only rewriting in green contexts can be used to establish the
entailment. Similarly, rewriting of positive and negative literals
(demodulation) can only be applied in green contexts. Moreover, for positive
literals, the rewriting clause must be smaller than the rewritten clause—a
condition that is also necessary with the standard first-order redundancy
criterion but not always fulfilled by Schulz’s rule. As for destructive
equality resolution, even in first-order logic the rule cannot be justified
with the standard redundancy criterion, and it is unclear whether it preserves
refutational completeness.

##  16\. Refutational Completeness

Besides soundness, the most important property of the four calculi introduced
in

##  17\.

12.1 is refutational completeness. We will prove the static and dynamic
refutational completeness of $\mathit{HInf}$ w.r.t.
$(\mathit{HRed}_{\mathrm{I}},{\mathit{HRed}_{\mathrm{C}}})$, which is defined
as follows:

######  Definition  (Static refutational completeness).

Let $\mathit{Inf}$ be an inference system and let
$(\mathit{Red}_{\mathrm{I}},\mathit{Red}_{\mathrm{C}})$ be a redundancy
criterion. The inference system $\mathit{Inf}$ is called _statically
refutationally complete_ w.r.t.
$(\mathit{Red}_{\mathrm{I}},\mathit{Red}_{\mathrm{C}})$ if we have
$N\models\bot$ if and only if $\bot\in N$ for every clause set $N$ that is
saturated w.r.t. $\mathit{Inf}$ and $\mathit{Red}_{\mathrm{I}}$.

######  Definition  (Dynamic refutational completeness).

Let $\mathit{Inf}$ be an inference system and let
$(\mathit{Red}_{\mathrm{I}},\mathit{Red}_{\mathrm{C}})$ be a redundancy
criterion. Let $(N_{i})_{i}$ be a finite or infinite sequence over sets of
clauses. Such a sequence is called a _derivation_ if $N_{i}\setminus
N_{i+1}\subseteq\mathit{Red}_{\mathrm{C}}(N_{i+1})$ for all $i$. It is called
_fair_ if all $\mathit{Inf}$-inferences from clauses in the limit inferior
$\bigcup_{i}\bigcap_{\\!j\geq i}N_{\\!j}$ are contained in
$\bigcup_{i}\mathit{Red}_{\mathrm{I}}(N_{i})$. The inference system
$\mathit{Inf}$ is called _dynamically refutationally complete_ w.r.t.
$(\mathit{Red}_{\mathrm{C}},\mathit{Red}_{\mathrm{I}})$ if for every fair
derivation $(N_{i})_{i}$ such that $N_{0}\models\bot$, we have $\bot\in N_{i}$
for some $i$.

To circumvent the term order’s potential nonmonotonicity, our Sup inference
rule only considers green subterms. This is reflected in our proof by the
reliance on the ${\mathrm{GF}}$ level introduced in

##  18\.

14.1. The equation
${\mathsf{g}}_{0}\approx{\mathsf{f}}_{0}\in\mathcalx{C}_{\mathrm{GF}}$, which
corresponds to the equation
${\mathsf{g}}\approx{\mathsf{f}}\in\mathcalx{C}_{\mathrm{GH}}$, cannot be used
directly to rewrite the clause
${\mathsf{g}}_{1}({\mathsf{a}}_{0})\not\approx{\mathsf{f}}_{1}({\mathsf{a}}_{0})\in\mathcalx{C}_{\mathrm{GF}}$,
which corresponds to
${\mathsf{g}}\;{\mathsf{a}}\not\approx{\mathsf{f}}\;{\mathsf{a}}\in\mathcalx{C}_{\mathrm{GH}}$.
Instead, we first need to apply ArgCong to derive
${\mathsf{g}}\>x\approx{\mathsf{f}}\>x$, which after grounding and transfer to
${\mathrm{GF}}$ yields
${\mathsf{g}}_{1}({\mathsf{a}}_{0})\approx{\mathsf{f}}_{1}({\mathsf{a}}_{0})$.
The ${\mathrm{GF}}$ level is a device that enables us to reuse the
refutational completeness result for standard (first-order) superposition.

The proof proceeds in three steps, corresponding to the three levels
${\mathrm{GF}}$, ${\mathrm{GH}}$, and ${\mathrm{H}}$ introduced in

##  19\.

14.1:

  1. (1)

We use Bachmair and Ganzinger’s work on the refutational completeness of
standard superposition [BG94] to prove the static refutational completeness of
$\mathit{GFInf}$.

  2. (2)

From the first-order model constructed in Bachmair and Ganzinger’s proof, we
derive a $\lambda$-free higher-order model to prove the static refutational
completeness of $\mathit{GHInf}$.

  3. (3)

We use the saturation framework of Waldmann et al. [WTRB20] to lift the static
refutational completeness of $\mathit{GHInf}$ to static and dynamic
refutational completeness of $\mathit{HInf}$.

In the first step, since the inference system $\mathit{GFInf}$ is standard
ground superposition, we only need to work around minor differences between
Bachmair and Ganzinger’s definitions and ours. Given a saturated clause set
$N\subseteq\mathcalx{C}_{\mathrm{GF}}$ with $\bot\not\in N$, Bachmair and
Ganzinger prove refutational completeness by constructing a term rewriting
system $R_{N}$ and showing that it can be viewed as an interpretation that is
a model of $N$. This step is exclusively concerned with ground first-order
clauses.

In the second step, we derive refutational completeness of $\mathit{GHInf}$.
Given a saturated clause set $N\subseteq\mathcalx{C}_{\mathrm{GH}}$ with
$\bot\not\in N$, we use the first-order model $R_{\mathcalx{F}(N)}$ of
$\mathcalx{F}(N)$ constructed in step (1) to derive a clausal higher-order
interpretation that is a model of $N$. Thanks to saturation w.r.t. GArgCong,
the higher-order interpretation can conflate the interpretations of the
members
${\mathsf{f}}_{0}^{\bar{\upsilon}},\dots,{\mathsf{f}}_{n}^{\bar{\upsilon}}$ of
a same symbol family. In the extensional calculi, saturation w.r.t. GExt can
be used to show that the constructed interpretation is extensional.

In the third step, we employ the saturation framework by Waldmann et al.
[WTRB20], which is largely based on Bachmair and Ganzinger’s [BG01], to prove
$\mathit{HInf}$ refutationally complete. Like Bachmair and Ganzinger’s, the
saturation framework allows us to prove the static and dynamic refutational
completeness of our calculus on the nonground level. On top of that, it allows
us to use the redundancy criterion defined in Section 14.1, which supports
deletion of subsumed formulas. Moreover, the saturation framework provides
completeness theorems for prover architectures, such as the DISCOUNT loop. The
main proof obligation the saturation framework leaves to us is that there
exist inferences in $\mathit{HInf}$ corresponding to all nonredundant
inferences in $\mathit{GHInf}$. For monotone term orders, we can avoid Sup
inferences into variables $x$ by exploiting the clause order’s compatibility
with contexts: If $t^{\prime}\prec t$, we have $C\\{x\mapsto\nobreak
t^{\prime}\\}\prec C\\{x\mapsto t\\}$, which allows us to show that Sup
inferences into variables are redundant. This technique fails for variables
$x$ that occur applied in $C$, because the order lacks compatibility with
arguments. This is why the calculi must either purify clauses to make this
line of reasoning work again or perform some Sup inferences into variables.

###  19.1. The Ground First-Order Level

We use Bachmair and Ganzinger’s results on standard superposition [BG94] to
prove ${\mathrm{GF}}$ refutationally complete. In the subsequent steps, we
will also make use of specific properties of Bachmair and Ganzinger’s model.

Bachmair and Ganzinger’s logic and inference system differ in some details
from ${\mathrm{GF}}$:

  * –

Bachmair and Ganzinger use untyped first-order logic, whereas
${\mathrm{GF}}$’s logic is typed. Bachmair and Ganzinger’s proof works
verbatim for monomorphic first-order logic as well, but we need to require
that the order $\succ$ has the subterm property to show that there exist no
critical pairs in the term rewriting system, as observed by Wand [Wan17,
Section 3.2.1].

  * –

In their redundancy criterion for clauses, Bachmair and Ganzinger require that
a finite subset of $\\{D\in N\mid D\prec C\\}$ entails $C$, whereas we require
that $\\{D\in N\mid D\prec C\\}$ entails $C$. By compactness of first-order
logic, the two criteria are equivalent.

Bachmair and Ganzinger prove refutational completeness for nonground clause
sets, but we only require the ground result here.

The basis of Bachmair and Ganzinger’s proof is that a term rewriting system
$R$ defines an interpretation $\mathcalx{T}_{\mathrm{GF}}/R$ such that for
every ground equation $s\approx t$, we have
$\mathcalx{T}_{\mathrm{GF}}/R\models s\approx t$ if and only if
$s\mathrel{\leftarrow\kern-7.25482pt\rightarrow}_{R}^{*}t$. Formally,
$\mathcalx{T}_{\mathrm{GF}}/R$ denotes the monomorphic first-order
interpretation whose universes $U_{\tau}$ consist of the $R$-equivalence
classes over $\mathcalx{T}_{\mathrm{GF}}$ containing terms of type $\tau$. The
interpretation $\mathcalx{T}_{\mathrm{GF}}/R$ is term-generated—that is, for
every element $a$ of the universe of this interpretation and for any valuation
$\xi$, there exists a ground term $t$ such that $\smash{\llbracket
t\rrbracket_{\mathcalx{T}_{\mathrm{GF}}/R}^{\smash{\xi}}}=a$. To lighten
notation, we will write $R$ to refer to both the term rewriting system $R$ and
the interpretation $\mathcalx{T}_{\mathrm{GF}}/R$.

The term rewriting system is constructed as follows. Let
$N\subseteq\mathcalx{C}_{\mathrm{GF}}$. We first define sets of rewrite rules
$E_{N}^{C}$ and $R_{N}^{C}$ for all $C\in N$ by induction on the clause order.
Assume that $E_{N}^{D}$ has already been defined for all $D\in N$ such that
$D\prec C.$ Then $R_{N}^{C}=\bigcup_{D\prec C}E_{N}^{D}.$ Let
$E_{N}^{C}=\\{s\mathrel{{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color<EMAIL_ADDRESS>to0.0pt{\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}$\blacksquare$\hss}\kern-3.87495pt}\joinrel{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rightarrow}}t\\}$
if the following conditions are met:

  1. (1)

$C=C^{\prime}\lor s\approx t$;

  2. (2)

$s\approx t$ is strictly maximal in $C$;

  3. (3)

$s\succ t$;

  4. (4)

$C^{\prime}$ is false in $R_{N}^{C}$;

  5. (5)

$s$ is irreducible w.r.t. $R_{N}^{C}.$

Then $C$ is said to _produce_
$s\mathrel{{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color<EMAIL_ADDRESS>to0.0pt{\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}$\blacksquare$\hss}\kern-3.87495pt}\joinrel{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rightarrow}}t$.
Otherwise, $E_{N}^{C}=\emptyset$. Finally, $R_{N}=\bigcup_{D}E_{N}^{D}.$

We call an inference $\iota\in\mathit{GFInf}$ _B &G-redundant_ if some
$C\in\mathit{prems}(\iota)$ is true in $R_{N}^{C}$ or $\mathit{concl}(\iota)$
is true in $\smash{R_{N}^{\mathit{mprem}(\iota)}}$. We call a set
$N\subseteq\mathcalx{C}_{\mathrm{GF}}$ _B &G-saturated_ if all inferences from
$N$ are B&G-redundant.

######  Lemma .

If $\bot\not\in N$ and $N\subseteq\mathcalx{C}_{\mathrm{GF}}$ is saturated
w.r.t. $\mathit{GFInf}$ and $\mathit{GFRed}_{\mathrm{I}}$, then $N$ is
B&G-saturated.

###### Proof.

Let $N\subseteq\mathcalx{C}_{\mathrm{GF}}$ be saturated w.r.t.
$\mathit{GFInf}$ and $\mathit{GFRed}_{\mathrm{I}}$. To show that $N$ is
B&G-saturated, let $\iota$ be an inference from $N$. We need to show that
$\iota$ is B&G-redundant w.r.t. $N$. We proceed by well-founded induction on
$\mathit{mprem}(\iota)$ w.r.t. $\succ$. By the induction hypothesis, for all
inferences $\iota^{\prime}$ with
$\mathit{concl}(\iota^{\prime})\prec\mathit{mprem}(\iota)$, $\iota^{\prime}$
is B&G-redundant w.r.t. $N$. By Lemma 5.5 of Bachmair and Ganzinger, $\iota$
is B&G-redundant w.r.t. $N$. ∎

######  Lemma .

Let $\bot\not\in N$ and $N\subseteq\mathcalx{C}_{\mathrm{GF}}$ be saturated
w.r.t. $\mathit{GFInf}$ and $\mathit{GFRed}_{\mathrm{I}}$. If
$C=C^{\prime}\lor s\approx t\in N$ produces
$s\mathrel{{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color<EMAIL_ADDRESS>to0.0pt{\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}$\blacksquare$\hss}\kern-3.87495pt}\joinrel{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rightarrow}}t$,
then $s\approx t$ is strictly eligible in $C$ and $C^{\prime}$ is false in
$R_{N}$.

###### Proof.

By Lemma 19.1, $N$ is also B&G-saturated. By condition 4, $C^{\prime}$ is
false in $R_{N}^{C}$. Since $s\succ t$ by condition 3 and $s$ is irreducible
w.r.t. $R_{N}^{C}$ by condition 5, $s\approx t$ is also false in $R_{N}^{C}$.
Hence, $C$ is false in $R_{N}^{C}$. Using this and conditions 1, 2, 3, and 5,
we can apply Lemma 4.11 of Bachmair and Ganzinger using $N$ for $N$ and for
$N^{\prime}$, $C$ for $C$ and for $D$, $s$ for $s$, and $t$ for $t$. Part (ii)
of that lemma shows that $s\approx t$ is strictly eligible in $C$, and part
(iv) shows that $C^{\prime}$ is false in $R_{N}$. ∎

######  Theorem  (Ground first-order static refutational completeness).

The inference system $\mathit{GFInf}$ is statically refutationally complete
w.r.t. $(\mathit{GFRed}_{\mathrm{I}},\mathit{GFRed}_{\mathrm{C}})$. More
precisely, if $N\subseteq\mathcalx{C}_{\mathrm{GF}}$ is a clause set saturated
w.r.t. $\mathit{GFInf}$ and $\mathit{GFRed}_{\mathrm{I}}$ such that
$\bot\not\in N$, then $R_{N}$ is a model of $N$.

###### Proof.

By Lemma 19.1, $N$ is also B&G-saturated. It follows that $R_{N}$ is a model
of $N$, as shown in the proof of Theorem 4.14 of Bachmair and Ganzinger. ∎

###  19.2. The Ground Higher-Order Level

In this subsection, let $\mathit{GHSel}$ be a selection function on
$\mathcalx{C}_{\mathrm{GH}}$, and let $N\subseteq\mathcalx{C}_{\mathrm{GH}}$
with $\bot\not\in N$ be a clause set saturated w.r.t.
$\mathit{GHInf}^{\mathit{GHSel}}$ and
$\mathit{GHRed}_{\mathrm{I}}^{\mathit{GHSel}}$. Clearly, $\mathcalx{F}(N)$ is
then saturated w.r.t. $\smash{\mathit{GFInf}^{\mathcalx{F}(\mathit{GHSel})}}$
and $\smash{\mathit{GFRed}_{\mathrm{I}}^{\mathcalx{F}(\mathit{GHSel})}}$.

We abbreviate $R_{\mathcalx{F}(N)}$ as $R$. From $R$, we construct a model
$\mathcal{I}^{\smash{{\mathrm{GH}}}}$ of $N$. The key properties enabling us
to perform this construction are that $R$ is term-generated and that the
interpretations of the members
${\mathsf{f}}_{0}^{\bar{\upsilon}},\dots,{\mathsf{f}}_{n}^{\bar{\upsilon}}$ of
a same symbol family behave in the same way thanks to the ArgCong rule.

######  Lemma  (Argument congruence).

For terms $s,t,u\in\mathcalx{T}_{\mathrm{GH}}$, if
$\smash{\llbracket\mathcalx{F}(s)\rrbracket_{R}^{\smash{}}}\allowbreak=\smash{\llbracket\mathcalx{F}(t)\rrbracket_{R}^{\smash{}}}$,
then
$\smash{\llbracket\mathcalx{F}(s\>u)\rrbracket_{R}^{\smash{}}}=\smash{\llbracket\mathcalx{F}(t\>u)\rrbracket_{R}^{\smash{}}}$.

###### Proof.

What we want to show is equivalent to

$\mathcalx{F}(s)\mathrel{\leftarrow\kern-7.25482pt\rightarrow}_{R}^{*}\mathcalx{F}(t)\text{
\,implies\,
}\mathcalx{F}(s\>u)\mathrel{\leftarrow\kern-7.25482pt\rightarrow}_{R}^{*}\mathcalx{F}(t\>u)$

By induction on the number of rewrite steps and due to symmetry, it suffices
to show that

$\mathcalx{F}(s)\mathrel{{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color<EMAIL_ADDRESS>to0.0pt{\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}$\blacksquare$\hss}\kern-3.87495pt}\joinrel{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rightarrow}}_{R}\mathcalx{F}(t)\text{
\,implies\,
}\mathcalx{F}(s\>u)\mathrel{\leftarrow\kern-7.25482pt\rightarrow}_{R}^{*}\mathcalx{F}(t\>u)$

If the rewrite step from $\mathcalx{F}(s)$ is below the top level, this is
obvious because there is a corresponding rewrite step from
$\mathcalx{F}(s\>u)$. If it is at the top level,
$\mathcalx{F}(s)\mathrel{{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color<EMAIL_ADDRESS>to0.0pt{\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@color@gray@fill{1}$\blacksquare$\hss}\kern-3.87495pt}\joinrel{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\rightarrow}}\mathcalx{F}(t)$
must be rule of $R$. This rule must originate from a productive clause of the
form $\mathcalx{F}(C)=\mathcalx{F}(C^{\prime}\mathrel{\lor}s\approx t)$. By
Lemma 19.1, $\mathcalx{F}(s\approx t)$ is strictly eligible in
$\mathcalx{F}(C)$ w.r.t. $\mathcalx{F}(\mathit{GHSel})$, and hence $s\approx
t$ is strictly eligible in $C$ w.r.t. $\mathit{GHSel}$. Moreover, $s$ and $t$
have functional type. Thus, the following GArgCong inference $\iota$ is
applicable:

$\prftree[r]{\small{\textsc{GArgCong}}}{C^{\prime}\mathrel{\lor}s\approx
t}{C^{\prime}\mathrel{\lor}s\>u\approx t\>u}$

By saturation, $\iota$ is redundant w.r.t. $N$—i.e., we have
$\mathit{concl}(\iota)\in N\mathrel{\cup}\mathit{GHRed}_{\mathrm{C}}(N)$ (for
the nonpurifying calculi) or $\mathcalx{F}(N)\models\mathit{concl}(\iota)$
(for the purifying calculi). In both cases, by Theorem 19.1,
$\mathcalx{F}(\mathit{concl}(\iota))$ is then true in $R$. By Lemma 19.1,
$\mathcalx{F}(C^{\prime})$ is false in $R$. Therefore,
$\mathcalx{F}(s\>u\approx t\>u)$ must be true in $R$. ∎

######  Lemma .

For terms $s,t,u,v\in\mathcalx{T}_{\mathrm{GH}}$, if
$\smash{\llbracket\mathcalx{F}(s)\rrbracket_{R}^{\smash{}}}\allowbreak=\smash{\llbracket\mathcalx{F}(t)\rrbracket_{R}^{\smash{}}}$
and
$\smash{\llbracket\mathcalx{F}(u)\rrbracket_{R}^{\smash{}}}\allowbreak=\smash{\llbracket\mathcalx{F}(v)\rrbracket_{R}^{\smash{}}}$,
then
$\smash{\llbracket\mathcalx{F}(s\>u)\rrbracket_{R}^{\smash{}}}=\smash{\llbracket\mathcalx{F}(t\>v)\rrbracket_{R}^{\smash{}}}$.

###### Proof.

By Lemma 19.2, we have
$\smash{\llbracket\mathcalx{F}(s\>u)\rrbracket_{R}^{\smash{}}}=\smash{\llbracket\mathcalx{F}(t\>u)\rrbracket_{R}^{\smash{}}}$.
It remains to show that
$\smash{\llbracket\mathcalx{F}(t\>u)\rrbracket_{R}^{\smash{}}}=\smash{\llbracket\mathcalx{F}(t\>v)\rrbracket_{R}^{\smash{}}}$.
Since $t$ is ground, it must be of the form
${\mathsf{f}}{\langle\bar{\upsilon}_{m}\rangle}\>\bar{t}_{n}$. The
interpretation $R$ defined above is an interpretation $(U,\mathcalx{J})$ in
monomorphic first-order logic. Then

$\smash{\llbracket\mathcalx{F}(t\>u)\rrbracket_{R}^{\smash{}}}=\mathcalx{J}({\mathsf{f}}_{n+1}^{\bar{\upsilon}_{m}})(\smash{\llbracket\mathcalx{F}(\bar{t}_{n})\rrbracket_{R}^{\smash{}}},\smash{\llbracket\mathcalx{F}(u)\rrbracket_{R}^{\smash{}}})=\mathcalx{J}({\mathsf{f}}_{n+1}^{\bar{\upsilon}_{m}})(\smash{\llbracket\mathcalx{F}(\bar{t}_{n})\rrbracket_{R}^{\smash{}}},\smash{\llbracket\mathcalx{F}(v)\rrbracket_{R}^{\smash{}}})=\smash{\llbracket\mathcalx{F}(t\>v)\rrbracket_{R}^{\smash{}}}$

######  Definition .

Define a higher-order interpretation
$\mathcal{I}^{\smash{{\mathrm{GH}}}}=(\mathcalx{U}^{\smash{{\mathrm{GH}}}},\mathcalx{J}_{\mathsf{ty}}^{\mathrm{GH}},\mathcalx{J}^{\smash{{\mathrm{GH}}}},\mathcalx{E}^{\smash{{\mathrm{GH}}}})$
as follows. The interpretation $R$ defined above is an interpretation
$(U,\mathcalx{J})$ in monomorphic first-order logic, where $U_{\tau}$ is its
universe for type $\tau$, and $\mathcalx{J}$ is its interpretation function.
Let $\mathcalx{U}^{\smash{{\mathrm{GH}}}}=\\{U_{\tau}\mid\tau\text{ is a
ground type}\\}$. Let
$\mathcalx{J}_{\mathsf{ty}}^{\mathrm{GH}}(\kappa)(U_{\bar{\tau}})=U_{\kappa(\bar{\tau})}$
for all type constructors $\kappa$ and type tuples $\bar{\tau}$. Let
$\mathcalx{J}^{\smash{{\mathrm{GH}}}}({\mathsf{f}},U_{\bar{\tau}})=\mathcalx{J}({\mathsf{f}}_{0}^{\bar{\tau}})$.

Since $R$ is term-generated, for every $a\in U_{{\tau\rightarrow\upsilon}}$
and $b\in U_{\tau}$, there exist ground terms $s:\tau\rightarrow\upsilon$ and
$u:\tau$ such that
$\smash{\llbracket\mathcalx{F}(s)\rrbracket_{R}^{\smash{}}}=a$ and
$\smash{\llbracket\mathcalx{F}(u)\rrbracket_{R}^{\smash{}}}=b$. We define
$\mathcalx{E}^{\smash{{\mathrm{GH}}}}$ by
$\smash{\mathcalx{E}^{\smash{{\mathrm{GH}}}}_{U_{\tau},U_{\upsilon}}(a)(b)=\smash{\llbracket\mathcalx{F}(s\>u)\rrbracket_{R}^{\smash{}}}}\kern-0.83328pt$
for any term $u$. By Lemma 19.2, this definition is independent of the choice
of $s$ and $u$.

######  Lemma  (Model transfer to ${\mathrm{GH}}$).

$\mathcal{I}^{\smash{{\mathrm{GH}}}}$ is a model of $N$. In the extensional
calculi, $\mathcal{I}^{\smash{{\mathrm{GH}}}}$ is an extensional model of $N$.

###### Proof.

We first prove by induction on terms $t\in\mathcalx{T}_{\mathrm{GH}}$ that
$\smash{\llbracket
t\rrbracket_{\mathcal{I}^{\smash{{\mathrm{GH}}}}}^{\smash{}}}=\smash{\llbracket\mathcalx{F}(t)\rrbracket_{R}^{\smash{}}}$.
Let $t\in\mathcalx{T}_{\mathrm{GH}}$, and assume as the induction hypothesis
that $\smash{\llbracket
u\rrbracket_{\mathcal{I}^{\smash{{\mathrm{GH}}}}}^{\smash{}}}=\smash{\llbracket\mathcalx{F}(u)\rrbracket_{R}^{\smash{}}}$
for all subterms $u$ of $t$. If $t$ is of the form
${\mathsf{f}}{\langle\bar{\upsilon}\rangle}$, then

$\displaystyle\smash{\llbracket
t\rrbracket_{\mathcal{I}^{\smash{{\mathrm{GH}}}}}^{\smash{}}}$
$\displaystyle=\mathcalx{J}^{\smash{{\mathrm{GH}}}}({\mathsf{f}},U_{\bar{\upsilon}})=\mathcalx{J}({\mathsf{f}}_{0}^{\bar{\upsilon}})=\smash{\llbracket{\mathsf{f}}_{0}^{\bar{\upsilon}}\rrbracket_{R}^{\smash{}}}=\smash{\llbracket\mathcalx{F}({\mathsf{f}}{\langle\bar{\upsilon}\rangle})\rrbracket_{R}^{\smash{}}}=\smash{\llbracket\mathcalx{F}(t)\rrbracket_{R}^{\smash{}}}$

If $t$ is an application $t=t_{1}\;t_{2}$, where $t_{1}$ is of type
$\tau\rightarrow\upsilon$, then, using the definition of the term denotation
and of $\mathcalx{E}^{\smash{{\mathrm{GH}}}}$, we have

$\displaystyle\smash{\llbracket
t_{1}\;t_{2}\rrbracket_{\mathcal{I}^{\smash{{\mathrm{GH}}}}}^{\smash{}}}=\mathcalx{E}^{\smash{{\mathrm{GH}}}}_{U_{\tau},U_{\upsilon}}(\smash{\llbracket
t_{1}\rrbracket_{\mathcal{I}^{\smash{{\mathrm{GH}}}}}^{\smash{}}})(\smash{\llbracket
t_{2}\rrbracket_{\mathcal{I}^{\smash{{\mathrm{GH}}}}}^{\smash{}}})\overset{\\!\text{IH}\\!}{=}\mathcalx{E}^{\smash{{\mathrm{GH}}}}_{U_{\tau},U_{\upsilon}}(\smash{\llbracket\mathcalx{F}(t_{1})\rrbracket_{R}^{\smash{}}})(\smash{\llbracket\mathcalx{F}(t_{2})\rrbracket_{R}^{\smash{}}})=\smash{\llbracket\mathcalx{F}(t_{1}\;t_{2})\rrbracket_{R}^{\smash{}}}$

So we have shown that $\smash{\llbracket
t\rrbracket_{\mathcal{I}^{\smash{{\mathrm{GH}}}}}^{\smash{}}}=\smash{\llbracket\mathcalx{F}(t)\rrbracket_{R}^{\smash{}}}$
for all terms $t$. It follows that a ground equation $s\approx t$ is true in
$\mathcal{I}^{\smash{{\mathrm{GH}}}}$ if and only if $\mathcalx{F}(s\approx
t)$ is true in $R$. Hence a ground clause $C$ is true in
$\mathcal{I}^{\smash{{\mathrm{GH}}}}$ if and only if $\mathcalx{F}(C)$ is true
in $R$. By Theorem 19.1, $R$ is a model of $\mathcalx{F}(N)$. Thus,
$\mathcal{I}^{\smash{{\mathrm{GH}}}}$ is a model of $N$.

For the extensional calculi, it remains to show that
$\mathcal{I}^{\smash{{\mathrm{GH}}}}$ is extensional—i.e., we have to show
that for all $\tau$ and $\upsilon$ and all $a,b\in
U_{\tau\rightarrow\upsilon}$, if $a\not=b$, then
$\mathcalx{E}^{\smash{{\mathrm{GH}}}}(a)\not=\mathcalx{E}^{\smash{{\mathrm{GH}}}}(b)$.
Since $R$ is term-generated, there are terms
$s,t\in\mathcalx{T}_{\mathrm{GF}}$ such that $\smash{\llbracket
s\rrbracket_{R}^{\smash{}}}=a$ and $\smash{\llbracket
t\rrbracket_{R}^{\smash{}}}=b$. By what we have shown above, it follows that
$\smash{\llbracket
s^{\prime}\rrbracket_{\mathcal{I}^{\smash{{\mathrm{GH}}}}}^{\smash{}}}=a$ and
$\smash{\llbracket
t^{\prime}\rrbracket_{\mathcal{I}^{\smash{{\mathrm{GH}}}}}^{\smash{}}}=b$ for
$s^{\prime}=\mathcalx{F}^{-1}(s)$ and $t^{\prime}=\mathcalx{F}^{-1}(t)$.

Since $N$ is saturated, the GExt inference that generates the clause

$C~{}=~{}s^{\prime}\;(\mathsf{diff}{\langle\tau,\upsilon\rangle}\>s^{\prime}\>t^{\prime})\not\approx
t^{\prime}\>(\mathsf{diff}{\langle\tau,\upsilon\rangle}\>s^{\prime}\>t^{\prime})\mathrel{\lor}s^{\prime}\approx
t^{\prime}$

is redundant—i.e., $C\in N\mathrel{\cup}\mathit{GHRed}_{\mathrm{C}}(N)$ (in
the nonpurifying calculi) or $\mathcalx{F}(N)\models\mathcalx{F}(C)$ (in the
purifying calculi). In both cases, it follows that $R\models\mathcalx{F}(C)$
by Theorem 19.1 and thus $\mathcal{I}^{\smash{{\mathrm{GH}}}}\models C$ by
what we have shown above. The second literal of $C$ is false in
$\mathcal{I}^{\smash{{\mathrm{GH}}}}$ because $\smash{\llbracket
s^{\prime}\rrbracket_{\mathcal{I}^{\smash{{\mathrm{GH}}}}}^{\smash{}}}=a\not=b=\smash{\llbracket
t^{\prime}\rrbracket_{\mathcal{I}^{\smash{{\mathrm{GH}}}}}^{\smash{}}}$. So
the first literal of $C$ must be true in $\mathcal{I}^{\smash{{\mathrm{GH}}}}$
and thus

$\displaystyle\mathcalx{E}^{\smash{{\mathrm{GH}}}}(a)(\smash{\llbracket\mathsf{diff}{\langle\tau,\upsilon\rangle}\>s^{\prime}\>t^{\prime}\rrbracket_{\mathcal{I}^{\smash{{\mathrm{GH}}}}}^{\smash{}}})$
$\displaystyle=\smash{\llbracket
s^{\prime}\;(\mathsf{diff}{\langle\tau,\upsilon\rangle}\>s^{\prime}\>t^{\prime})\rrbracket_{\mathcal{I}^{\smash{{\mathrm{GH}}}}}^{\smash{}}}$
$\displaystyle\not=\smash{\llbracket
t^{\prime}\>(\mathsf{diff}{\langle\tau,\upsilon\rangle}\>s^{\prime}\>t^{\prime})\rrbracket_{\mathcal{I}^{\smash{{\mathrm{GH}}}}}^{\smash{}}}=\mathcalx{E}^{\smash{{\mathrm{GH}}}}(b)(\smash{\llbracket\mathsf{diff}{\langle\tau,\upsilon\rangle}\>s^{\prime}\>t^{\prime}\rrbracket_{\mathcal{I}^{\smash{{\mathrm{GH}}}}}^{\smash{}}})$

It follows that
$\mathcalx{E}^{\smash{{\mathrm{GH}}}}(a)\not=\mathcalx{E}^{\smash{{\mathrm{GH}}}}(b)$.
∎

We summarize the results of this subsection in the following theorem:

######  Theorem  (Ground static refutational completeness).

Let $\mathit{GHSel}$ be a selection function on $\mathcalx{C}_{\mathrm{GH}}$.
Then the inference system $\mathit{GHInf}^{\mathit{GHSel}}$ is statically
refutationally complete w.r.t.
$(\mathit{GHRed}_{\mathrm{I}},\mathit{GHRed}_{\mathrm{C}})$. That means, if
$N\subseteq\mathcalx{C}_{\mathrm{GH}}$ is saturated w.r.t.
$\mathit{GHInf}^{\mathit{GHSel}}$ and
$\mathit{GHRed}_{\mathrm{I}}^{\mathit{GHSel}}$, then $N\models\bot$ if and
only if $\bot\in N$.

The construction of $\mathcal{I}^{\smash{{\mathrm{GH}}}}$ relies on the
specific properties of $R$. It would not work with an arbitrary first-order
interpretation. Transforming a $\lambda$-free higher-order interpretation into
a first-order interpretation is easier:

######  Lemma .

Given an interpretation $\mathcal{I}$ on ${\mathrm{GH}}$, there exists an
interpretation $\mathcal{I}^{\mathrm{GF}}$ on ${\mathrm{GF}}$ such that for
any clause $C\in\mathcalx{C}_{\mathrm{GH}}$ the truth values of $C$ in
$\mathcal{I}$ and of $\mathcalx{F}(C)$ in $\mathcal{I}^{\mathrm{GF}}$
coincide.

###### Proof.

Let
$\mathcal{I}=(\mathcalx{U},\mathcalx{J}_{\mathsf{ty}},\mathcalx{J},\mathcalx{E})$
be a $\lambda$-free higher-order interpretation. Let
$\mathcalx{U}^{\mathrm{GF}}_{\tau}=\smash{\llbracket\tau\rrbracket_{\mathcal{I}_{\mathsf{ty}}}^{\smash{}}}$
be the first-order type universe for the ground type $\tau$. For a symbol
$\smash{{\mathsf{f}}_{l}^{\bar{\upsilon}_{m}}}\in\mathrm{\Sigma}_{\mathrm{GF}}$
and universe elements $\bar{a}_{l}$, let
$\mathcalx{J}^{\mathrm{GF}}(\smash{{\mathsf{f}}_{l}^{\bar{\upsilon}_{m}}})(\bar{a}_{l})=\smash{\llbracket{\mathsf{f}}{\langle\bar{\upsilon}_{m}\rangle}\>\bar{x}_{l}\rrbracket_{\mathcal{I}}^{\smash{\\{\bar{x}_{l}\mapsto\bar{a}\\}}}}$.
This defines an interpretation
$\mathcal{I}^{\mathrm{GF}}=(\mathcalx{U}^{\mathrm{GF}},\mathcalx{J}^{\mathrm{GF}})$
on ${\mathrm{GF}}$.

We need to show that for any $C\in\mathcalx{C}_{\mathrm{GH}}$,
$\mathcal{I}\models C$ if and only if
$\mathcal{I}^{\mathrm{GF}}\models\mathcalx{F}(C)$. It suffices to show that
$\smash{\llbracket
t\rrbracket_{\mathcal{I}}^{\smash{}}}=\smash{\llbracket\mathcalx{F}(t)\rrbracket_{\mathcal{I}^{\mathrm{GF}}}^{\smash{}}}$
for all terms $t\in\mathcalx{T}_{\mathrm{GH}}$. We prove this by induction on
$t$. Since $t$ is ground, it must be of the form
${\mathsf{f}}{\langle\bar{\upsilon}_{m}\rangle}\>\bar{s}_{l}$. Then
$\mathcalx{F}(t)=\smash{{\mathsf{f}}_{l}^{\bar{\upsilon}_{m}}(\mathcalx{F}(\bar{s}_{l}))}$
and hence

$\smash{\llbracket\mathcalx{F}(t)\rrbracket_{\mathcal{I}^{\mathrm{GF}}}^{\smash{}}}=\mathcalx{J}^{\mathrm{GF}}(\smash{{\mathsf{f}}_{l}^{\bar{\upsilon}_{m}}})(\smash{\llbracket\mathcalx{F}(\bar{s}_{l})\rrbracket_{\mathcal{I}^{\mathrm{GF}}}^{\smash{}}})\overset{\smash{\text{IH}}}{=}\mathcalx{J}^{\mathrm{GF}}(\smash{{\mathsf{f}}_{l}^{\bar{\upsilon}_{m}}})(\smash{\llbracket\bar{s}_{l}\rrbracket_{\mathcal{I}}^{\smash{}}})=\smash{\llbracket{\mathsf{f}}{\langle\bar{\upsilon}_{m}\rangle}\>\bar{s}_{l}\rrbracket_{\mathcal{I}}^{\smash{}}}=\smash{\llbracket
t\rrbracket_{\mathcal{I}}^{\smash{}}}$

using the definition of $\mathcalx{J}^{\mathrm{GF}}$ and Lemma 12.3 for the
third step. ∎

###  19.3. The Nonground Higher-Order Level

To lift the result to the nonground level, we employ the saturation framework
of Waldmann et al. [WTRB20]. It is easy to see that the entailment relation
$\models$ on ${\mathrm{GH}}$ is a consequence relation in the sense of the
framework. It remains to show that our redundancy criterion on ${\mathrm{GH}}$
is a redundancy criterion in the sense of the framework and that
$\mathcalx{G}$ is a grounding function in the sense of the framework:

######  Lemma .

The redundancy criterion for ${\mathrm{GH}}$ is a redundancy criterion in the
sense of the framework.

###### Proof.

We must prove the conditions (R1) to (R4) defined by Waldmann et al., which,
adapted to our context, state the following for all clause sets
$N,N^{\prime}\subseteq\mathcalx{C}_{\mathrm{GH}}$:

  1. (R1)

if $N\models\bot$, then $N\setminus\mathit{GHRed}_{\mathrm{C}}(N)\models\bot$;

  2. (R2)

if $N\subseteq N^{\prime}$, then
$\mathit{GHRed}_{\mathrm{C}}(N)\subseteq\mathit{GHRed}_{\mathrm{C}}(N^{\prime})$
and
$\mathit{GHRed}_{\mathrm{I}}(N)\subseteq\mathit{GHRed}_{\mathrm{I}}(N^{\prime})$;

  3. (R3)

if $N^{\prime}\subseteq\mathit{GHRed}_{\mathrm{C}}(N)$, then
$\mathit{GHRed}_{\mathrm{C}}(N)\subseteq\mathit{GHRed}_{\mathrm{C}}(N\setminus
N^{\prime})$ and
$\mathit{GHRed}_{\mathrm{I}}(N)\subseteq\mathit{GHRed}_{\mathrm{I}}(N\setminus
N^{\prime})$;

  4. (R4)

if $\iota\in\mathit{GHInf}$ and $\mathit{concl}(\iota)\in N$, then
$\iota\in\mathit{GHRed}_{\mathrm{I}}(N)$.

(R1) It suffices to show that $N\setminus\mathit{GHRed}_{\mathrm{C}}(N)\models
N$ for $N\subseteq\mathcalx{C}_{\mathrm{GH}}$. Let $\mathcal{I}$ be a model of
$N\setminus\mathit{GHRed}_{\mathrm{C}}(N)$. In the extensional calculi, let
$\mathcal{I}$ be extensional. Then by Lemma 19.2, there exists a model
$\mathcal{I}^{\mathrm{GF}}$ of
$\mathcalx{F}(N\setminus\mathit{GHRed}_{\mathrm{C}}(N))=\mathcalx{F}(N)\setminus\mathit{GFRed}_{\mathrm{C}}(\mathcalx{F}(N))$.
By Lemma 5.2 of Bachmair and Ganzinger, this is also a model of
$\mathcalx{F}(N)$. By Lemma 19.2, it follows that $\mathcal{I}\models N$.

(R2) By Lemma 5.6(i) of Bachmair and Ganzinger, this holds on ${\mathrm{GF}}$.
For clauses and all inferences except GArgCong and GExt, this implies that it
holds on ${\mathrm{GH}}$ as well because $\mathcalx{F}$ is a redundancy-
preserving bijection between $\mathcalx{C}_{\mathrm{GH}}$ and
$\mathcalx{C}_{\mathrm{GF}}$ and between these inferences. For GArgCong and
GExt inferences, it holds because it holds on clauses.

(R3) The proof is analogous to (R2), with Lemma 5.6(ii) of Bachmair and
Ganzinger instead of Lemma 5.6(i).

(R4) We must show that for all inferences with $\mathit{concl}(\iota)\in N$,
we have $\iota\in\mathit{GHRed}_{\mathrm{I}}(N)$. Since
$\mathit{concl}(\iota)\prec\mathit{mprem}(\iota)$ for all
$\iota\in\mathit{GFInf}$, this holds on ${\mathrm{GF}}$. For all inferences
except GArgCong and GExt, since $\mathcalx{F}$ is a bijection preserving
redundancy, it follows that it also holds also on ${\mathrm{GH}}$. For
GArgCong and GExt inferences, it holds by definition. ∎

######  Lemma .

The grounding functions $\mathcalx{G}^{\mathit{GHSel}}$ for
$\mathit{GHSel}\in\mathcalx{G}(\mathit{HSel})$ are grounding functions in the
sense of the framework.

###### Proof.

We must prove the conditions (G1) to (G3) defined by Waldmann et al., which,
adapted to our context, state the following:

  1. (G1)

$\mathcalx{G}(\bot)=\\{\bot\\}$;

  2. (G2)

for every $C\in\mathcalx{C}_{\mathrm{GH}}$, if $\bot\in\mathcalx{G}(C)$, then
$C=\bot$;

  3. (G3)

for every $\iota\in\mathit{HInf}$, if
$\mathcalx{G}^{\mathit{GHSel}}(\iota)\not=\mathit{undef}$, then
$\mathcalx{G}^{\mathit{GHSel}}(\iota)\subseteq\mathit{GHRed}_{\mathrm{I}}^{\mathit{GHSel}}(\mathcalx{G}(\mathit{concl}(\iota)))$.

Clearly, $C=\bot$ if and only if $\bot\in\mathcalx{G}(C)$ if and only if
$\mathcalx{G}(C)=\\{\bot\\}$, proving (G1) and (G2). For (G3), we have to show
for all non-PosExt inferences $\iota\in\mathit{HInf}$ that
$\mathcalx{G}^{\mathit{GHSel}}(\iota)\subseteq\mathit{GHRed}_{\mathrm{I}}^{\mathit{GHSel}}(\mathcalx{G}(\mathit{concl}(\iota)))$.
Let $\iota\in\mathit{HInf}$ and
$\iota^{\prime}\in\mathcalx{G}^{\mathit{GHSel}}(\iota)$. By the definition of
$\mathcalx{G}^{\mathit{GHSel}}$, there exists a grounding substitution
$\theta$ such that
$\mathit{prems}(\iota^{\prime})=\mathit{prems}(\iota)\theta$ and
$\mathit{concl}(\iota^{\prime})=\mathit{preconcl}(\iota)\theta$. We want to
show that
$\iota^{\prime}\in\mathit{GHRed}_{\mathrm{I}}^{\mathit{GHSel}}(\mathcalx{G}(\mathit{concl}(\iota)))$.

If $\iota^{\prime}$ is not an GArgCong or GExt inference, by the definition of
inference redundancy, it suffices to show that
$\\{D\in\mathcalx{F}(\mathcalx{G}(\mathit{concl}(\iota)))\mid
D\prec\mathit{mprem}(\mathcalx{F}(\iota^{\prime}))\\}\models\mathit{concl}(\mathcalx{F}(\iota^{\prime}))$.
We define a substitution $\theta^{\prime}$ that extends $\theta$ to all
variables in $\mathit{concl}(\iota)$. Due to purification, the clause
$\mathit{concl}(\iota)$ may contain variables not present in
$\mathit{preconcl}(\iota)$. For each such variable $x^{\prime}$, let $x$ be
the variable in $\mathit{preconcl}(\iota)$ that $x^{\prime}$ stems from and
define $x^{\prime}\theta^{\prime}=x\theta$. Then the clause
$\mathcalx{F}(\mathit{concl}(\iota)\theta^{\prime})$ differs from the clause
$\mathcalx{F}(\mathit{concl}(\iota^{\prime}))=\mathcalx{F}(\mathit{preconcl}(\iota)\theta^{\prime})$
only in some additional grounded purification literals, which all have the
form $t\not\approx t$ and are thus trivially false in any interpretation.
Hence,
$\mathcalx{F}(\mathit{concl}(\iota)\theta^{\prime})\models\mathcalx{F}(\mathit{concl}(\iota^{\prime}))$.
Since one of the variables of a purification literal must appear applied in
the clause, for each grounded purification literal $t\not\approx t$ the term
$t$ must be smaller than the maximal term of the clause
$\mathcalx{F}(\mathit{concl}(\iota^{\prime}))$.

If no literals are selected in $\mathit{mprem}(\mathcalx{F}(\iota^{\prime}))$,
inspection of the rules in $\mathit{GFInf}$ shows that
$\mathcalx{F}(\mathit{concl}(\iota)\theta^{\prime})\prec\mathit{mprem}(\mathcalx{F}(\iota^{\prime}))$.
Otherwise, $\iota^{\prime}$ can only be an ERes inference or a Sup inference
into a negative literal. If it is an ERes inference, due to the selection
restrictions, the substitution $\sigma$ used in $\iota$ is the identity for
all variables of functional type. Therefore, applying $\sigma$ cannot trigger
any purification and hence
$\mathcalx{F}(\mathit{concl}(\iota)\theta^{\prime})=\mathcalx{F}(\mathit{preconcl}(\iota)\theta^{\prime})\prec\mathit{mprem}(\mathcalx{F}(\iota^{\prime}))$.
If $\iota^{\prime}$ is a Sup inference into a negative literal, due to the
selection restrictions, the substitution $\sigma=\operatorname{mgu}(t,u)$ used
in $\iota$ is the identity for all variables of functional type that stem from
the main premise. Therefore the variables from the main premise $C$ need not
be purified. The variables from the side premise $D$ might need to be
purified, yielding purification literals of the form $x\not\approx y$ where
$x\theta^{\prime}=y\theta^{\prime}$. Then $x$ or $y$ must appear applied in
$D$ and hence $x\theta^{\prime}$ is smaller than $t\theta^{\prime}$. Again, it
follows that
$\mathcalx{F}(\mathit{concl}(\iota)\theta^{\prime})\prec\mathit{mprem}(\mathcalx{F}(\iota^{\prime}))$.

This proves $\\{D\in\mathcalx{F}(\mathcalx{G}(\mathit{concl}(\iota)))\mid
D\prec\mathit{mprem}(\mathcalx{F}(\iota^{\prime}))\\}\models\mathit{concl}(\mathcalx{F}(\iota^{\prime}))$.

In the nonpurifying calculi, if $\iota^{\prime}$ is an GArgCong or GExt
inference, it suffices to show that
$\mathit{concl}(\iota^{\prime})\in\mathcalx{G}(\mathit{concl}(\iota))$. This
holds because
$\mathit{concl}(\iota^{\prime})=\mathit{preconcl}(\iota)\theta=\mathit{concl}(\iota)\theta$.
In the purifying calculi, if $\iota^{\prime}$ is an GArgCong or GExt
inference, we must show that
$\mathcalx{F}(\mathcalx{G}(\mathit{concl}(\iota)))\models\mathcalx{F}(\mathit{concl}(\iota^{\prime}))$.
Defining $\theta^{\prime}$ as above, we have
$\mathcalx{F}(\mathit{concl}(\iota)\theta^{\prime})\models\mathcalx{F}(\mathit{concl}(\iota^{\prime}))$,
as desired. ∎

To lift the completeness result of the previous section to the nonground
calculus $\mathit{HInf}$, we employ Theorem 14 of Waldmann et al., which,
adapted to our context, is stated as follows. The theorem uses the notation
$\mathit{Inf}(N)$ to denote the set of $\mathit{Inf}$-inferences whose
premises are in $N$, for an inference system $\mathit{Inf}$ and a clause set
$N$. Moreover, it uses the Herbrand entailment $\models{G}$ on
$\mathcalx{C}_{\mathrm{H}}$, which is defined as $N_{1}\models{G}N_{2}$ if
$\mathcalx{G}(N_{1})\models\mathcalx{G}(N_{2})$.

######  Theorem  (Lifting theorem).

If $\mathit{GHInf}^{\mathit{GHSel}}$ is statically refutationally complete
w.r.t.
$(\mathit{GHRed}_{\mathrm{I}}^{\mathit{GHSel}},\mathit{GHRed}_{\mathrm{C}})$
for every $\mathit{GHSel}\in\mathcalx{G}(\mathit{HSel})$, and if for every
$N\subseteq\mathcalx{C}_{\mathrm{H}}$ that is saturated w.r.t. $\mathit{HInf}$
and $\mathit{HRed}_{\mathrm{I}}$ there exists a
$\mathit{GHSel}\in\mathcalx{G}(\mathit{HSel})$ such that
$\mathit{GHInf}^{\mathit{GHSel}}(\mathcalx{G}(N))\subseteq\mathcalx{G}^{\mathit{GHSel}}(\mathit{HInf}(N))\cup\mathit{GHRed}_{\mathrm{I}}^{\mathit{GHSel}}(\mathcalx{G}(N))$,
then $\mathit{HInf}$ is statically refutationally complete w.r.t.
$(\mathit{HRed}_{\mathrm{I}},{\mathit{HRed}_{\mathrm{C}}})$ and $\models{G}$.

###### Proof.

This is essentially Theorem 14 of Waldmann et al. We take ${\mathrm{H}}$ for
$\mathbf{F}$, ${\mathrm{GH}}$ for $\mathbf{G}$, and
$\mathcalx{G}(\mathit{HSel})$ for $Q$. It is easy to see that the entailment
relation $\models$ on ${\mathrm{GH}}$ is a consequence relation in the sense
of the framework. By Lemma 19.3 and 19.3,
$(\mathit{GHRed}_{\mathrm{I}}^{\mathit{GHSel}},\mathit{GHRed}_{\mathrm{C}})$
is a redundancy criterion in the sense of the framework, and
$\mathcalx{G}^{\mathit{GHSel}}$ are grounding functions in the sense of the
framework, for all $\mathit{GHSel}\in\mathcalx{G}(\mathit{HSel})$. The
redundancy criterion
$(\mathit{HRed}_{\mathrm{I}},{\mathit{HRed}_{\mathrm{C}}})$ matches exactly
the intersected lifted redundancy criterion
$\mathit{Red}^{\mathrel{\cap}\mathcalx{G},\sqsupset}$ of Waldmann et al.
Theorem 14 of Waldmann et al. states the theorem only for
${\sqsupset}=\varnothing$. By Lemma 16 of Waldmann et al., it also holds if
${\sqsupset}\not=\varnothing$. ∎

Let $N\subseteq\mathcalx{C}_{\mathrm{H}}$ be a clause set saturated w.r.t.
$\mathit{HInf}$ and $\mathit{HRed}_{\mathrm{I}}$. We assume that
$\mathit{HSel}$ fulfills the selection restrictions introduced in Section
12.1. For the above theorem to apply, we need to show that there exists a
selection function $\mathit{GHSel}\in\mathcalx{G}(\mathit{HSel})$ such that
all inferences $\iota\in\mathit{GHInf}^{\mathit{GHSel}}$ with
$\mathit{prems}(\iota)\in\mathcalx{G}(N)$ are liftable or redundant. Here, by
_liftable_ , we mean that $\iota$ is a
$\smash{\mathcalx{G}^{\mathit{GHSel}}}$-ground instance of a
$\smash{\mathit{HInf}}$-inference from $N$; by _redundant_ , we mean that
$\iota\in\smash{\mathit{GHRed}_{\mathrm{I}}^{\mathit{GHSel}}(\mathcalx{G}(N))}$.

To choose the right selection function
$\mathit{GHSel}\in\mathcalx{G}(\mathit{HSel})$, we observe that each ground
clause $C\in\mathcalx{G}(N)$ must have at least one corresponding clause $D\in
N$ such that $C$ is a ground instance of $D$. We choose one of them for each
$C\in\mathcalx{G}(N)$, which we denote by $\mathcalx{G}^{-1}(C)$. Then let
$\mathit{GHSel}$ select those literals in $C$ that correspond to the literals
selected by $\mathit{HSel}$ in $\mathcalx{G}^{-1}(C)$. Given this selection
function $\mathit{GHSel}$, we can show that all inferences from
$\mathcalx{G}(N)$ are liftable or redundant.

All non-Sup inferences in $\mathit{GHInf}$ are liftable (Lemma 19.3). For Sup,
some inferences are liftable (Lemma 19.3) and some are redundant (Lemma 19.3).
As in standard superposition, Sup inferences into positions below variables
are redundant. The variable condition of each of the four calculi is designed
to cover the nonredundant Sup inferences into positions of variable-headed
terms, which makes these inferences liftable.

######  Lemma .

Let $\sigma$ be the most general unifier of $s$ and $s^{\prime}$. Let $\theta$
be an arbitrary unifier of $s$ and $s^{\prime}$. Then $\sigma\theta=\theta$.

###### Proof.

Like in first-order logic, we can assume that $\sigma$ is idempotent without
loss of generality [Fit96, Corollary 7.2.11]. Since $\sigma$ is most general,
there exists a substitution $\rho$ such that $\sigma\rho=\theta$. Therefore,
by idempotence, $\sigma\theta=\sigma\sigma\rho=\sigma\rho=\theta$. ∎

######  Lemma  (Lifting of ERes, EFact, GArgCong, and GExt).

All ERes, EFact, GArgCong, and GExt inferences are liftable.

###### Proof.

ERes: Let $\iota\in\mathit{GHInf}^{\mathit{GHSel}}$ be an ERes inference with
$\mathit{prems}(\iota)\in\mathcalx{G}(N)$. Then $\iota$ is of the form

$\prftree[r]{\small{\textsc{ERes}}}{C\theta~{}=~{}C^{\prime}\theta\mathrel{\lor}s\theta\not\approx
s^{\prime}\theta}{C^{\prime}\theta}$

where $\mathcalx{G}^{-1}(C\theta)=C=C^{\prime}\mathrel{\lor}s\not\approx
s^{\prime}$ and the literal $s\theta\not\approx s^{\prime}\theta$ is eligible
w.r.t. $\mathit{GHSel}$. Let $\sigma=\operatorname{mgu}(s,s^{\prime})$. It
follows that $s\not\approx s^{\prime}$ is eligible in $C$ w.r.t. $\sigma$ and
$\mathit{HSel}$. Moreover, $s\theta$ and $s^{\prime}\theta$ are unifiable and
ground, and therefore $s\theta=s^{\prime}\theta$. Thus, the following
inference $\iota^{\prime}\in\mathit{HInf}$ is applicable:

$\prftree[r]{\small{\textsc{ERes}}}{C^{\prime}\mathrel{\lor}s\not\approx
s^{\prime}}{\operatorname{\mathcalx{pure}}(C^{\prime}\sigma)}$

(where $\operatorname{\mathcalx{pure}}$ is the identity in the nonpurifying
calculi). By Lemma 19.3, we have $C^{\prime}\sigma\theta=C^{\prime}\theta$.
Therefore, $\iota$ is the $\theta$-ground instance of $\iota^{\prime}$ and is
therefore liftable.

EFact: Analogously, if $\iota\in\mathit{GHInf}^{\mathit{GHSel}}$ is an EFact
inference with $\mathit{prems}(\iota)\in\mathcalx{G}(N)$, then $\iota$ is of
the form

$\prftree[r]{\small{\textsc{EFact}}}{C\theta~{}=~{}C^{\prime}\theta\mathrel{\lor}s^{\prime}\theta\approx
t^{\prime}\theta\mathrel{\lor}s\theta\approx
t\theta}{C^{\prime}\theta\mathrel{\lor}t\theta\not\approx
t^{\prime}\theta\mathrel{\lor}s\theta\approx t^{\prime}\theta}$

where $\mathcalx{G}^{-1}(C\theta)=C=C^{\prime}\mathrel{\lor}s^{\prime}\approx
t^{\prime}\mathrel{\lor}s\approx t$, the literal $s\theta\approx t\theta$ is
eligible in $C$ w.r.t. $\mathit{GHSel}$, and $s\theta\not\prec t\theta$. Let
$\sigma=\operatorname{mgu}(s,s^{\prime})$. Hence, $s\approx t$ is eligible in
$C$ w.r.t. $\sigma$ and $\mathit{HSel}$. We have $s\not\prec t$. Moreover,
$s\theta$ and $s^{\prime}\theta$ are unifiable and ground. Hence,
$s\theta=s^{\prime}\theta$. Thus, the following inference
$\iota^{\prime}\in\mathit{HInf}$ is applicable:

$\prftree[r]{\small{\textsc{EFact}}}{C^{\prime}\mathrel{\lor}s^{\prime}\approx
t^{\prime}\mathrel{\lor}s\approx
t}{\operatorname{\mathcalx{pure}}((C^{\prime}\mathrel{\lor}t\not\approx
t^{\prime}\mathrel{\lor}s\approx t^{\prime})\sigma)}$

By Lemma 19.3, we have
$\mathit{preconcl}(\iota^{\prime})\theta=\mathit{concl}(\iota)$. Hence,
$\iota$ is the $\theta$-ground instance of $\iota^{\prime}$ and is therefore
liftable.

GArgCong: Let $\iota\in\mathit{GHInf}^{\mathit{GHSel}}$ be a GArgCong
inference with $\mathit{prems}(\iota)\in\mathcalx{G}(N)$. Then $\iota$ is of
the form

$\prftree[r]{\small{\textsc{GArgCong}}}{C\theta~{}=~{}C^{\prime}\theta\mathrel{\lor}s\theta\approx
s^{\prime}\theta}{C^{\prime}\theta\mathrel{\lor}s\theta\>\bar{u}_{n}\approx
s^{\prime}\theta\>\bar{u}_{n}}$

where $\mathcalx{G}^{-1}(C\theta)=C=C^{\prime}\mathrel{\lor}s\approx
s^{\prime}$, the literal $s\theta\approx s^{\prime}\theta$ is strictly
eligible w.r.t. $\mathit{GHSel}$, and $s\theta$ and $s^{\prime}\theta$ are of
functional type. It follows that $s$ and $s^{\prime}$ have either a functional
or a polymorphic type. Let $\sigma$ be the most general substitution such that
$s\sigma$ and $s^{\prime}\sigma$ take $n$ arguments. Then $s\not\approx
s^{\prime}$ is eligible in $C$ w.r.t. $\sigma$ and $\mathit{HSel}$. Hence the
following inference $\iota^{\prime}\in\mathit{HInf}$ is applicable:

$\prftree[r]{\small{\textsc{ArgCong}}}{C^{\prime}\mathrel{\lor}s\approx
s^{\prime}}{\operatorname{\mathcalx{pure}}(C^{\prime}\sigma\mathrel{\lor}s\sigma\>\bar{x}_{n}\approx
s^{\prime}\sigma\>\bar{x}_{n})}$

Then $\iota$ is a ground instance of $\iota^{\prime}$ and is therefore
liftable.

GExt: The conclusion of a GExt inference in $\mathit{GHInf}$ is by definition
a ground instance of the conclusion of the Ext inference in $\mathit{HInf}$
before purification. Hence, the GExt inference is a ground instance of the Ext
inference. Therefore it is liftable. ∎

######  Lemma  (Lifting of Sup).

Let $\iota\in\mathit{GHInf}^{\mathit{GHSel}}$ be a Sup inference

$\prftree[r]{\small{\textsc{Sup}}}{D^{\prime}\theta\mathrel{\lor}t\theta\approx
t^{\prime}\theta\quad
C^{\prime}\theta\mathrel{\lor}s\theta\begin{picture}(5.0,7.0)\put(1.1,3.0){\rotatebox{45.0}{\line(1,0){6.0}}}
\put(1.1,3.0){\rotatebox{315.0}{\line(1,0){6.0}}} \end{picture}\kern
0.83328ptt\theta\begin{picture}(5.0,7.0)\put(0.1,3.0){\rotatebox{135.0}{\line(1,0){6.0}}}
\put(0.1,3.0){\rotatebox{225.0}{\line(1,0){6.0}}}
\end{picture}\,_{p}\mathrel{\dot{\approx}}s^{\prime}\theta}{D^{\prime}\theta\mathrel{\lor}C^{\prime}\theta\mathrel{\lor}s\theta\begin{picture}(5.0,7.0)\put(1.1,3.0){\rotatebox{45.0}{\line(1,0){6.0}}}
\put(1.1,3.0){\rotatebox{315.0}{\line(1,0){6.0}}} \end{picture}\kern