∎ notyet

11institutetext: Alexander Bentkamp (✉)22institutetext: Jasmin Blanchette
33institutetext: Petar Vukmirović44institutetext: Vrije Universiteit
Amsterdam, Department of Computer Science, Section of Theoretical Computer
Science, De Boelelaan 1111, 1081 HV Amsterdam, the Netherlands
44email<EMAIL_ADDRESS>55institutetext:
Jasmin Blanchette 66institutetext: Sophie Tourret 77institutetext: Uwe
Waldmann 88institutetext: Max-Planck-Institut für Informatik, Saarland
Informatics Campus E1 4, 66123 Saarbrücken, Germany
88email<EMAIL_ADDRESS>
# Superposition with Lambdas

Alexander Bentkamp  Jasmin Blanchette  Sophie Tourret  Petar Vukmirović  Uwe
Waldmann

(Received: date / Accepted: date)

###### Abstract

We designed a superposition calculus for a clausal fragment of extensional
polymorphic higher-order logic that includes anonymous functions but excludes
Booleans. The inference rules work on $\beta\eta$-equivalence classes of
$\lambda$-terms and rely on higher-order unification to achieve refutational
completeness. We implemented the calculus in the Zipperposition prover and
evaluated it on TPTP and Isabelle benchmarks. The results suggest that
superposition is a suitable basis for higher-order reasoning.

###### Keywords:

superposition calculus higher-order logic refutational completeness

††journal: J. Autom. Reasoning

##  1 Introduction

Superposition bachmair-ganzinger-1994  is widely regarded as the calculus par
excellence for reasoning about first-order logic with equality. To increase
automation in proof assistants and other verification tools based on higher-
order formalisms, we propose to generalize superposition to an extensional,
polymorphic, clausal version of higher-order logic (also called simple type
theory). Our ambition is to achieve a _graceful_ extension, which coincides
with standard superposition on first-order problems and smoothly scales up to
arbitrary higher-order problems.

Bentkamp, Blanchette, Cruanes, and Waldmann bentkamp-et-al-2018  designed a
family of superposition-like calculi for a $\lambda$-free clausal fragment of
higher-order logic, with currying and applied variables. We adapt their
extensional nonpurifying calculus to support $\lambda$-terms (Sect. 3). Our
calculus does not support interpreted Booleans; it is conceived as the
penultimate milestone towards a superposition calculus for full higher-order
logic. If desired, Booleans can be encoded in our logic fragment using an
uninterpreted type and uninterpreted “proxy” symbols corresponding to
equality, the connectives, and the quantifiers.

Designing a higher-order superposition calculus poses three main challenges:

  1. 1.

Standard superposition is parameterized by a ground-total simplification order
$\succ$, but such orders do not exist for $\lambda$-terms equal up to
$\beta$-conversion. The relations designed for proving termination of higher-
order term rewriting systems, such as HORPO jouannaud-rubio-2007  and CPO
blanqui-et-al-2015 , lack many of the desired properties (e.g., transitivity,
stability under grounding substitutions).

  2. 2.

Higher-order unification is undecidable and may give rise to an infinite set
of incomparable unifiers. For example, the constraint
${\mathsf{f}}\>(y\>{\mathsf{a}})\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}y\>({\mathsf{f}}\>{\mathsf{a}})$
admits infinitely many independent solutions of the form $\\{y\mapsto\lambda
x.\;{\mathsf{f}}^{n}\,x\\}.$

  3. 3.

In first-order logic, to rewrite into a term $s$ using an oriented equation
$t\approx t^{\prime}$, it suffices to find a subterm of $s$ that is unifiable
with $t$. In higher-order logic, this is insufficient. Consider superposition
from ${\mathsf{f}}\>{\mathsf{c}}\approx{\mathsf{a}}$ into
$y\>{\mathsf{c}}\not\approx y\>{\mathsf{b}}$. The left-hand sides can
obviously be unified by $\\{y\mapsto{\mathsf{f}}\\}$, but the more general
$\\{y\mapsto\lambda x.\>z\>x\>({\mathsf{f}}\>x)\\}$ also gives rise to a
subterm ${\mathsf{f}}\>{\mathsf{c}}$ after $\beta$-reduction. The
corresponding inference generates the clause
$z\>{\mathsf{c}}\>{\mathsf{a}}\not\approx
z\>{\mathsf{b}}\>({\mathsf{f}}\>{\mathsf{b}})$.

To address the first challenge, we adopt the $\eta$-short $\beta$-normal form
to represent $\beta\eta$-equivalence classes of $\lambda$-terms. In the spirit
of Jouannaud and Rubio’s early joint work jouannaud-rubio-1998 , we state
requirements on the term order only for ground terms (i.e., closed monomorphic
$\beta\eta$-equivalence classes); the nonground case is connected to the
ground case via stability under grounding substitutions. Even on ground terms,
we cannot obtain all desirable properties. We sacrifice compatibility with
arguments (the property that $s^{\prime}\succ s$ implies $s^{\prime}\>t\succ
s\>t$), compensating with an _argument congruence_ rule (ArgCong), as in
Bentkamp et al. bentkamp-et-al-2018 .

For the second challenge, we accept that there might be infinitely many
incomparable unifiers and enumerate a complete set (including the notorious
flex–flex pairs huet-1975 ), relying on heuristics to postpone the
combinatorial explosion. The saturation loop must also be adapted to
interleave this enumeration with the theorem prover’s other activities (Sect.
6). Despite its reputation for explosiveness, higher-order unification is a
conceptual improvement over ${\mathsf{SK}}$ combinators, because it can often
_compute_ the right unifier. Consider the conjecture $\exists z.\>\forall
x\>y.\>z\>x\>y\approx{\mathsf{f}}\>y\>x$. After negation, clausification, and
skolemization (which are as for first-order logic), the formula becomes
$z\>({\mathsf{sk}}_{\mathsf{x}}\>z)\>({\mathsf{sk}}_{\mathsf{y}}\>z)\not\approx{\mathsf{f}}\>({\mathsf{sk}}_{\mathsf{y}}\>z)\>({\mathsf{sk}}_{\mathsf{x}}\>z)$.
Higher-order unification quickly computes the unique unifier:
$\\{z\mapsto\lambda x\>y.\>{\mathsf{f}}\>y\>x\\}$. In contrast, an encoding
approach based on combinators, similar to the one implemented in Sledgehammer
meng-paulson-2008-trans , would blindly enumerate all possible ${\mathsf{SK}}$
terms for $z$ until the right one,
${\mathsf{S}}\>({\mathsf{K}}\>({\mathsf{S}}\>{\mathsf{f}}))\>{\mathsf{K}}$, is
found. Given the definitions ${\mathsf{S}}\>z\>y\>x\approx z\>x\>(y\>x)$ and
${\mathsf{K}}\>x\>y\approx x$, the E prover schulz-et-al-2019  in _auto_ mode
needs to perform 3757 inferences to derive the empty clause.

For the third challenge, the idea is that, when applying $t\approx t^{\prime}$
to perform rewriting inside a higher-order term $s$, we can encode an
arbitrary context as a fresh higher-order variable $z$, unifying $s$ with
$z\>t$; the result is $(z\>t^{\prime})\sigma$, for some unifier $\sigma$. This
is performed by a dedicated _fluid subterm superposition_ rule (FluidSup).

Functional extensionality is also considered a quintessential higher-order
challenge benzmueller-kohlhase-1998 , although similar difficulties arise with
first-order sets and arrays gupta-et-al-2014 . Our approach is to add
extensionality as an axiom and provide optional rules as optimizations (Sect.
5). With this axiom, our calculus is refutationally complete w.r.t.
extensional Henkin semantics (Sect. 4). Our proof employs the new saturation
framework by Waldmann et al. waldmann-et-al-2020-saturation  to derive dynamic
completeness of a given clause prover from ground static completeness.

We implemented the calculus in the Zipperposition prover cruanes-2017  (Sect.
6). Our empirical evaluation includes benchmarks from the TPTP
sutcliffe-2017-tptp  and interactive verification problems exported from
Isabelle/HOL boehme-nipkow-2010  (Sect. 7). The results clearly demonstrate
the calculus’s potential. The 2020 edition of the CADE ATP System Competition
(CASC) provides further confirmation: Zipperposition finished 20 percentage
points ahead of its closest rival. This suggests that an implementation inside
a high-performance prover such as E schulz-et-al-2019  or Vampire kovacs-
voronkov-2013  could fulfill the promise of strong proof automation for
higher-order logic (Sect. 8).

An earlier version of this article was presented at CADE-27 bentkamp-et-
al-2019-lamsup . This article extends the conference paper with more
explanations, detailed soundness and completeness proofs, including dynamic
completeness, and new optional inference rules. We have also updated the
empirical evaluation and extended the coverage of related work. Finally, we
tightened side condition 4 of FluidSup, making the rule slightly less
explosive.

##  2 Logic

Our extensional polymorphic clausal higher-order logic is a restriction of
full TPTP THF benzmueller-paulson-2010  to rank-1 (top-level) polymorphism, as
in TH1 kaliszyk-et-al-2016 . In keeping with standard superposition, we
consider only formulas in conjunctive normal form, without explicit
quantifiers or Boolean type. We use Henkin semantics henkin-1950 ;
benzmueller-miller-2014 ; fitting-2002 , as opposed to the standard semantics
that is commonly considered the foundation of the HOL systems gordon-
melham-1993 . However, both of these semantics are compatible with the notion
of provability employed by the HOL systems. By admitting nonstandard models,
Henkin semantics is not subject to Gödel’s first incompleteness theorem,
allowing us to claim not only soundness but also refutational completeness of
our calculus.

#### Syntax

We fix a set $\mathrm{\Sigma}_{\mathsf{ty}}$ of type constructors with arities
and a set $\mathscr{V}_{\mathsf{ty}}$ of type variables. We require at least
one nullary type constructor and a binary function type constructor
${\rightarrow}$ to be present in $\mathrm{\Sigma}_{\mathsf{ty}}$. A type
$\tau,\upsilon$ is either a type variable $\alpha\in\mathscr{V}_{\mathsf{ty}}$
or has the form $\kappa(\bar{\tau}_{n})$ for an $n$-ary type constructor
$\kappa\in\mathrm{\Sigma}_{\mathsf{ty}}$ and types $\bar{\tau}_{n}$. We use
the notation $\bar{a}_{n}$ or $\bar{a}$ to stand for the tuple
$(a_{1},\dots,a_{n})$ or product $a_{1}\times\dots\times a_{n}$, where $n\geq
0$. We write $\kappa$ for $\kappa()$ and $\tau\rightarrow\upsilon$ for
${\rightarrow}(\tau,\upsilon)$. Type declarations have 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 (function) symbols
${\mathsf{a}},{\mathsf{b}},{\mathsf{c}},{\mathsf{f}},{\mathsf{g}},{\mathsf{h}},\dots$,
with type declarations, written as
${\mathsf{f}}:\mathsf{\Pi}\bar{\alpha}_{m}.\;\tau$ or ${\mathsf{f}}$, and a
set $\mathscr{V}$ of term variables with associated types, written as
${\mathit{x}}:\tau$ or ${\mathit{x}}$. The notation $t:\tau$ will also be used
to indicate the type of arbitrary terms $t$. We require the presence of a
symbol of type $\mathsf{\Pi}\alpha.\;\alpha$ and of a symbol
${\mathsf{diff}}:\mathsf{\Pi}\alpha,\beta.\;(\alpha\rightarrow\beta)\rightarrow(\alpha\rightarrow\beta)\rightarrow{\alpha}$
in $\mathrm{\Sigma}$. We use ${\mathsf{diff}}$ to express the polymorphic
functional extensionality axiom. A signature is a pair
$(\mathrm{\Sigma}_{\mathsf{ty}},\mathrm{\Sigma})$.

In the following, we will define terms in three layers of abstraction: raw
$\lambda$-terms, $\lambda$-terms, and terms; where $\lambda$-terms will be
$\alpha$-equivalence classes of raw $\lambda$-terms and terms will be
$\beta\eta$-equivalence classes of $\lambda$-terms.

The _raw $\lambda$-terms_ over a given signature and their associated types
are defined inductively as follows. Every $x\mathbin{:}\tau\in\mathscr{V}$ is
a raw $\lambda$-term of type $\tau$. If
${\mathsf{f}}:\mathsf{\Pi}\bar{\alpha}_{m}.\;\tau\in\mathrm{\Sigma}$ and
$\bar{\upsilon}_{m}$ is a tuple of types, called _type arguments_ , then
${\mathsf{f}}{\langle\bar{\upsilon}_{m}\rangle\kern-0.83328pt}$ (or
${\mathsf{f}}$ if $m=0$) is a raw $\lambda$-term of type
$\tau\\{\bar{\alpha}_{m}\mapsto\bar{\upsilon}_{m}\\}$. If $x\mathbin{:}\tau$
and $t:\upsilon$, then the _$\lambda$ -expression_ $\lambda x.\>t$ is a raw
$\lambda$-term of type $\tau\rightarrow\upsilon$. If
$s:\tau\rightarrow\upsilon$ and $t:\tau$, then the _application_ $s\>t$ is a
raw $\lambda$-term of type $\upsilon$.

The function type constructor $\rightarrow$ is right-associative; application
is left-associative. Using the spine notation cervesato-pfenning-2003 , raw
$\lambda$-terms can be decomposed in a unique way as a nonapplication _head_
$t$ applied to zero or more arguments: $t\>s_{1}\dots s_{n}$ or
$t\>\bar{s}_{n}$ (abusing notation).

A raw $\lambda$-term $s$ is a _subterm_ of a raw $\lambda$-term $t$, written
$t=t[s]$, if $t=s$, if $t=(\lambda x.\>u[s])$, if $t=(u[s])\>v$, or if
$t=u\>(v[s])$ for some raw $\lambda$-terms $u$ and $v$. A _proper_ subterm of
a raw $\lambda$-term $t$ is any subterm of $t$ that is distinct from $t$
itself.

A variable occurrence is _free_ in a raw $\lambda$-term if it is not bound by
a $\lambda$-expression. A raw $\lambda$-term is _ground_ if it is built
without using type variables and contains no free term variables.

The $\alpha$-renaming rule is defined as $(\lambda x.\>t)\kern
0.83328pt\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}}_{\alpha}\kern
0.83328pt(\lambda y.\>t\\{x\mapsto y\\})$, where $y$ does not occur free in
$t$ and is not captured by a $\lambda$-binder in $t$. Raw $\lambda$-terms form
equivalence classes modulo $\alpha$-renaming, called _$\lambda$ -terms_. We
lift the above notions on raw $\lambda$-terms to $\lambda$-terms.

A substitution $\rho$ is a function from type variables to types and from term
variables to $\lambda$-terms such that it maps all but finitely many variables
to themselves. We require that it is type-correct—i.e., for each
$x:\tau\in\mathscr{V}$, $x\rho$ is of type $\tau\rho$. The letters
$\theta,\pi,\rho,\sigma$ are reserved for substitutions. Substitutions
$\alpha$-rename $\lambda$-terms to avoid capture; for example, $(\lambda
x.\>y)\\{y\mapsto x\\}=(\lambda x^{\prime}\\!.\>x)$. The composition
$\rho\sigma$ applies $\rho$ first: $t\rho\sigma=(t\rho)\sigma$. The notation
$\sigma[\bar{x}_{n}\mapsto\bar{s}_{n}]$ denotes the substitution that replaces
each $x_{i}$ by $s_{i}$ and that otherwise coincides with $\sigma$.

The $\beta$\- and $\eta$-reduction rules are specified on $\lambda$-terms as
$(\lambda x.\>t)\>u\kern
0.83328pt\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}}_{\beta}\kern
0.83328ptt\\{x\mapsto u\\}$ and $(\lambda x.\>t\>x)\kern
0.83328pt\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}}_{\eta}\kern
0.83328ptt$. For $\beta$, bound variables in $t$ are implicitly renamed to
avoid capture; for $\eta$, the variable $x$ must not occur free in $t$. The
$\lambda$-terms form equivalence classes modulo $\beta\eta$-reduction, called
_$\beta\eta$ -equivalence classes_ or simply _terms_.

###### Convention 2.1

When defining operations that need to analyze the structure of terms, we will
use the $\eta$-short $\beta$-normal form $t\kern
0.83328pt{\downarrow}_{\beta\eta}$, obtained by applying
$\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}}_{\beta}$
and
$\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}}_{\eta}$
exhaustively, as a representative of the equivalence class $t$. In particular,
we lift the notions of subterms and occurrences of variables to
$\beta\eta$-equivalence classes via their $\eta$-short $\beta$-normal
representative.

Many authors prefer the $\eta$-long $\beta$-normal form huet-1975 ; mayr-
nipkow-1998 ; jouannaud-rubio-1998 , but in a polymorphic setting it has the
drawback that instantiating a type variable with a functional type can lead to
$\eta$-expansion. We reserve the letters $s,t,u,v$ for terms and $x,y,z$ for
variables.

An equation $s\approx t$ is formally an unordered pair of terms $s$ and $t$. A
literal is an equation or a negated equation, written $\lnot\;s\approx t$ or
$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$.

A _complete set of unifiers_ on a set $X$ of variables for two terms $s$ and
$t$ is a set $U$ of unifiers of $s$ and $t$ such that for every unifier
$\theta$ of $s$ and $t$ there exists a member $\sigma\in U$ and a substitution
$\rho$ such that $x\sigma\rho=x\theta$ for all $x\in X.$ We let
$\operatorname{CSU}_{X}(s,t)$ denote an arbitrary (preferably minimal)
complete set of unifiers on $X$ for $s$ and $t$. We assume that all
$\sigma\in\operatorname{CSU}_{X}(s,t)$ are idempotent on $X$—i.e.,
$x\sigma\sigma=x\sigma$ for all $x\in X.$ The set $X$ will consist of the free
variables of the clauses in which $s$ and $t$ occur and will be left implicit.

Given a substitution $\sigma$, the $\sigma$-instance of a term $t$ or clause
$C$ is the term $t\sigma$ or the clause $C\sigma$, respectively. If $t\sigma$
or $C\sigma$ is ground, we call it a $\sigma$-ground instance.

#### Semantics

A _type interpretation_
$\mathscr{I}_{\mathsf{ty}}=(\mathscr{U},\mathscr{J}_{\mathsf{ty}})$ is defined
as follows. The _universe_ $\mathscr{U}$ is a nonempty collection of nonempty
sets, called _domains_. The function $\mathscr{J}_{\mathsf{ty}}$ associates a
function
$\mathscr{J}_{\mathsf{ty}}(\kappa):\mathscr{U}^{n}\rightarrow\mathscr{U}$ with
each $n$-ary type constructor $\kappa$, such that for all domains
$\mathscr{D}_{1},\mathscr{D}_{2}\in\mathscr{U}$, the set
$\mathscr{J}_{\mathsf{ty}}(\rightarrow)(\mathscr{D}_{1},\mathscr{D}_{2})$ is a
subset of the function space from $\mathscr{D}_{1}$ to $\mathscr{D}_{2}$. The
semantics is _standard_ if
$\mathscr{J}_{\mathsf{ty}}(\rightarrow)(\mathscr{D}_{1},\mathscr{D}_{2})$ is
the entire function space for all $\mathscr{D}_{1},\mathscr{D}_{2}$.

A _type valuation_ $\xi$ is a function that maps every type variable to a
domain. The _denotation_ of a type for a type interpretation
$\mathscr{I}_{\mathsf{ty}}$ and a type valuation $\xi$ is defined by
$\smash{\llbracket\alpha\rrbracket_{\mathscr{I}_{\mathsf{ty}}}^{\xi}}=\xi(\alpha)$
and
$\smash{\llbracket\kappa(\bar{\tau})\rrbracket_{\mathscr{I}_{\mathsf{ty}}}^{\xi}}=\mathscr{J}_{\mathsf{ty}}(\kappa)(\smash{\llbracket\bar{\tau}\rrbracket_{\mathscr{I}_{\mathsf{ty}}}^{\xi}})$.
We abuse notation by applying an operation on a tuple when it must be applied
elementwise; thus,
$\smash{\llbracket\bar{\tau}_{n}\rrbracket_{\mathscr{I}_{\mathsf{ty}}}^{\xi}}$
stands for
$\smash{\llbracket\tau_{1}\rrbracket_{\mathscr{I}_{\mathsf{ty}}}^{\xi}},\dots,\smash{\llbracket\tau_{n}\rrbracket_{\mathscr{I}_{\mathsf{ty}}}^{\xi}}$.
A type valuation $\xi$ can be extended to be a _valuation_ by additionally
assigning an element
$\xi(x)\in\smash{\llbracket\tau\rrbracket_{\mathscr{I}_{\mathsf{ty}}}^{\xi}}$
to each variable $x:\tau$. An _interpretation function_ $\mathscr{J}$ for a
type interpretation $\mathscr{I}_{\mathsf{ty}}$ associates with each symbol
${\mathsf{f}}:\mathsf{\Pi}\bar{\alpha}_{m}.\;\tau$ and domain tuple
$\bar{\mathscr{D}}_{m}\in\mathscr{U}^{m}$ a value
$\mathscr{J}({\mathsf{f}},\bar{\mathscr{D}}_{m})\in\smash{\llbracket\tau\rrbracket_{\mathscr{I}_{\mathsf{ty}}}^{\xi}}$,
where $\xi$ is the type valuation that maps each $\alpha_{i}$ to
$\mathscr{D}_{i}$.

The comprehension principle states that every function designated by a
$\lambda$-expression is contained in the corresponding domain. Loosely
following Fitting (fitting-2002, , Sect. 2.4), we initially allow
$\lambda$-expressions to designate arbitrary elements of the domain, to be
able to define the denotation of a term. We impose restrictions afterwards
using the notion of a proper interpretation. A _$\lambda$ -designation
function_ $\mathscr{L}$ for a type interpretation $\mathscr{I}_{\mathsf{ty}}$
is a function that maps a valuation $\xi$ and a $\lambda$-expression of type
$\tau$ to elements of
$\smash{\llbracket\tau\rrbracket_{\mathscr{I}_{\mathsf{ty}}}^{\xi}}$. A type
interpretation, an interpretation function, and a $\lambda$-designation
function form an (_extensional_) _interpretation_
$\mathscr{I}=(\mathscr{I}_{\mathsf{ty}},\mathscr{J},\mathscr{L})$. For an
interpretation $\mathscr{I}$ and a valuation $\xi$, the denotation of a term
is defined as $\smash{\llbracket x\rrbracket_{\mathscr{I}}^{\xi}}=\xi(x)$,
$\smash{\llbracket{\mathsf{f}}{\langle\bar{\tau}_{m}\rangle\kern-0.83328pt}\rrbracket_{\mathscr{I}}^{\xi}}=\mathscr{J}({\mathsf{f}},\smash{\llbracket\bar{\tau}_{m}\rrbracket_{\mathscr{I}_{\mathsf{ty}}}^{\xi}})$,
$\smash{\llbracket s\>t\rrbracket_{\mathscr{I}}^{\xi}}=\smash{\llbracket
s\rrbracket_{\mathscr{I}}^{\xi}}(\smash{\llbracket
t\rrbracket_{\mathscr{I}}^{\xi}})$, and $\smash{\llbracket\lambda
x.\>t\rrbracket_{\mathscr{I}}^{\xi}}=\mathscr{L}(\xi,\lambda x.\>t)$. For
ground terms $t$, the denotation does not depend on the choice of the
valuation $\xi$, which is why we sometimes write $\smash{\llbracket
t\rrbracket_{\mathscr{I}}}$ for $\smash{\llbracket
t\rrbracket_{\mathscr{I}}^{\xi}}$.

An interpretation $\mathscr{I}$ is _proper_ if $\smash{\llbracket\lambda
x.\>t\rrbracket_{\mathscr{I}}^{\xi}}(a)=\smash{\llbracket
t\rrbracket_{\mathscr{I}}^{\xi[x\mapsto a]}}$ for all $\lambda$-expressions
$\lambda x.\>t$, all valuations $\xi$, and all $a$. If a type interpretation
$\mathscr{I}_{\mathsf{ty}}$ and an interpretation function $\mathscr{J}$ can
be extended by a $\lambda$-designation function $\mathscr{L}$ to a proper
interpretation $(\mathscr{I}_{\mathsf{ty}},\mathscr{J},\mathscr{L})$, then
this $\mathscr{L}$ is unique (fitting-2002, , Proposition 2.18). Given an
interpretation $\mathscr{I}$ and a valuation $\xi$, an equation $s\approx t$
is true if $\smash{\llbracket s\rrbracket_{\mathscr{I}}^{\xi}}$ and
$\smash{\llbracket t\rrbracket_{\mathscr{I}}^{\xi}}$ are equal and it is false
otherwise. 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. A clause set is true
if all its clauses are true. A proper interpretation $\mathscr{I}$ is a
_model_ of a clause set $N$, written $\mathscr{I}\models N$, if $N$ is true in
$\mathscr{I}$ for all valuations $\xi$.

#### Axiomatization of Booleans

Our clausal logic lacks a Boolean type, but it can easily be axiomatized as
follows. We extend the signature with a nullary type constructor
${\mathit{bool}}\in\mathrm{\Sigma}_{\mathsf{ty}}$ equipped with the proxy
constants ${\mathsf{t}},{\mathsf{f}}:{\mathit{bool}}$,
${\mathsf{not}}:{\mathit{bool}}\rightarrow{\mathit{bool}}$,
${\mathsf{and}},{\mathsf{or}},{\mathsf{impl}},{\mathsf{equiv}}:{\mathit{bool}}\rightarrow{\mathit{bool}}\rightarrow{\mathit{bool}}$,
${\mathsf{forall}},{\mathsf{exists}}:\mathsf{\Pi}\alpha.\;(\alpha\rightarrow{\mathit{bool}})\rightarrow{\mathit{bool}}$,
${\mathsf{eq}}:\mathsf{\Pi}\alpha.\;\alpha\rightarrow\alpha\rightarrow{\mathit{bool}}$,
and
${\mathsf{choice}}:\mathsf{\Pi}\alpha.\;(\alpha\rightarrow{\mathit{bool}})\rightarrow\alpha$,
characterized by the axioms

${\mathsf{t}}\not\approx{\mathsf{f}}$

$x\approx{\mathsf{t}}\mathrel{\lor}x\approx{\mathsf{f}}$

${\mathsf{not}}\>{\mathsf{t}}\approx{\mathsf{f}}$

${\mathsf{not}}\>{\mathsf{f}}\approx{\mathsf{t}}$

${\mathsf{and}}\>{\mathsf{t}}\>x\approx x$

${\mathsf{and}}\>{\mathsf{f}}\>x\approx{\mathsf{f}}$

${\mathsf{or}}\>{\mathsf{t}}\>x\approx{\mathsf{t}}$

${\mathsf{or}}\>{\mathsf{f}}\>x\approx x$

${\mathsf{impl}}\>{\mathsf{t}}\>x\approx x$

${\mathsf{impl}}\>{\mathsf{f}}\>x\approx{\mathsf{t}}$

$x\not\approx
y\mathrel{\lor}{\mathsf{eq}}{\langle\alpha\rangle\kern-0.83328pt}\;x\>y\approx{\mathsf{t}}$

$x\approx
y\mathrel{\lor}{\mathsf{eq}}{\langle\alpha\rangle\kern-0.83328pt}\;x\>y\approx{\mathsf{f}}$

${\mathsf{equiv}}\>x\>y\approx{\mathsf{and}}\>({\mathsf{impl}}\>x\>y)\>({\mathsf{impl}}\>y\>x)$

${\mathsf{forall}}{\langle\alpha\rangle\kern-0.83328pt}\;(\lambda
x.\;{\mathsf{t}})\approx{\mathsf{t}}$

$y\approx(\lambda
x.\;{\mathsf{t}})\mathrel{\lor}{\mathsf{forall}}{\langle\alpha\rangle\kern-0.83328pt}\;y\approx{\mathsf{f}}$

${\mathsf{exists}}{\langle\alpha\rangle\kern-0.83328pt}\;y\approx{\mathsf{not}}\>({\mathsf{forall}}{\langle\alpha\rangle\kern-0.83328pt}\;(\lambda
x.\>{\mathsf{not}}\>(y\>x)))$

$y\>x\approx{\mathsf{f}}\mathrel{\lor}y\>(\textsf{choice}{\langle\alpha\rangle\kern-0.83328pt}\>y)\approx{\mathsf{t}}$

This axiomatization of Booleans can be used in a prover to support full
higher-order logic with or without Hilbert choice, corresponding to the TPTP
THF format variants TH0 (monomorphic) sutcliffe-et-al-2009  and TH1
(polymorphic) kaliszyk-et-al-2016 . The prover’s clausifier would transform
the outer first-order skeleton of a formula into a clause and use the
axiomatized Booleans within the terms. It would also add the proxy axioms to
the clausal problem. As an alternative to this complete axiomatization,
Vukmirović and Nummelin vukmirovic-nummelin-2020-boolean  present a possibly
refutationally incomplete calculus extension with dedicated rules to support
Booleans. This approach works better in practice and contributed to
Zipperposition’s victory at CASC 2020.

##  3 The Calculus

Our _Boolean-free $\lambda$-superposition calculus_ presented here is inspired
by the extensional nonpurifying Boolean-free $\lambda$-free higher-order
superposition calculus described by Bentkamp et al. bentkamp-et-al-2018 . The
text of this and the next section is partly based on that paper and the
associated journal submission bentkamp-et-al-lfhosup-arxiv  (with Cruanes’s
permission). The central idea is that superposition inferences are restricted
to _unapplied_ subterms occurring in the first-order outer skeleton of
clauses—that is, outside $\lambda$-expressions and outside the arguments of
applied variables. We call these “green subterms.” Thus,
${\mathsf{g}}\approx(\lambda x.\>{\mathsf{f}}\>x\>x)$ cannot be used directly
to rewrite ${\mathsf{g}}\>{\mathsf{a}}$ to
${\mathsf{f}}\>{\mathsf{a}}\>{\mathsf{a}}$, because ${\mathsf{g}}$ is applied
in ${\mathsf{g}}\>{\mathsf{a}}$. A separate inference rule, ArgCong, takes
care of deriving ${\mathsf{g}}\>x\approx{\mathsf{f}}\>x\>x$, which can be
oriented independently of its parent clause and used to rewrite
${\mathsf{g}}\>{\mathsf{a}}$ or ${\mathsf{f}}\>{\mathsf{a}}\>{\mathsf{a}}$.

######  Definition 3.1 (Green positions and subterms)

The _green positions_ and _green subterms_ of a term (i.e., a
$\beta\eta$-equivalence class) are defined inductively as follows. A green
position is a tuple of natural numbers. For any term $t$, the empty tuple
$\varepsilon$ is a green position of $t$, and $t$ is the green subterm of $t$
at position $\varepsilon$. For all symbols ${\mathsf{f}}\in\mathrm{\Sigma}$,
types $\bar{\tau}$, and terms $\bar{u}$, if $t$ is a green subterm of $u_{i}$
at some position $p$ for some $i$, then $i.p$ is a green position of
${\mathsf{f}}{\langle\bar{\tau}\rangle\kern-0.83328pt}\kern
0.83328pt\>\bar{u}$, and $t$ is the green subterm of
${\mathsf{f}}{\langle\bar{\tau}\rangle\kern-0.83328pt}\>\bar{u}$ at position
$i.p$. We denote the green subterm of $s$ at the green position $p$ by
$s|_{p}$.

In ${\mathsf{f}}\>({\mathsf{g}}\>{\mathsf{a}})\>(y\>{\mathsf{b}})\>(\lambda
x.\>{\mathsf{h}}\>{\mathsf{c}}\>({\mathsf{g}}\>x))$, the proper green subterms
are ${\mathsf{a}}$, ${\mathsf{g}}\>{\mathsf{a}}$, $y\>{\mathsf{b}}$, and
$\lambda x.\>{\mathsf{h}}\>{\mathsf{c}}\>({\mathsf{g}}\>x)$. The last two of
these do not look like first-order terms and hence their subterms are not
green.

######  Definition 3.2 (Green contexts)

We write
$t=s\begin{picture}(5.0,7.0)\put(1.1,2.5){\rotatebox{45.0}{\line(1,0){6.0}}}
\put(1.1,2.5){\rotatebox{315.0}{\line(1,0){6.0}}}
\end{picture}\,u\begin{picture}(5.0,7.0)\put(0.0,2.5){\rotatebox{135.0}{\line(1,0){6.0}}}
\put(0.0,2.5){\rotatebox{225.0}{\line(1,0){6.0}}} \end{picture}_{p}$ to
express that $u$ is a green subterm of $t$ at the green position $p$ and call
$s\begin{picture}(5.0,7.0)\put(1.1,2.5){\rotatebox{45.0}{\line(1,0){6.0}}}
\put(1.1,2.5){\rotatebox{315.0}{\line(1,0){6.0}}}
\end{picture}\,\phantom{.}\begin{picture}(5.0,7.0)\put(0.0,2.5){\rotatebox{135.0}{\line(1,0){6.0}}}
\put(0.0,2.5){\rotatebox{225.0}{\line(1,0){6.0}}} \end{picture}_{p}$ a _green
context_. We omit the subscript $p$ if there are no ambiguities.

In a $\beta\eta$-normal representative of a green context, the hole never
occurs applied. Therefore, inserting a $\beta\eta$-normal term into the
context produces another $\beta\eta$-normal term.

Another key notion is that of a fluid term:

######  Definition 3.3 (Fluid terms)

A term $t$ is called _fluid_ if (1) $t\kern 0.83328pt{\downarrow}_{\beta\eta}$
is of the form $y\>\bar{u}_{n}$ where $n\geq 1$, or (2) $t\kern
0.83328pt{\downarrow}_{\beta\eta}$ is a $\lambda$-expression and there exists
a substitution $\sigma$ such that $t\sigma\kern
0.83328pt{\downarrow}_{\beta\eta}$ is not a $\lambda$-expression (due to
$\eta$-reduction).

Case (2) can arise only if $t$ contains an applied variable. Intuitively,
fluid terms are terms whose $\eta$-short $\beta$-normal form can change
radically as a result of instantiation. For example, $\lambda
x.\>y\>{\mathsf{a}}\>(z\>x)$ is fluid because applying $\\{z\mapsto\lambda
x.\>x\\}$ makes the $\lambda$ vanish: $(\lambda
x.\>y\>{\mathsf{a}}\>x)=y\>{\mathsf{a}}$. Similarly, $\lambda
x.\>{\mathsf{f}}\>(y\>x)\>x$ is fluid because $(\lambda
x.\>{\mathsf{f}}\>(y\>x)\>x)\\{y\mapsto\lambda x.\>{\mathsf{a}}\\}=(\lambda
x.\>{\mathsf{f}}\>{\mathsf{a}}\>x)={\mathsf{f}}\>{\mathsf{a}}$.

###  3.1 The Core Inference Rules

The calculus is parameterized by a strict and a nonstrict term order as well
as a selection function. These concepts are defined below.

######  Definition 3.4 (Strict ground term order)

A _strict ground term order_ is a well-founded strict total order $\succ$ on
ground terms satisfying the following criteria, where $\succeq$ denotes the
reflexive closure of $\succ$:

  * –

_green subterm property_ :
$t\begin{picture}(5.0,7.0)\put(1.1,2.5){\rotatebox{45.0}{\line(1,0){6.0}}}
\put(1.1,2.5){\rotatebox{315.0}{\line(1,0){6.0}}}
\end{picture}\,s\begin{picture}(5.0,7.0)\put(0.0,2.5){\rotatebox{135.0}{\line(1,0){6.0}}}
\put(0.0,2.5){\rotatebox{225.0}{\line(1,0){6.0}}} \end{picture}\succeq s$;

  * –

_compatibility with green contexts_ : $s^{\prime}\succ s$ implies
$t\begin{picture}(5.0,7.0)\put(1.1,2.5){\rotatebox{45.0}{\line(1,0){6.0}}}
\put(1.1,2.5){\rotatebox{315.0}{\line(1,0){6.0}}}
\end{picture}\,s^{\prime}\begin{picture}(5.0,7.0)\put(0.0,2.5){\rotatebox{135.0}{\line(1,0){6.0}}}
\put(0.0,2.5){\rotatebox{225.0}{\line(1,0){6.0}}} \end{picture}\succ
t\begin{picture}(5.0,7.0)\put(1.1,2.5){\rotatebox{45.0}{\line(1,0){6.0}}}
\put(1.1,2.5){\rotatebox{315.0}{\line(1,0){6.0}}}
\end{picture}\,s\begin{picture}(5.0,7.0)\put(0.0,2.5){\rotatebox{135.0}{\line(1,0){6.0}}}
\put(0.0,2.5){\rotatebox{225.0}{\line(1,0){6.0}}} \end{picture}$.

Given a strict ground term order, we extend it to literals and clauses via the
multiset extensions in the standard way (bachmair-ganzinger-1994, , Sect.
2.4).

Two properties that are not required are _compatibility with
$\lambda$-expressions_ ($s^{\prime}\succ s$ implies $(\lambda
x.\>s^{\prime})\succ(\lambda x.\>s)$) and _compatibility with arguments_
($s^{\prime}\succ s$ implies $s^{\prime}\>{t}\succ s\kern 0.83328pt\>{t}$).
The latter would even be inconsistent with totality. To see why, consider the
symbols ${\mathsf{c}}\succ{\mathsf{b}}\succ{\mathsf{a}}$ and the terms
$\lambda x.\>{\mathsf{b}}$ and $\lambda x.\>x$. Owing to totality, one of the
terms must be larger than the other, say, $(\lambda
x.\>{\mathsf{b}})\succ(\lambda x.\>x)$. By compatibility with arguments, we
get $(\lambda x.\>{\mathsf{b}})\>{\mathsf{c}}\succ(\lambda
x.\>x)\>{\mathsf{c}}$, i.e., ${\mathsf{b}}\succ{\mathsf{c}}$, a contradiction.
A similar line of reasoning applies if $(\lambda
x.\>{\mathsf{b}})\prec(\lambda x.\>x)$, using ${\mathsf{a}}$ instead of
${\mathsf{c}}$.

######  Definition 3.5 (Strict term order)

A _strict term order_ is a relation $\succ$ on terms, literals, and clauses
such that restriction to ground entities is a strict ground term order and
such that it is stable under grounding substitutions (i.e., $t\succ s$ implies
$t\theta\succ s\theta$ for all substitutions $\theta$ grounding the entities
$t$ and $s$).

######  Definition 3.6 (Nonstrict term order)

Given a strict term order $\succ$ and its reflexive closure $\succeq$, a
_nonstrict term order_ is a relation $\succsim$ on terms, literals, and
clauses such that $t\succsim s$ implies $t\theta\succeq s\theta$ for all
$\theta$ grounding the entities $t$ and $s$.

Although we call them orders, a strict term order $\succ$ is not required to
be transitive on nonground entities, and a nonstrict term order $\succsim$
does not need to be transitive at all. Normally, $t\succeq s$ should imply
$t\succsim s$, but this is not required either. A nonstrict term order
$\succsim$ allows us to be more precise than the reflexive closure $\succeq$
of $\succ$. For example, we cannot have $y\>{\mathsf{b}}\succeq
y\>{\mathsf{a}}$, because $y\>{\mathsf{b}}\not=y\>{\mathsf{a}}$ and
$y\>{\mathsf{b}}\not\succ y\>{\mathsf{a}}$ by stability under grounding
substitutions (with $\\{y\mapsto\lambda x.\>{\mathsf{c}}\\}$). But we can have
$y\>{\mathsf{b}}\succsim y\>{\mathsf{a}}$ if ${\mathsf{b}}\succ{\mathsf{a}}$.
In practice, the strict and the nonstrict term order should be chosen so that
they can compare as many pairs of terms as possible while being computable and
reasonably efficient.

######  Definition 3.7 (Maximality)

An element $x$ of a multiset $M$ is $\unrhd$-_maximal_ for some relation
$\unrhd$ if for all $y\in M$ with $y\unrhd x$, we have $y\unlhd x$. It is
_strictly $\unrhd$-maximal_ if it is $\unrhd$-maximal and occurs only once in
$M$.

######  Definition 3.8 (Selection function)

A _selection function_ is a function that maps each clause to a subclause
consisting of negative literals, which we call the _selected_ literals of that
clause. A literal
$L\begin{picture}(5.0,7.0)\put(1.1,2.5){\rotatebox{45.0}{\line(1,0){6.0}}}
\put(1.1,2.5){\rotatebox{315.0}{\line(1,0){6.0}}}
\end{picture}\,\,y\begin{picture}(5.0,7.0)\put(0.0,2.5){\rotatebox{135.0}{\line(1,0){6.0}}}
\put(0.0,2.5){\rotatebox{225.0}{\line(1,0){6.0}}} \end{picture}$ must not be
selected if $y\>\bar{u}_{n}$, with $n>0$, is a $\succeq$-maximal term of the
clause.

The restriction on the selection function is needed for our proof, but it is
an open question whether it is actually necessary for refutational
completeness.

Our calculus is parameterized by a strict term order $\succ$, a nonstrict term
order $\succsim$, and a selection function $\mathit{HSel}$. The calculus rules
depend on the following auxiliary notions.

######  Definition 3.9 (Eligibility)

A literal $L$ is (_strictly_) $\unrhd$-_eligible_ w.r.t. a substitution
$\sigma$ in $C$ for some relation $\unrhd$ if it is selected in $C$ or there
are no selected literals in $C$ and $L\sigma$ is (strictly) $\unrhd$-maximal
in $C\sigma.$ If $\sigma$ is the identity substitution, we leave it implicit.

######  Definition 3.10 (Deep occurrences)

A variable _occurs deeply_ in a clause $C$ if it occurs inside a
$\lambda$-expression or inside an argument of an applied variable.

For example, $x$ and $z$ occur deeply in ${\mathsf{f}}\kern
0.41672ptx\>y\approx y\>x\mathrel{\lor}z\not\approx(\lambda
w.\>z\>{\mathsf{a}})$, whereas $y$ does not occur deeply. The purpose of this
definition is to capture all variables with an occurrence that corresponds to
a position inside a $\lambda$-expression in some ground instances of $C$.

The first rule of our calculus is the superposition rule. We regard positive
and negative superposition as two cases of a single rule

$\prftree[r]{{\textsc{Sup}}}{\overbrace{D^{\prime}\mathrel{\lor}{t\approx
t^{\prime}}}^{\vphantom{\cdot}\smash{D}}\hskip
12.50002pt\overbrace{C^{\prime}\mathrel{\lor}s\begin{picture}(5.0,7.0)\put(1.1,2.5){\rotatebox{45.0}{\line(1,0){6.0}}}
\put(1.1,2.5){\rotatebox{315.0}{\line(1,0){6.0}}}
\end{picture}\,u\begin{picture}(5.0,7.0)\put(0.0,2.5){\rotatebox{135.0}{\line(1,0){6.0}}}
\put(0.0,2.5){\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,2.5){\rotatebox{45.0}{\line(1,0){6.0}}}
\put(1.1,2.5){\rotatebox{315.0}{\line(1,0){6.0}}}
\end{picture}\,t^{\prime}\begin{picture}(5.0,7.0)\put(0.0,2.5){\rotatebox{135.0}{\line(1,0){6.0}}}
\put(0.0,2.5){\rotatebox{225.0}{\line(1,0){6.0}}}
\end{picture}\mathrel{\dot{\approx}}s^{\prime})\sigma}$

where $\mathrel{\dot{\approx}}$ denotes either $\approx$ or $\not\approx$. The
following side conditions apply:

  1. 1.

$u$ is not fluid; 2. $u$ is not a variable deeply occurring in $C$;

  2. 3.

_variable condition_ : if $u$ is a variable $y$, there must exist a grounding
substitution $\theta$ such that $t\sigma\theta\succ
t^{\prime}\kern-0.83328pt\sigma\theta$ and $C\sigma\theta\prec
C^{\prime\prime}\sigma\theta$, where $C^{\prime\prime}=C\\{y\mapsto
t^{\prime}\\}$;

  3. 4.

$\sigma\in\operatorname{CSU}(t,u)$; 5. $t\sigma\not\precsim
t^{\prime}\kern-0.83328pt\sigma$; 6.
$s\begin{picture}(5.0,7.0)\put(1.1,2.5){\rotatebox{45.0}{\line(1,0){6.0}}}
\put(1.1,2.5){\rotatebox{315.0}{\line(1,0){6.0}}}
\end{picture}\,u\begin{picture}(5.0,7.0)\put(0.0,2.5){\rotatebox{135.0}{\line(1,0){6.0}}}
\put(0.0,2.5){\rotatebox{225.0}{\line(1,0){6.0}}}
\end{picture}\sigma\not\precsim s^{\prime}\sigma$; 7. $C\sigma\not\precsim
D\sigma$;

  4. 8.

$t\approx t^{\prime}$ is strictly $\succsim$-eligible in $D$ w.r.t. $\sigma$;

  5. 9.

$s\begin{picture}(5.0,7.0)\put(1.1,2.5){\rotatebox{45.0}{\line(1,0){6.0}}}
\put(1.1,2.5){\rotatebox{315.0}{\line(1,0){6.0}}}
\end{picture}\,u\begin{picture}(5.0,7.0)\put(0.0,2.5){\rotatebox{135.0}{\line(1,0){6.0}}}
\put(0.0,2.5){\rotatebox{225.0}{\line(1,0){6.0}}}
\end{picture}\mathrel{\dot{\approx}}s^{\prime}$ is $\succsim$-eligible in $C$
w.r.t. $\sigma$, and strictly $\succsim$-eligible if it is positive.

There are four main differences with the statement of the standard
superposition rule: Contexts $s[~{}]$ are replaced by green contexts
$s\begin{picture}(5.0,7.0)\put(1.1,2.5){\rotatebox{45.0}{\line(1,0){6.0}}}
\put(1.1,2.5){\rotatebox{315.0}{\line(1,0){6.0}}}
\end{picture}\,\phantom{.}\begin{picture}(5.0,7.0)\put(0.0,2.5){\rotatebox{135.0}{\line(1,0){6.0}}}
\put(0.0,2.5){\rotatebox{225.0}{\line(1,0){6.0}}} \end{picture}$. The standard
condition $u\notin\mathscr{V}$ is generalized by conditions 2 and 3. Most
general unifiers are replaced by complete sets of unifiers. And $\not\preceq$
is replaced by the more precise $\not\precsim$.

The second rule is a variant of Sup that focuses on fluid green subterms:

$\prftree[r]{{\textsc{FluidSup}}}{\overbrace{D^{\prime}\mathrel{\lor}t\approx
t^{\prime}}^{\phantom{\cdot}\smash{D}}\hskip
12.50002pt\overbrace{C^{\prime}\mathrel{\lor}s\begin{picture}(5.0,7.0)\put(1.1,2.5){\rotatebox{45.0}{\line(1,0){6.0}}}
\put(1.1,2.5){\rotatebox{315.0}{\line(1,0){6.0}}}
\end{picture}\,u\begin{picture}(5.0,7.0)\put(0.0,2.5){\rotatebox{135.0}{\line(1,0){6.0}}}
\put(0.0,2.5){\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,2.5){\rotatebox{45.0}{\line(1,0){6.0}}}
\put(1.1,2.5){\rotatebox{315.0}{\line(1,0){6.0}}}
\end{picture}\,z\>t^{\prime}\begin{picture}(5.0,7.0)\put(0.0,2.5){\rotatebox{135.0}{\line(1,0){6.0}}}
\put(0.0,2.5){\rotatebox{225.0}{\line(1,0){6.0}}}
\end{picture}\mathrel{\dot{\approx}}s^{\prime})\sigma}$

with the following side conditions, in addition to Sup’s conditions 5 to 9:

  1. 1.

$u$ is either a fluid term or a variable deeply occurring in $C$;

  2. 2.

$z$ is a fresh variable; 3. $\sigma\in\operatorname{CSU}(z\>t{,}\;u)$; 4.
$(z\>t^{\prime})\sigma\not=(z\>t)\sigma$.

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

$\displaystyle\prftree[r]{{\textsc{ERes}}}{\overbrace{C^{\prime}\mathrel{\lor}{u\not\approx
u^{\prime}}}^{C}}{C^{\prime}\sigma}$
$\displaystyle\prftree[r]{{\textsc{EFact}}}{\overbrace{C^{\prime}\mathrel{\lor}{u^{\prime}}\approx
v^{\prime}\mathrel{\lor}{u}\approx
v}^{C}}{(C^{\prime}\mathrel{\lor}v\not\approx v^{\prime}\mathrel{\lor}u\approx
v^{\prime})\sigma}$

For ERes: $\sigma\in\operatorname{CSU}(u,u^{\prime})$ and $u\not\approx
u^{\prime}$ is $\succsim$-eligible in $C$ w.r.t. $\sigma$. For EFact:
$\sigma\in\operatorname{CSU}(u,u^{\prime})$, $u\sigma\not\precsim v\sigma$,
and $u\approx v$ is $\succsim$-eligible in $C$ w.r.t. $\sigma$.

Argument congruence, a higher-order concern, is embodied by the rule

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

where $\sigma$ is the most general type substitution that ensures well-
typedness of the conclusion. In particular, if the result type of $s$ is not a
type variable, $\sigma$ is the identity substitution; and if the result type
is a type variable, it is instantiated with
$\alpha_{1}\rightarrow\cdots\rightarrow\alpha_{m}\rightarrow\beta$, where
$\bar{\alpha}_{m}$ and $\beta$ are fresh. This yields infinitely many
conclusions, one for each $m$. The literal $s\approx s^{\prime}$ must be
strictly $\succsim$-eligible in $C$ w.r.t. $\sigma$, and $\bar{x}_{n}$ is a
nonempty tuple of distinct fresh variables.

The rules are complemented by the polymorphic functional extensionality axiom:

$y\>({\mathsf{diff}}{\langle\alpha,\beta\rangle\kern-0.83328pt}\>y\>z)\not\approx
z\>({\mathsf{diff}}{\langle\alpha,\beta\rangle\kern-0.83328pt}\>y\>z)\mathrel{\lor}y\approx
z$

From now on, we will omit the type arguments to ${\mathsf{diff}}$ since they
can be inferred from the term arguments.

###  3.2 Rationale for the Rules

The calculus realizes the following division of labor: Sup and FluidSup are
responsible for green subterms, which are outside $\lambda$s, ArgCong
effectively gives access to the remaining positions outside $\lambda$s, and
the extensionality axiom takes care of subterms inside $\lambda$s.

###### Example 3.11

Prefix subterms such as ${\mathsf{g}}$ in the term
${\mathsf{g}}\>{\mathsf{a}}$ are not green subterms and thus cannot be
superposed into. ArgCong gives us access to those positions. Consider the
clauses ${\mathsf{g}}\>{\mathsf{a}}\not\approx{\mathsf{f}}\>{\mathsf{a}}$ and
${\mathsf{g}}\approx{\mathsf{f}}$. An ArgCong inference from
${\mathsf{g}}\approx{\mathsf{f}}$ generates
${\mathsf{g}}\>x\approx{\mathsf{f}}\>x$. This clause can be used for a Sup
inference into the first clause, yielding
${\mathsf{f}}\>{\mathsf{a}}\not\approx{\mathsf{f}}\>{\mathsf{a}}$ and thus
$\bot$ by ERes.

###### Example 3.12

Applied variables give rise to subtle situations with no counterparts in
first-order logic. Consider the clauses
${\mathsf{f}}\>{\mathsf{a}}\approx{\mathsf{c}}$ and
${\mathsf{h}}\>(y\>{\mathsf{b}})\>(y\>{\mathsf{a}})\not\approx{\mathsf{h}}\>({\mathsf{g}}\>({\mathsf{f}}\>{\mathsf{b}}))\>({\mathsf{g}}\>{\mathsf{c}})$,
where ${\mathsf{f}}\>{\mathsf{a}}\succ{\mathsf{c}}$. It is easy to see that
the clause set is unsatisfiable, by grounding the second clause with
$\theta=\\{y\mapsto\lambda x.\>{\mathsf{g}}\>({\mathsf{f}}\>x)\\}$. However,
to mimic the superposition inference that can be performed at the ground
level, it is necessary to superpose at an imaginary position _below_ the
applied variable $y$ and yet _above_ its argument ${\mathsf{a}}$, namely, into
the subterm ${\mathsf{f}}\>{\mathsf{a}}$ of
${\mathsf{g}}\>({\mathsf{f}}\>{\mathsf{a}})=(\lambda
x.\>{\mathsf{g}}\>({\mathsf{f}}\>x))\>{\mathsf{a}}=(y\>{\mathsf{a}})\theta$.
FluidSup’s $z$ variable effectively transforms
${\mathsf{f}}\>{\mathsf{a}}\approx{\mathsf{c}}$ into
$z\>({\mathsf{f}}\>{\mathsf{a}})\approx z\>{\mathsf{c}}$, whose left-hand side
can be unified with $y\>{\mathsf{a}}$ by taking $\\{y\mapsto\lambda
x.\>z\>({\mathsf{f}}\>x)\\}$. The resulting clause is
${\mathsf{h}}\>(z\>({\mathsf{f}}\>{\mathsf{b}}))\>(z\>{\mathsf{c}})\not\approx{\mathsf{h}}\>({\mathsf{g}}\>({\mathsf{f}}\>{\mathsf{b}}))\>({\mathsf{g}}\>{\mathsf{c}})$,
from which $\bot$ follows by ERes.

###### Example 3.13

The clause set consisting of ${\mathsf{f}}\>{\mathsf{a}}\approx{\mathsf{c}}$,
${\mathsf{f}}\>{\mathsf{b}}\approx{\mathsf{d}}$, and
${\mathsf{g}}\>{\mathsf{c}}\not\approx
y\>{\mathsf{a}}\mathrel{\lor}{\mathsf{g}}\>{\mathsf{d}}\not\approx
y\>{\mathsf{b}}$ has a similar flavor. ERes is applicable on either literal of
the third clause, but the computed unifier, $\\{y\mapsto\lambda
x.\>{\mathsf{g}}\>{\mathsf{c}}\\}$ or $\\{y\mapsto\lambda
x.\>{\mathsf{g}}\>{\mathsf{d}}\\}$, is not the right one. Again, we need
FluidSup.

###### Example 3.14

Third-order clauses containing subterms of the form $y\>(\lambda x.\>t)$ can
be even more stupefying. The clause set consisting of
${\mathsf{f}}\>{\mathsf{a}}\approx{\mathsf{c}}$ and
${\mathsf{h}}\>(y\>(\lambda
x.\>{\mathsf{g}}\>({\mathsf{f}}\>x))\>{\mathsf{a}})\>y\not\approx{\mathsf{h}}\>({\mathsf{g}}\>{\mathsf{c}})\>(\lambda
w\>x.\>w\>x)$ is unsatisfiable. To see why, apply $\theta=\\{y\mapsto\lambda
w\>x.\>w\>x\\}$ to the second clause, yielding
${\mathsf{h}}\>({\mathsf{g}}\>({\mathsf{f}}\>{\mathsf{a}}))\>(\lambda
w\>x.\>w\>x)\not\approx{\mathsf{h}}\>({\mathsf{g}}\>{\mathsf{c}})\>(\lambda
w\>x.\>w\>x)$. Let ${\mathsf{f}}\>{\mathsf{a}}\succ{\mathsf{c}}$. A Sup
inference is possible between the first clause and this ground instance of the
second one. But at the nonground level, the subterm
${\mathsf{f}}\>{\mathsf{a}}$ is not clearly localized:
${\mathsf{g}}\>({\mathsf{f}}\>{\mathsf{a}})=(\lambda
x.\>{\mathsf{g}}\>({\mathsf{f}}\>x))\>{\mathsf{a}}=(\lambda
w\>x.\>w\>x)\>(\lambda
x.\>{\mathsf{g}}\>({\mathsf{f}}\>x))\>{\mathsf{a}}=(y\>(\lambda
x.\>{\mathsf{g}}\>({\mathsf{f}}\>x))\>{\mathsf{a}})\theta$. The FluidSup rule
can cope with this. One of the unifiers of $z\>({\mathsf{f}}\>{\mathsf{a}})$
and $y\>(\lambda x.\>{\mathsf{g}}\>({\mathsf{f}}\>x))\>{\mathsf{a}}$ will be
$\\{y\mapsto\lambda w\>x.\>w\>x{,}\;z\mapsto{\mathsf{g}}\\}$, yielding the
clearly unsatisfiable clause
${\mathsf{h}}\>({\mathsf{g}}\>{\mathsf{c}})\>(\lambda
w\>x.\>w\>x)\not\approx{\mathsf{h}}\>({\mathsf{g}}\>{\mathsf{c}})\>(\lambda
w\>x.\>w\>x)$.

###### Example 3.15

The FluidSup rule is concerned not only with applied variables but also with
$\lambda$-expressions that, after substitution, may be $\eta$-reduced to
reveal new applied variables or green subterms. Consider the clauses
${\mathsf{g}}\>{\mathsf{a}}\approx{\mathsf{b}}$, ${\mathsf{h}}\>(\lambda
y.\>x\>y\>{\mathsf{g}}\>z)\approx{\mathsf{c}}$, and
${\mathsf{h}}\>({\mathsf{f}}\>{\mathsf{b}})\not\approx{\mathsf{c}}$. Applying
$\\{x\mapsto\lambda
y^{\prime}\>w\>z^{\prime}.\>{\mathsf{f}}\>(w\>{\mathsf{a}})\>y^{\prime}\\}$ to
the second clause yields ${\mathsf{h}}\>(\lambda y.\>(\lambda
y^{\prime}\>w\>z^{\prime}.\;{\mathsf{f}}\>(w\>{\mathsf{a}})\>y^{\prime})\>y\>{\mathsf{g}}\>z)\approx{\mathsf{c}}$,
which $\beta$-reduces to ${\mathsf{h}}\;(\lambda
y.\>{\mathsf{f}}\>({\mathsf{g}}\>{\mathsf{a}})\>y)\approx{\mathsf{c}}$ and
$\beta\eta$-reduces to
${\mathsf{h}}\;({\mathsf{f}}\>({\mathsf{g}}\>{\mathsf{a}}))\approx{\mathsf{c}}$.
A Sup inference is possible between the first clause and this new ground
clause, generating the clause
${\mathsf{h}}\>({\mathsf{f}}\>{\mathsf{b}})\approx{\mathsf{c}}$. By also
considering $\lambda$-expressions, the FluidSup rule is applicable at the
nonground level to derive this clause.

###### Example 3.16

Consider the clause set consisting of the facts
$C_{\text{succ}}={\mathsf{succ}}\>x\not\approx{\mathsf{zero}}$,
$C_{\text{div}}=n\approx{\mathsf{zero}}\mathrel{\lor}{\mathsf{div}}\;n\;n\approx{\mathsf{one}}$,
$C_{\text{prod}}={\mathsf{prod}}\;K\;(\lambda
k.\>{\mathsf{one}})\approx{\mathsf{one}}$, and the negated conjecture
$C_{\text{conj}}={\mathsf{prod}}\;K\;(\lambda
k.\>{\mathsf{div}}\;({\mathsf{succ}}\;k)\;({\mathsf{succ}}\;k))\not\approx{\mathsf{one}}$.
Intuitively, the term ${\mathsf{prod}}\;K\;(\lambda k.\;u)$ is intended to
denote the product $\smash{\prod_{k\in K}u}$, where $k$ ranges over a finite
set $K$ of natural numbers. The calculus derives the empty clause as follows:

$\prftree[r]{\textsc{ERes}}{\prftree[r]{\textsc{Sup}}{C_{\text{prod}}\\!}{\prftree[r]{\textsc{Sup}}{C_{\text{conj}}}{\trimbox{3.2em0pt0em0em}{{\prftree[r]{\textsc{ERes}}{\prftree[r]{\textsc{Sup}}{\prftree[r]{\textsc{ERes}}{\prftree[r]{\textsc{FluidSup}}{C_{\text{div}}}{\prftree[r]{\textsc{Ext}}{}{y\>({\mathsf{diff}}{\langle\alpha,\beta\rangle\kern-0.83328pt}\>y\>z)\not\approx
z\>({\mathsf{diff}}{\langle\alpha,\beta\rangle\kern-0.83328pt}\>y\>z)\mathrel{\lor}y\approx
z}}{\begin{aligned}
w&\>({\mathsf{diff}}{\langle\alpha,\iota\rangle\kern-0.83328pt}\>(\lambda
k.\>{\mathsf{div}}\>(w\>k)\>(w\>k))\>z)\approx{\mathsf{zero}}\\\
&\mathrel{\lor}{\mathsf{one}}\not\approx
z\>({\mathsf{diff}}{\langle\alpha,\iota\rangle\kern-0.83328pt}\>(\lambda
k.\>{\mathsf{div}}\>(w\>k)\>(w\>k))\>z)\mathrel{\lor}(\lambda
k.\>{\mathsf{div}}\>(w\>k)\>(w\>k))\approx z\end{aligned}}}{{\begin{aligned}
\\\ C_{\text{succ}}\end{aligned}}\quad\begin{aligned}
w&\>({\mathsf{diff}}{\langle\alpha,\iota\rangle\kern-0.83328pt}\>(\lambda
k.\>{\mathsf{div}}\>(w\>k)\>(w\>k))\>(\lambda
k.\>{\mathsf{one}}))\approx{\mathsf{zero}}\\\ &\mathrel{\lor}(\lambda
k.\>{\mathsf{div}}\>(w\>k)\>(w\>k))\approx(\lambda
k.\>{\mathsf{one}})\end{aligned}}}{{\mathsf{zero}}\not\approx{\mathsf{zero}}\mathrel{\lor}(\lambda
k.\>{\mathsf{div}}\>({\mathsf{succ}}\>k)\>({\mathsf{succ}}\>k))\approx(\lambda
k.\>{\mathsf{one}})}}{(\lambda
k.\>{\mathsf{div}}\>({\mathsf{succ}}\>k)\>({\mathsf{succ}}\>k))\approx(\lambda
k.\>{\mathsf{one}})}}}}{{\mathsf{prod}}\;K\;(\lambda
k.\>{\mathsf{one}})\not\approx{\mathsf{one}}}}{{\mathsf{one}}\not\approx{\mathsf{one}}}}{\bot}$

Since the calculus does not superpose into $\lambda$-expressions, we need to
use the extensionality axiom to refute this clause set. We perform a FluidSup
inference into the extensionality axiom with the unifier
$\\{\beta\mapsto\iota,\>\allowbreak z^{\prime}\mapsto\lambda
x.\>x,\>\allowbreak n\mapsto
w\>({\mathsf{diff}}{\langle\alpha,\iota\rangle\kern-0.83328pt}\>(\lambda
k.\>{\mathsf{div}}\>(w\>k)\>(w\>k))\>z),\>\allowbreak y\mapsto\lambda
k.\>{\mathsf{div}}\>(w\>k)\>(w\>k)\\}\in\operatorname{CSU}(z^{\prime}\>({\mathsf{div}}\>n\>n){,}\;y\>({\mathsf{diff}}{\langle\alpha,\beta\rangle\kern-0.83328pt}\>y\>z))$.
Then we apply ERes with the unifier $\\{z\mapsto\lambda
k.\>{\mathsf{one}}\\}\in\operatorname{CSU}({\mathsf{one}}{,}\;z\>({\mathsf{diff}}{\langle\alpha,\iota\rangle\kern-0.83328pt}\>(\lambda
k.\>{\mathsf{div}}\>(w\>k)\>(w\>k))\>z))$ to eliminate the negative literal.
Next, we perform a Sup inference into $C_{\text{succ}}$ with the unifier
$\\{\alpha\mapsto\iota,\>\allowbreak w\mapsto{\mathsf{succ}},\>\allowbreak
x\mapsto{\mathsf{diff}}{\langle\alpha,\iota\rangle\kern-0.83328pt}\>\allowbreak(\lambda
k.\>{\mathsf{div}}\>(w\>k)\>(w\>k))\>(\lambda
k.\>{\mathsf{one}})\\}\in\operatorname{CSU}(w\>({\mathsf{diff}}{\langle\alpha,\iota\rangle\kern-0.83328pt}\>(\lambda
k.\>{\mathsf{div}}\>(w\>k)\>(w\>k))\>(\lambda
k.\>{\mathsf{one}})),\allowbreak\>{\mathsf{succ}}\>x)$. To eliminate the
trivial literal, we apply ERes. We then apply a Sup inference into
$C_{\text{conj}}$ and superpose into the resulting clause with
$C_{\text{prod}}$. Finally we derive the empty clause by ERes. The unifiers in
this example were chosen to keep the clauses reasonably small.

Because it gives rise to flex–flex pairs, which are unification constraints
where both sides are variable-headed, FluidSup can be very prolific. With
variable-headed terms on both sides of its maximal literal, the extensionality
axiom is another prime source of flex–flex pairs. Flex–flex pairs can also
arise in the other rules (Sup, ERes, and EFact). Due to order restrictions and
fairness, we cannot postpone solving flex–flex pairs indefinitely. Thus, we
cannot use Huet’s pre-unification procedure huet-1975  and must instead choose
a full unification procedure such as Jensen and Pietrzykowski’s jensen-
pietrzykowski-1976 , Snyder and Gallier’s snyder-gallier-1989 , or the
procedure that has recently been developed by Vukmirović, Bentkamp, and
Nummelin vukmirovic-et-al-2020-unif . On the positive side, optional inference
rules can efficiently cover many cases where FluidSup or the extensionality
axiom would otherwise be needed (Sect. 5), and heuristics can help postpone
the explosion. Moreover, flex–flex pairs are not always as bad as their
reputation; for example,
$y\>{\mathsf{a}}\>{\mathsf{b}}\mathrel{\smash{\stackrel{{\scriptstyle\lower
0.3014pt\hbox{$\scriptscriptstyle?$}}}{{=}}}}z\>{\mathsf{c}}\>{\mathsf{d}}$
admits a most general unifier: $\\{y\mapsto\lambda
w\>x.\>y^{\prime}\,w\>x\>{\mathsf{c}}\>{\mathsf{d}}{,}\;z\mapsto
y^{\prime}\,{\mathsf{a}}\>{\mathsf{b}}\\}$.

The calculus is a graceful generalization of standard superposition, except
for the extensionality axiom. From simple first-order clauses, the axiom can
be used to derive clauses containing $\lambda$-expressions, which are useless
if the problem is first-order. For instance, the clause
${\mathsf{g}}\>x\approx{\mathsf{f}}\>x\>x$ can be used for a FluidSup
inference into the axiom (Ext) yielding the clause
$w\>t\>({\mathsf{f}}\>t\>t)\not\approx z\>t\mathrel{\lor}(\lambda
u.\>w\>u\>({\mathsf{g}}u))\approx z$ via the unifier
$\\{\alpha\mapsto\iota,\>\allowbreak\beta\mapsto\iota,\>\allowbreak x\mapsto
t,\>\allowbreak v\mapsto\lambda u.\>w\>t\>u,\>\allowbreak y\mapsto\lambda
u.\>w\>u\>({\mathsf{g}}\>u)\\}\in\operatorname{CSU}(v\>({\mathsf{g}}\>x),\>y\>({\mathsf{diff}}{\langle\alpha,\beta\rangle\kern-0.83328pt}\>y\>z))$
where $t={\mathsf{diff}}{\langle\iota,\iota\rangle\kern-0.83328pt}\>(\lambda
u.\>w\>u\>({\mathsf{g}}\>u))\>z$, the variable $w$ is freshly introduced by
unification, and $v$ is the fresh variable introduced by FluidSup (named $z$
in the definition of the rule). By ERes, with the unifier $\\{z\mapsto\lambda
u.\>w\>u\>({\mathsf{f}}\>u\>u)\\}\in\operatorname{CSU}(w\>t\>({\mathsf{f}}\>t\>t),\>z\>t)$,
we can then derive $(\lambda u.\>w\>u\>({\mathsf{g}}\>u))\approx(\lambda
u.\>w\>u\>({\mathsf{f}}\>u\>u))$, an equality of two $\lambda$-expressions,
although we started with a simple first-order clause. This could be avoided if
we could find a way to make the positive literal $y\approx z$ of (Ext) larger
than the other literal, or to select $y\approx z$ without losing refutational
completeness. The literal $y\approx z$ interacts only with green subterms of
functional type, which do not arise in first-order clauses.

###  3.3 Soundness

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

######  Lemma 3.17 (Substitution lemma)

Let $\mathscr{I}=(\mathscr{I}_{\mathsf{ty}},\mathscr{J},\mathscr{L})$ be a
proper interpretation. Then

$\smash{\llbracket\tau\rho\rrbracket_{\mathscr{I}_{\mathsf{ty}}}^{\xi}}=\smash{\llbracket\tau\rrbracket_{\mathscr{I}_{\mathsf{ty}}}^{\xi^{\prime}}}\text{\quad
and\quad}\smash{\llbracket
t\rho\rrbracket_{\mathscr{I}}^{\xi}}=\smash{\llbracket
t\rrbracket_{\mathscr{I}}^{\xi^{\prime}}}$

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

###### Proof

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

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

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

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

Next, we prove $\smash{\llbracket
t\rho\rrbracket_{\mathscr{I}}^{\xi}}=\smash{\llbracket
t\rrbracket_{\mathscr{I}}^{\xi^{\prime}}}$ by induction on the structure of a
$\lambda$-term representative of $t$, allowing arbitrary substitutions $\rho$
in the induction hypothesis. If $t=y$, then by the definition of the
denotation of a variable

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

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

$\smash{\llbracket{\mathsf{f}}{\langle\bar{\tau}\rangle\kern-0.83328pt}\rho\rrbracket_{\mathscr{I}}^{\xi}}=\mathscr{J}({\mathsf{f}},\smash{\llbracket\bar{\tau}\rho\rrbracket_{\mathscr{I}_{\mathsf{ty}}}^{\xi}})\overset{\smash{\scriptscriptstyle\text{IH}}}{=}\mathscr{J}({\mathsf{f}},\smash{\llbracket\bar{\tau}\rrbracket_{\mathscr{I}_{\mathsf{ty}}}^{\xi^{\prime}}})=\smash{\llbracket{\mathsf{f}}{\langle\bar{\tau}\rangle\kern-0.41664pt}\rrbracket_{\mathscr{I}}^{\xi^{\prime}}}$

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

$\smash{\llbracket(u\>v)\rho\rrbracket_{\mathscr{I}}^{\xi}}=\smash{\llbracket
u\rho\rrbracket_{\mathscr{I}}^{\xi}}(\smash{\llbracket
v\rho\rrbracket_{\mathscr{I}}^{\xi}})\overset{\smash{\scriptscriptstyle\text{IH}}}{=}\smash{\llbracket
u\rrbracket_{\mathscr{I}}^{\xi^{\prime}}}(\smash{\llbracket
v\rrbracket_{\mathscr{I}}^{\xi^{\prime}}})=\smash{\llbracket
u\>v\rrbracket_{\mathscr{I}}^{\xi^{\prime}}}$

If $t=\lambda z.\>u$, let $\rho^{\prime}(z)=z$ and $\rho^{\prime}(x)=\rho(x)$
for $x\neq z$. Using properness of $\mathscr{I}$ in the second and the last
step, we have

$\smash{\llbracket(\lambda
z.\>u)\rho\rrbracket_{\mathscr{I}}^{\xi}}(a)=\smash{\llbracket(\lambda
z.\>u\rho^{\prime})\rrbracket_{\mathscr{I}}^{\xi}}(a)=\smash{\llbracket
u\rho^{\prime}\rrbracket_{\mathscr{I}}^{\xi[z\mapsto
a]}}\overset{\smash{\scriptscriptstyle\text{IH}}}{=}\smash{\llbracket
u\rrbracket_{\mathscr{I}}^{\xi^{\prime}[z\mapsto a]}}=\smash{\llbracket\lambda
z.\>u\rrbracket_{\mathscr{I}}^{\xi^{\prime}}}(a)$

###### Lemma 3.18

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

###### Proof

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

######  Theorem 3.19 (Soundness)

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

###### Proof

We fix an inference and an interpretation $\mathscr{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 in our logic, at least for subterms that are not inside a
$\lambda$-expression. In particular, it holds for green subterms and for the
left subterm $t$ of an application $t\>s$.

By Lemma 3.18, $\mathscr{I}$ is a model of the $\sigma$-instances of the
premises as well, where $\sigma$ is the substitution used for the inference.
Let $\xi$ be a valuation. By making case distinctions on the truth under
$\mathscr{I},\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 true under $\mathscr{I},\xi$. Hence,
$\mathscr{I}$ is a model of the conclusion. ∎

As in the $\lambda$-free higher-order logic of Bentkamp et al. bentkamp-et-al-
lfhosup-arxiv , skolemization is unsound in our logic. As a consequence, axiom
(Ext) does not hold in all interpretations, but the axiom is consistent with
our logic, i.e., there exist models of (Ext).

###  3.4 The Redundancy Criterion

A redundant clause is usually defined as a clause whose ground instances are
entailed by smaller ($\prec$) ground instances of existing clauses. This would
be too strong for our calculus, as it would make most clauses produced by
ArgCong redundant. The solution is to base the redundancy criterion on a
weaker ground logic—ground monomorphic first-order logic—in which argument
congruence and extensionality do not hold. The resulting notion of redundancy
gracefully generalizes the standard first-order notion.

We employ an encoding $\mathcalx{F}$ to translate ground higher-order terms
into ground first-order terms. $\mathcalx{F}$ indexes each symbol occurrence
with the type arguments and the number of term arguments. For example,
$\mathcalx{F}\\!({\mathsf{f}}\>{\mathsf{a}})={\mathsf{f}}_{1}({\mathsf{a}}_{0})$
and
$\mathcalx{F}\\!({\mathsf{g}}{\langle\kappa\rangle\kern-0.83328pt})={\mathsf{g}}\kern
0.41672pt{}^{\kappa}_{0}$. In addition, $\mathcalx{F}$ conceals
$\lambda$-expressions by replacing them with fresh symbols. These measures
effectively disable argument congruence and extensionality. For example, the
clause sets
$\\{{\mathsf{g}}\approx{\mathsf{f}}{,}\;{\mathsf{g}}\>{\mathsf{a}}\not\approx{\mathsf{f}}\>{\mathsf{a}}\\}$
and $\\{{\mathsf{b}}\approx{\mathsf{a}}{,}\;(\lambda
x.\;{\mathsf{b}})\not\approx(\lambda x.\;{\mathsf{a}})\\}$ are unsatisfiable
in higher-order logic, but the encoded clause sets
$\\{{\mathsf{g}}_{0}\approx{\mathsf{f}}_{0}{,}\allowbreak\;{\mathsf{g}}_{1}({\mathsf{a}}_{0})\not\approx{\mathsf{f}}_{1}({\mathsf{a}}_{0})\\}$
and
$\\{{\mathsf{b}}_{0}\approx{\mathsf{a}}_{0}{,}\allowbreak\;{\mathsf{lam}}_{\lambda
x.\;{\mathsf{b}}}\not\approx{\mathsf{lam}}_{\lambda x.\;{\mathsf{a}}}\\}$ are
satisfiable in first-order logic, where ${\mathsf{lam}}_{\lambda x.\>t}$ is a
family of fresh symbols.

Given a higher-order signature
($\mathrm{\Sigma}_{\mathsf{ty}},\mathrm{\Sigma})$, we define a ground first-
order signature
($\mathrm{\Sigma}_{\mathsf{ty}},\allowbreak\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 ground instance
${\mathsf{f}}{\langle\bar{\upsilon}\rangle\kern-0.83328pt}:\tau_{1}\rightarrow\cdots\rightarrow\tau_{n}\rightarrow\tau$
of a symbol ${\mathsf{f}}\in\mathrm{\Sigma}$, we introduce a first-order
symbol
$\smash{{\mathsf{f}}^{\bar{\upsilon}}_{\\!j}}\in\mathrm{\Sigma}_{\mathrm{GF}}$
with argument types $\bar{\tau}_{\\!j}$ and return type
$\tau_{\\!j+1}\rightarrow\cdots\rightarrow\tau_{n}\rightarrow\tau$, for each
$j$. Moreover, for each ground term $\lambda x.\>t$, we introduce a symbol
${\mathsf{lam}}_{\lambda x.\>t}\in\mathrm{\Sigma}_{\mathrm{GF}}$ of the same
type.

Thus, we consider three levels of logics: the higher-order level
${\mathrm{H}}$ over a given signature
($\mathrm{\Sigma}_{\mathsf{ty}},\mathrm{\Sigma})$, the ground higher-order
level ${\mathrm{GH}}$, which is the ground fragment of ${\mathrm{H}}$, and the
ground monomorphic first-order level ${\mathrm{GF}}$ over the signature
($\mathrm{\Sigma}_{\mathsf{ty}},\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. 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 every model of
$N_{1}$ is also a model of $N_{2}$. For ${\mathrm{H}}$ and ${\mathrm{GH}}$, we
use higher-order models; for ${\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 (Sect. 4).

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

######  Definition 3.20 (Grounding function $\bm{{\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 3.21 (Encoding $\bm{\mathcalx{F}}$ on terms and clauses)

The encoding
$\mathcalx{F}:\mathcalx{T}_{\mathrm{GH}}\rightarrow\mathcalx{T}_{\mathrm{GF}}$
is recursively defined as

$\displaystyle\mathcalx{F}\\!(\lambda x.\>t)={\mathsf{lam}}_{\lambda x.\>t}$
$\displaystyle\mathcalx{F}\\!({\mathsf{f}}{\langle\bar{\upsilon}\rangle\kern-0.83328pt}\>\bar{s}_{\\!j})={\mathsf{f}}^{\bar{\upsilon}}_{\\!j}(\mathcalx{F}\\!(\bar{s}_{\\!j}))$

using $\eta$-short $\beta$-normal representatives of terms. 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.

Schematically, the three levels are connected as follows:

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

The mapping $\mathcalx{F}$ is clearly bijective. Using the inverse mapping,
the order $\succ$ can be transferred from $\mathcalx{T}_{\mathrm{GH}}$ to
$\mathcalx{T}_{\mathrm{GF}}$ and from $\mathcalx{C}_{\mathrm{GH}}$ to
$\mathcalx{C}_{\mathrm{GF}}$ by defining $t\succ s$ as
$\mathcalx{F}^{-1}\\!(t)\succ\mathcalx{F}^{-1}\\!(s)$ and $C\succ D$ as
$\mathcalx{F}^{-1}\\!(C)\succ\mathcalx{F}^{-1}\\!(D)$. 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.

For example, let $C=y\>{\mathsf{b}}\approx y\>{\mathsf{a}}\lor
y\not\approx{\mathsf{f}}\>{\mathsf{a}}\in\mathcalx{C}_{\mathrm{H}}$. Then
${\mathcalx{G}}(C)$ contains, among many other clauses,
$C\theta={\mathsf{f}}\>{\mathsf{b}}\>{\mathsf{b}}\approx{\mathsf{f}}\>{\mathsf{a}}\>{\mathsf{a}}\lor(\lambda
x.\>{\mathsf{f}}\>x\>x)\not\approx{\mathsf{f}}\>{\mathsf{a}}\in\mathcalx{C}_{\mathrm{GH}}$,
where $\theta=\\{y\mapsto\lambda x.\>{\mathsf{f}}\>x\>x\\}$. On the
${\mathrm{GF}}$ level, this clause corresponds to
$\mathcalx{F}\\!(C\theta)={\mathsf{f}}_{2}({\mathsf{b}}_{0},{\mathsf{b}}_{0})\approx{\mathsf{f}}_{2}({\mathsf{a}}_{0},{\mathsf{a}}_{0})\lor{\mathsf{lam}}_{\lambda
x.\>{\mathsf{f}}\>x\>x}\not\approx{\mathsf{f}}_{1}({\mathsf{a}}_{0})\in\mathcalx{C}_{\mathrm{GF}}$.

A key property of $\mathcalx{F}$ is that green subterms in
$\mathcalx{T}_{\mathrm{GH}}$ correspond to subterms in
$\mathcalx{T}_{\mathrm{GF}}$. This allows us to show that well-foundedness,
totality on ground terms, compatibility with contexts, and the subterm
property hold for $\succ$ on $\mathcalx{T}_{\mathrm{GF}}$.

###### Lemma 3.22

Let $s,t\in\mathcalx{T}_{\mathrm{GH}}$. We have
$\mathcalx{F}\\!(t\begin{picture}(5.0,7.0)\put(1.1,2.5){\rotatebox{45.0}{\line(1,0){6.0}}}
\put(1.1,2.5){\rotatebox{315.0}{\line(1,0){6.0}}}
\end{picture}\,s\begin{picture}(5.0,7.0)\put(0.0,2.5){\rotatebox{135.0}{\line(1,0){6.0}}}
\put(0.0,2.5){\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

Analogous to Lemma 3.13 of Bentkamp et al. bentkamp-et-al-lfhosup-arxiv . ∎

###### Lemma 3.23

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

###### Proof

Analogous to Lemma 3.15 of Bentkamp et al. bentkamp-et-al-lfhosup-arxiv ,
using Lemma 3.22. ∎

The saturation procedures of superposition provers aggressively delete clauses
that are strictly subsumed by other clauses. 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$.
For example, $x\approx{\mathsf{c}}$ strictly subsumes both
${\mathsf{a}}\approx{\mathsf{c}}$ and
${\mathsf{b}}\not\approx{\mathsf{a}}\mathrel{\lor}x\approx{\mathsf{c}}$. The
proof of refutational completeness of resolution and superposition provers
relies on the well-foundedness of the strict subsumption relation.
Unfortunately, this property does not hold for higher-order logic, where
${\mathsf{f}}\>x\>x\approx{\mathsf{c}}$ is strictly subsumed by
${\mathsf{f}}\>(x\>{\mathsf{a}})\>(x\>{\mathsf{b}})\approx{\mathsf{c}}$, which
is strictly subsumed by
${\mathsf{f}}\>(x\>{\mathsf{a}}\>{\mathsf{a}}^{\prime})\>(x\>{\mathsf{b}}\>{\mathsf{b}}^{\prime})\approx{\mathsf{c}}$,
and so on. To prevent such infinite chains, we use a well-founded partial
order $\sqsupset$ on $\mathcalx{C}_{\mathrm{H}}$. We can define $\sqsupset$ as
${\mathrel{\raisebox{0.8pt}{\Large\hbox to0.0pt{\kern
0.5pt$\cdot$\hss}}}\gtrsim}\mathrel{\cap}{>_{\text{size}}}$, where
$\mathrel{\raisebox{0.8pt}{\Large\hbox to0.0pt{\kern
0.5pt$\cdot$\hss}}}\gtrsim$ stands for “subsumed by” and $D>_{\text{size}}C$
if either $\mathit{size}(D)>\mathit{size}(C)$ or
$\mathit{size}(D)=\mathit{size}(C)$ and $D$ contains fewer distinct variables
than $C$; the $\mathit{size}$ function is some notion of syntactic size, such
as the number of constants and variables contained in a clause. This yields
for instance ${\mathsf{a}}\mathbin{\approx}{\mathsf{c}}\sqsupset
x\mathbin{\approx}{\mathsf{c}}$ and
${\mathsf{f}}\>(x\>{\mathsf{a}}\>{\mathsf{a}})\mathbin{\approx}{\mathsf{c}}\sqsupset{\mathsf{f}}\>(y\>{\mathsf{a}})\mathbin{\approx}{\mathsf{c}}$.
To justify the deletion of subsumed clauses, we set up our redundancy
criterion to cover subsumption, following Waldmann et al. waldmann-et-
al-2020-saturation .

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})$.

For example,
$({\mathsf{h}}\>{\mathsf{g}})\>x\approx({\mathsf{h}}\>{\mathsf{f}})\>x$ is
redundant w.r.t. ${\mathsf{g}}\approx{\mathsf{f}}$, but
${\mathsf{g}}\>x\approx{\mathsf{f}}\>x$ and $(\lambda
x.\>{\mathsf{g}})\approx(\lambda x.\>{\mathsf{f}})$ are not, because
$\mathcalx{F}$ translates an unapplied ${\mathsf{g}}$ to ${\mathsf{g}}_{0}$,
whereas an applied ${\mathsf{g}}$ is translated to ${\mathsf{g}}_{1}$ and the
expression $\lambda x.\>{\mathsf{g}}$ is translated to
${\mathsf{lam}}_{\lambda x.\>{\mathsf{g}}}$. These different translations
prevent entailment on the ${\mathrm{GF}}$ level. For an example of
subsumption, we assume that
${\mathsf{a}}\mathbin{\approx}{\mathsf{c}}\sqsupset
x\mathbin{\approx}{\mathsf{c}}$ holds, for instance using the above definition
of $\sqsupset$. Then ${\mathsf{a}}\mathbin{\approx}{\mathsf{c}}$ is redundant
w.r.t. $x\mathbin{\approx}{\mathsf{c}}$.

Along with the three levels of logics, we consider three inference systems:
$\mathit{HInf}$, $\mathit{GHInf}$, and $\mathit{GFInf}$. $\mathit{HInf}$ is
the inference system described in Sect. 3.1. For uniformity, we regard the
extensionality axiom as a premise-free inference rule Ext whose conclusion is
axiom (Ext). The rules of $\mathit{GHInf}$ include Sup, ERes, and EFact from
$\mathit{HInf}$, but with the restriction that premises and conclusion are
ground and with all references to $\succsim$ replaced by $\succeq$. In
addition, $\mathit{GHInf}$ contains a premise-free rule GExt whose infinitely
many conclusions are the ground instances of (Ext), and the following ground
variant of ArgCong:

$\prftree[r]{{\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 $\succeq$-eligible in
$C^{\prime}\mathrel{\lor}s\approx s^{\prime}$ 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 with standard
first-order superposition.

Each of the three inference systems is parameterized by a selection function.
For $\mathit{HInf}$, we globally fix one selection function $\mathit{HSel}$.
For $\mathit{GHInf}$ and $\mathit{GFInf}$, we need to consider different
selection functions. 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 $\mathit{GHSel}$ and
$\mathit{GFSel}$ 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})$.

We extend the functions $\mathcalx{F}$ and ${\mathcalx{G}}$ to inferences:

###### Notation 3.24

Given an inference $\iota$, we write $\mathit{prems}(\iota)$ for the tuple of
premises, $\mathit{mprem}(\iota)$ for the main (i.e., rightmost) premise, and
$\mathit{concl}(\iota)$ for the conclusion.

######  Definition 3.25 (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 3.26 (Grounding function ${\mathcalx{G}}$ on inferences)

Given an inference $\iota\in\mathit{HInf}$, and a selection function
$\mathit{GHSel}\in{\mathcalx{G}}(\mathit{HSel})$, 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{concl}(\iota)\theta$ for some
grounding substitution $\theta$.

This will map Sup and FluidSup 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

    * –

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

  * –

Given $\iota\in\mathit{HInf}$ and $N\subseteq\mathcalx{C}_{\mathrm{H}}$, let
$\iota\in\mathit{HRed}_{\mathrm{I}}(N)$ if
${\mathcalx{G}}^{\mathit{GHSel}}(\iota)\subseteq\mathit{GHRed}_{\mathrm{I}}({\mathcalx{G}}(N))$
for all $\mathit{GHSel}\in{\mathcalx{G}}(\mathit{HSel})$.

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 the
inference component $\mathit{Red}_{\mathrm{I}}$ of a redundancy criterion if
every inference from clauses in $N$ is in $\mathit{Red}_{\mathrm{I}}(N).$

###  3.5 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 (schulz-2002-brainiac, , 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
$u\begin{picture}(5.0,7.0)\put(1.1,2.5){\rotatebox{45.0}{\line(1,0){6.0}}}
\put(1.1,2.5){\rotatebox{315.0}{\line(1,0){6.0}}}
\end{picture}\,\phantom{.}\begin{picture}(5.0,7.0)\put(0.0,2.5){\rotatebox{135.0}{\line(1,0){6.0}}}
\put(0.0,2.5){\rotatebox{225.0}{\line(1,0){6.0}}} \end{picture}$ instead of
arbitrary contexts $u[\phantom{.}]$. 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.

###  3.6 A Derived Term Order

We stated some requirements on the term orders $\succ$ and $\succsim$ in Sect.
3.1 but have not shown how to fulfill them. To derive a suitable strict term
order $\succ$, we propose to encode $\eta$-short $\beta$-normal forms into
untyped first-order terms and apply an order
$\succ_{\kern-0.5833pt{\mathsf{fo}}}$ of first-order terms such as the
Knuth–Bendix order knuth-bendix-1970  or the lexicographic path order kamin-
levy-1980-cannotfind .

The encoding, denoted by $\mathcalx{\kern-0.41672ptO}$, indexes symbols with
their number of term arguments, similarly to the $\mathcalx{F}$ encoding.
Unlike the $\mathcalx{F}$ encoding, $\mathcalx{\kern-0.41672ptO}$ translates
$\lambda x\mathbin{:}\nobreak\tau.\;t$ to
${\mathsf{lam}}(\mathcalx{\kern-0.41672ptO}(\tau),\mathcalx{\kern-0.41672ptO}(t))$
and uses De Bruijn de-bruijn-1972  symbols to represent bound variables. The
$\mathcalx{\kern-0.41672ptO}$ encoding replaces fluid terms $t$ by fresh
variables $z_{\kern 0.2917ptt}$ and maps type arguments to term arguments,
while erasing any other type information. For example,
$\mathcalx{\kern-0.41672ptO}(\lambda
x\mathbin{:}\kappa.\>{\mathsf{f}}\>({\mathsf{f}}\>({\mathsf{a}}{\langle\kappa\rangle\kern-0.83328pt}))\>(y\>{\mathsf{b}}))={\mathsf{lam}}(\kappa,{\mathsf{f}}_{2}({\mathsf{f}}_{1}({\mathsf{a}}_{0}(\kappa)),z_{\kern
0.2917pty\kern 0.2917pt{\mathsf{b}}}))$. The use of De Bruijn indices and the
monolithic encoding of fluid terms ensure stability under both
$\alpha$-renaming and substitution.

######  Definition 3.27 (Encoding $\bm{\mathcalx{\kern-0.41672ptO}}$)

Given a signature
$(\mathrm{\Sigma}_{\mathsf{ty}},\allowbreak\mathrm{\Sigma})$,
$\mathcalx{\kern-0.41672ptO}$ encodes types and terms as terms over the
untyped first-order signature
$\mathrm{\Sigma}_{\mathsf{ty}}\uplus\\{{\mathsf{f}}_{k}\mid{\mathsf{f}}\in\mathrm{\Sigma},\>k\in\nobreak\mathbb{N}\\}\uplus\\{{\mathsf{lam}}\\}\uplus\\{\smash{{\mathsf{db}}^{i}_{k}}\mid
i,k\in\nobreak\mathbb{N}\\}$. We reuse higher-order type variables as term
variables in the target untyped first-order logic. Moreover, let $z_{\kern
0.2917ptt}$ be an untyped first-order variable for each higher-order term $t$.
The auxiliary function $\mathcalx{B}_{x}(t)$ replaces each free occurrence of
the variable $x$ by a symbol ${\mathsf{db}}^{i}$, where $i$ is the number of
$\lambda$-expressions surrounding the variable occurrence. The type-to-term
version of $\mathcalx{\kern-0.41672ptO}$ is defined by
$\mathcalx{\kern-0.41672ptO}(\alpha)=\alpha$ and
$\mathcalx{\kern-0.41672ptO}(\kappa(\bar{\tau}))=\kappa(\mathcalx{\kern-0.41672ptO}(\bar{\tau}))$.
The term-to-term version is defined by

$\mathcalx{\kern-0.41672ptO}(t)=\begin{cases}z_{\kern 0.2917ptt}&\text{if
$t=x$ or $t$ is fluid}\\\
{\mathsf{lam}}(\mathcalx{\kern-0.41672ptO}(\tau),\mathcalx{\kern-0.41672ptO}(\mathcalx{B}_{x}(u)))&\text{if
$t=(\lambda x\mathbin{:}\tau.\;u)$ and $t$ is not fluid}\\\
{\mathsf{f}}_{k}(\mathcalx{\kern-0.41672ptO}(\bar{\tau}),\mathcalx{\kern-0.41672ptO}(\bar{u}_{k}))&\text{if
$t={\mathsf{f}}{\langle\bar{\tau}\rangle\kern-0.83328pt}\>\bar{u}_{k}$}\end{cases}$

For example, let $s=\lambda y.\>{\mathsf{f}}\>y\>(\lambda
w.\>{\mathsf{g}}\>(y\>w))$ where $y$ has type $\kappa\rightarrow\kappa$ and
$w$ has type $\kappa$. We have $\mathcalx{B}_{y}({\mathsf{f}}\>y\>(\lambda
w.\>{\mathsf{g}}\>(y\>w)))={\mathsf{f}}\>{\mathsf{db}}^{0}(\lambda
w.\>{\mathsf{g}}\>({\mathsf{db}}^{1}\>w))$ and
$\mathcalx{B}_{w}({\mathsf{g}}\>({\mathsf{db}}^{1}\>w))={\mathsf{g}}\>({\mathsf{db}}^{1}\>{\mathsf{db}}^{0})$.
Neither $s$ nor $\lambda w.\>{\mathsf{g}}\>(y\>w)$ are fluid. Hence, we have
$\mathcalx{\kern-0.41672ptO}(s)={\mathsf{lam}}({\rightarrow}(\kappa,\kappa),\allowbreak{\mathsf{f}}_{2}({\mathsf{db}}^{0}_{0},{\mathsf{lam}}(\kappa,{\mathsf{g}}_{1}({\mathsf{db}}^{1}_{1}({\mathsf{db}}^{0}_{0}))))$.

######  Definition 3.28 (Derived strict term order)

Let the strict term order derived from $\succ_{\kern-0.5833pt{\mathsf{fo}}}$
be $\succ_{\kern-0.5833pt{\lambda}}$ where $t\succ_{\kern-0.5833pt{\lambda}}s$
if
$\mathcalx{\kern-0.41672ptO}(t)\succ_{\kern-0.5833pt{\mathsf{fo}}}\mathcalx{\kern-0.41672ptO}(s)$.

We will show that the derived $\succ_{\kern-0.5833pt{\lambda}}$ fulfills all
properties of a strict term order (Definition 3.5) if
$\succ_{\kern-0.5833pt{\mathsf{fo}}}$ fulfills the corresponding properties on
first-order terms. For the nonstrict term order $\succsim$, we can use the
reflexive closure $\succeq_{{\lambda}}$ of $\succ_{\kern-0.5833pt{\lambda}}$.

###### Lemma 3.29

Let $\succ_{\kern-0.5833pt{\mathsf{fo}}}$ be a strict partial order on first-
order terms and $\succ_{\kern-0.5833pt{\lambda}}$ the derived term order on
$\beta\eta$-equivalence classes. If the restriction of
$\succ_{\kern-0.5833pt{\mathsf{fo}}}$ to ground terms enjoys well-foundedness,
totality, the subterm property, and compatibility with contexts (w.r.t. first-
order terms), the restriction of $\succ_{\kern-0.5833pt{\lambda}}$ to ground
terms enjoys well-foundedness, totality, the green subterm property, and
compatibility with green contexts (w.r.t. $\beta\eta$-equivalence classes).

###### Proof

Transitivity and irreflexivity of $\succ_{\kern-0.5833pt{\mathsf{fo}}}$ imply
transitivity and irreflexivity of $\succ_{\kern-0.5833pt{\lambda}}$.

Well-foundedness: If there existed an infinite chain
$t_{1}\succ_{\kern-0.5833pt{\lambda}}t_{2}\succ_{\kern-0.5833pt{\lambda}}\cdots$
of ground terms, there would also be the chain
$\mathcalx{\kern-0.41672ptO}(t_{1})\succ_{\kern-0.5833pt{\mathsf{fo}}}\mathcalx{\kern-0.41672ptO}(t_{2})\succ_{\kern-0.5833pt{\mathsf{fo}}}\cdots$,
contradicting the well-foundedness of $\succ_{\kern-0.5833pt{\mathsf{fo}}}$ on
ground $\lambda$-free terms.

Totality: By ground totality of $\succ_{\kern-0.5833pt{\mathsf{fo}}}$, for any
ground terms $t$ and $s$ we have
$\mathcalx{\kern-0.41672ptO}(t)\succ_{\kern-0.5833pt{\mathsf{fo}}}\mathcalx{\kern-0.41672ptO}(s)$,
$\mathcalx{\kern-0.41672ptO}(t)\prec_{\mathsf{fo}}\mathcalx{\kern-0.41672ptO}(s)$,
or $\mathcalx{\kern-0.41672ptO}(t)=\mathcalx{\kern-0.41672ptO}(s)$. In the
first two cases, it follows that $t\succ_{\kern-0.5833pt{\lambda}}s$ or
$t\prec_{\lambda}s$. In the last case, it follows that $t=s$ because
$\mathcalx{\kern-0.41672ptO}$ is clearly injective.

Green subterm property: Let $s$ be a term. We show that
$s\succeq_{{\lambda}}s|_{p}$ by induction on $p$, where $s|_{p}$ denotes the
green subterm at position $p$. If $p=\varepsilon$, this is trivial. If
$p=p^{\prime}.i$, we have $s\succeq_{{\lambda}}s|_{p^{\prime}}$ by the
induction hypothesis. Hence, it suffices to show that
$s|_{p^{\prime}}\succeq_{{\lambda}}s|_{p^{\prime}.i}$. From the existence of
the position $p^{\prime}.i$, we know that $s|_{p^{\prime}}$ must be of the
form
$s|_{p^{\prime}}={\mathsf{f}}{\langle\bar{\tau}\rangle\kern-0.83328pt}\>\bar{u}_{k}$.
Then $s|_{p^{\prime}.i}=u_{i}$. The encoding yields
$\mathcalx{\kern-0.41672ptO}(s|_{p^{\prime}})={\mathsf{f}}_{k}(\mathcalx{\kern-0.41672ptO}(\bar{\tau}),\mathcalx{\kern-0.41672ptO}(\bar{u}_{k}))$
and hence
$\mathcalx{\kern-0.41672ptO}(s|_{p^{\prime}})\succeq_{\kern-0.2917pt{\mathsf{fo}}}\mathcalx{\kern-0.41672ptO}(s|_{p^{\prime}.i})$
by the ground subterm property of $\succ_{\kern-0.5833pt{\mathsf{fo}}}$.
Hence, $s|_{p^{\prime}}\succeq_{{\lambda}}s|_{p^{\prime}.i}$ and thus
$s\succeq_{{\lambda}}s|_{p}$.

Compatibility with green contexts: By induction on the depth of the context,
it suffices to show that $t\succ_{\kern-0.5833pt{\lambda}}s$ implies
${\mathsf{f}}{\langle\bar{\tau}\rangle\kern-0.83328pt}\>\bar{u}\>t\>\bar{v}\succ_{\kern-0.5833pt{\lambda}}{\mathsf{f}}{\langle\bar{\tau}\rangle\kern-0.83328pt}\>\bar{u}\>s\>\bar{v}$
for all $t$, $s$, ${\mathsf{f}}$, $\bar{\tau}$, $\bar{u}$, and $\bar{v}$. This
amounts to showing that
$\mathcalx{\kern-0.41672ptO}(t)\succ_{\kern-0.5833pt{\mathsf{fo}}}\mathcalx{\kern-0.41672ptO}(s)$
implies
$\mathcalx{\kern-0.41672ptO}({\mathsf{f}}{\langle\bar{\tau}\rangle\kern-0.83328pt}\>\bar{u}\>t\>\bar{v})={\mathsf{f}}_{k}(\mathcalx{\kern-0.41672ptO}(\bar{\tau}),\mathcalx{\kern-0.41672ptO}(\bar{u}),\mathcalx{\kern-0.41672ptO}(t),\mathcalx{\kern-0.41672ptO}(\bar{v}))\succ_{\kern-0.5833pt{\mathsf{fo}}}{\mathsf{f}}_{k}(\mathcalx{\kern-0.41672ptO}(\bar{\tau}),\mathcalx{\kern-0.41672ptO}(\bar{u}),\mathcalx{\kern-0.41672ptO}(s),\mathcalx{\kern-0.41672ptO}(\bar{v}))=\mathcalx{\kern-0.41672ptO}({\mathsf{f}}{\langle\bar{\tau}\rangle\kern-0.83328pt}\>\bar{u}\>s\>\bar{v})$,
which follows directly from ground compatibility of
$\succ_{\kern-0.5833pt{\mathsf{fo}}}$ with contexts and the induction
hypothesis. ∎

###### Lemma 3.30

Let $\succ_{\kern-0.5833pt{\mathsf{fo}}}$ be a strict partial order on first-
order terms. If $\succ_{\kern-0.5833pt{\mathsf{fo}}}$ is stable under
grounding substitutions (w.r.t. first-order terms), the derived term order
$\succ_{\kern-0.5833pt{\lambda}}$ is stable under grounding substitutions
(w.r.t. $\beta\eta$-equivalence classes).

###### Proof

Assume $s\succ_{\kern-0.5833pt{\lambda}}s^{\prime}$ for some terms $s$ and
$s^{\prime}$. Let $\theta$ be a higher-order substitution grounding $s$ and
$s^{\prime}$. We must show
$s\theta\succ_{\kern-0.5833pt{\lambda}}s^{\prime}\theta$. We will define a
first-order substitution $\rho$ grounding $\mathcalx{\kern-0.41672ptO}(s)$ and
$\mathcalx{\kern-0.41672ptO}(s^{\prime})$ such that
$\mathcalx{\kern-0.41672ptO}(s)\rho=\mathcalx{\kern-0.41672ptO}(s\theta)$ and
$\mathcalx{\kern-0.41672ptO}(s^{\prime})\rho=\mathcalx{\kern-0.41672ptO}(s^{\prime}\theta)$.
Since $s\succ_{\kern-0.5833pt{\lambda}}s^{\prime}$, we have
$\mathcalx{\kern-0.41672ptO}(s)\succ_{\kern-0.5833pt{\mathsf{fo}}}\mathcalx{\kern-0.41672ptO}(s^{\prime})$.
By stability of $\succ_{\kern-0.5833pt{\mathsf{fo}}}$ under grounding
substitutions,
$\mathcalx{\kern-0.41672ptO}(s)\rho\succ_{\kern-0.5833pt{\mathsf{fo}}}\mathcalx{\kern-0.41672ptO}(s^{\prime})\rho$.
It follows that
$\mathcalx{\kern-0.41672ptO}(s\theta)\succ_{\kern-0.5833pt{\mathsf{fo}}}\mathcalx{\kern-0.41672ptO}(s^{\prime}\theta)$
and hence $s\theta\succ_{\kern-0.5833pt{\lambda}}s^{\prime}\theta$.

We define the first-order substitution $\rho$ as $\alpha\rho=\alpha\theta$ for
type variables $\alpha$ and $z_{\kern
0.2917ptu}\rho=\mathcalx{\kern-0.41672ptO}(u\theta)$ for terms $u$. Strictly
speaking, the domain of a substitution must be finite, so we restrict this
definition of $\rho$ to the finitely many variables that occur in the
computation of $\mathcalx{\kern-0.41672ptO}(s)$ and
$\mathcalx{\kern-0.41672ptO}(s^{\prime})$.

Clearly
$\mathcalx{\kern-0.41672ptO}(\tau)\rho=\mathcalx{\kern-0.41672ptO}(\tau\theta)$
for all types $\tau$ occurring in the computation of
$\mathcalx{\kern-0.41672ptO}(s)$ and
$\mathcalx{\kern-0.41672ptO}(s^{\prime})$. Moreover,
$\mathcalx{\kern-0.41672ptO}(t)\rho=\mathcalx{\kern-0.41672ptO}(t\theta)$ for
all $t$ occurring in the computation of $\mathcalx{\kern-0.41672ptO}(s)$ and
$\mathcalx{\kern-0.41672ptO}(s^{\prime})$, which we show by induction on the
definition of the encoding. If $t=x$ or if $t$ is fluid,
$\mathcalx{\kern-0.41672ptO}(t)\rho=z_{\kern
0.2917ptt}\rho=\mathcalx{\kern-0.41672ptO}(t\theta)$. If
$t={\mathsf{f}}{\langle\bar{\tau}\rangle\kern-0.83328pt}\>\bar{u}$, then
$\mathcalx{\kern-0.41672ptO}(t)\rho={\mathsf{f}}_{k}(\mathcalx{\kern-0.41672ptO}(\bar{\tau})\rho,\mathcalx{\kern-0.41672ptO}(\bar{u})\rho)\overset{\smash{\scriptscriptstyle\text{IH}}}{=}{\mathsf{f}}_{k}(\mathcalx{\kern-0.20836ptO}(\bar{\tau}\theta),\mathcalx{\kern-0.20836ptO}(\bar{u}\theta))=\mathcalx{\kern-0.20836ptO}({\mathsf{f}}{\langle\bar{\tau}\theta\rangle\kern-0.41664pt}\>(\bar{u}\theta))=\mathcalx{\kern-0.20836ptO}(t\theta)$.
If $t=(\lambda x\mathbin{:}\tau.\;u)$ and $t$ is not fluid, then
$\mathcalx{\kern-0.41672ptO}(t)\rho={\mathsf{lam}}(\mathcalx{\kern-0.41672ptO}(\tau)\rho,\allowbreak\mathcalx{\kern-0.41672ptO}(\mathcalx{B}_{x}(u))\rho)\overset{\smash{\scriptscriptstyle\text{IH}}}{=}{\mathsf{lam}}(\mathcalx{\kern-0.20836ptO}(\tau\theta),\allowbreak\mathcalx{\kern-0.20836ptO}(\mathcalx{B}_{x}(u)\theta))={\mathsf{lam}}(\mathcalx{\kern-0.20836ptO}(\tau\theta),\allowbreak\mathcalx{\kern-0.20836ptO}(\mathcalx{B}_{x}(u)\theta[x\mapsto
x]))=\mathcalx{\kern-0.20836ptO}(\lambda
x\mathbin{:}\tau\theta.\;u\theta[x\mapsto
x])=\mathcalx{\kern-0.20836ptO}((\lambda
x\mathbin{:}\tau.\;u)\theta)=\mathcalx{\kern-0.20836ptO}(t\theta)$. ∎

Starting with a $\lambda$-free higher-order term order
$\succ_{\kern-0.5833pt{\mathsf{fo}}}$, we can also derive a relation
$\succsim_{\kern 0.2917pt{\lambda}}$ which, unlike the reflexive closure
$\succeq_{{\lambda}}$ of $\succ_{\kern-0.5833pt{\lambda}}$, is precise enough
to orient pairs of terms such as $y\>{\mathsf{b}}\succsim_{\kern
0.2917pt{\lambda}}y\>{\mathsf{a}}$. The idea is that if
${\mathsf{b}}\succsim_{\kern 0.2917pt{\lambda}}{\mathsf{a}}$ and their type is
neither functional nor a type variable (which could be instantiated by a
functional type), then ${\mathsf{b}}$ and ${\mathsf{a}}$ will appear unapplied
in $(y\>{\mathsf{b}})\theta$ and $(y\>{\mathsf{a}})\theta$, as green subterms,
regardless of $\theta$. Intuitively, in higher-order logic, $y\>{\mathsf{b}}$
can be construed as an arbitrary term with zero or more occurrences of
${\mathsf{b}}$, and $y\>{\mathsf{a}}$ is the same term but with zero or more
occurrences of ${\mathsf{a}}$ instead.

Like $\succ_{\kern-0.5833pt{\lambda}}$, the relation $\succsim_{\kern
0.2917pt{\lambda}}$ is defined via an encoding: $t\succsim_{\kern
0.2917pt{\lambda}}s$ if and only if
$\mathcalx{\kern-0.41672ptO}(t)\succeq_{\kern-0.2917pt{\mathsf{fo}}}\mathcalx{\kern-0.41672ptO}_{\kern
0.2917ptt}(s)$. In turn, $\mathcalx{\kern-0.41672ptO}_{\kern
0.2917ptt}(s)=\encZsub{\mathcalx{B}_{XXX}(t)}{\mathcalx{B}_{XXX}(s)}$, where
$\mathcalx{B}$ encodes the bound variables as above and

$\encZsub{t}{s}=\begin{cases}z_{\kern 0.2917pty\kern 0.2917pt\bar{t}}&\text{if
$t=y\>\bar{t}_{n}$, $s=y\>\bar{s}_{n}$, and each $(t_{i},s_{i})$ satisfies
($*$) below}\\\ {\mathsf{lam}}\>\encZ{\tau}\>\encZsub{v}{u}&\text{if
$t=(\lambda x\mathbin{:}\tau.\;v)$, $s=(\lambda x\mathbin{:}\tau.\>u)$, and
$t$ and $s$ are not fluid}\\\
{\mathsf{f}}\>\encZ{\bar{\tau}}\>\bar{u}^{\prime}_{n}&\text{if
$t={\mathsf{f}}{\langle\bar{\tau}\rangle\kern-0.83328pt}\>\bar{v}_{n}$,
$s={\mathsf{f}}{\langle\bar{\tau}\rangle\kern-0.83328pt}\>\bar{u}_{n}$, and
$u^{\prime}_{i}=\encZsub{v_{i}}{u_{i}}$ for all $i$}\\\
\encZ{s}&\text{otherwise}\end{cases}$

The condition ($*$) on $(t_{i},s_{i})$ is that (1) $t_{i}\succsim_{\kern
0.2917pt{\lambda}}s_{i}$ and $t_{i}$’s type is neither functional nor a type
variable or (2) $t_{i}=s_{i}$. Notice the (well-founded) mutual dependency
between $\succsim_{\kern 0.2917pt{\lambda}}$ and $\encZsubonly{t}$.

The difference between $\mathcalx{\kern-0.41672ptO}_{\kern 0.2917ptt}$ and
$\mathcalx{\kern-0.41672ptO}$, and hence between $\succsim_{\kern
0.2917pt{\lambda}}$ and $\succeq_{{\lambda}}$, concerns applied variables. If
the subterm $y\>{\mathsf{b}}$ occurs in $t$ where $s$ has $y\>{\mathsf{a}}$,
and it can be determined that ${\mathsf{b}}\succsim_{\kern
0.2917pt{\lambda}}{\mathsf{a}}$, we proceed as if $y\>{\mathsf{a}}$ had been
$y\>{\mathsf{b}}$, using the same variable $z_{\kern 0.2917pty\kern
0.2917pt{\mathsf{b}}}$ to represent both $y\>{\mathsf{b}}$ and
$y\>{\mathsf{a}}$. For example, we have
${\mathsf{g}}\>(y\>{\mathsf{b}}\>{\mathsf{f}})\succsim_{\kern
0.2917pt{\lambda}}{\mathsf{g}}\>(y\>{\mathsf{a}}\>{\mathsf{f}})$ and
${\mathsf{h}}\>{\mathsf{b}}\>(y\>{\mathsf{b}})\succsim_{\kern
0.2917pt{\lambda}}{\mathsf{h}}\>{\mathsf{a}}\>(y\>{\mathsf{a}})$ because

$\begin{array}[]{r@{}c@{}r@{\>}c@{\>}l@{}c@{}l}\mathcalx{\kern-0.41672ptO}({\mathsf{g}}\>(y\>{\mathsf{b}}\>{\mathsf{f}}))&{}={}&{\mathsf{g}}\>z_{\kern
0.2917pty\kern 0.2917pt{\mathsf{b}}\kern
0.2917pt{\mathsf{f}}}&=&{\mathsf{g}}\>z_{\kern 0.2917pty\kern
0.2917pt{\mathsf{b}}\kern
0.2917pt{\mathsf{f}}}&{}={}&\mathcalx{\kern-0.41672ptO}_{\kern
0.2917pt{\mathsf{g}}\kern 0.2917pt(y\kern 0.2917pt{\mathsf{b}}\kern
0.2917pt{\mathsf{f}})}({\mathsf{g}}\>(y\>{\mathsf{a}}\>{\mathsf{f}}))\\\
\mathcalx{\kern-0.41672ptO}({\mathsf{h}}\>{\mathsf{b}}\>(y\>{\mathsf{b}}))&{}={}&{\mathsf{h}}\>{\mathsf{b}}\>z_{\kern
0.2917pty\kern
0.2917pt{\mathsf{b}}}&{}\succ_{\kern-0.5833pt{\mathsf{fo}}}\kern-0.83328pt{}&{\mathsf{h}}\>{\mathsf{a}}\>z_{\kern
0.2917pty\kern 0.2917pt{\mathsf{b}}}&{}={}&\mathcalx{\kern-0.41672ptO}_{\kern
0.2917pt{\mathsf{h}}\kern 0.2917pt{\mathsf{b}}\kern 0.2917pt(y\kern
0.2917pt{\mathsf{b}})}({\mathsf{h}}\>{\mathsf{a}}\>(y\>{\mathsf{a}}))\end{array}$

On the other hand,
${\mathsf{g}}\>(y\>{\mathsf{b}}\>{\mathsf{f}})\not\succeq_{{\lambda}}{\mathsf{g}}\>(y\>{\mathsf{a}}\>{\mathsf{f}})$
and
${\mathsf{h}}\>{\mathsf{b}}\>(y\>{\mathsf{b}})\not\succeq_{{\lambda}}{\mathsf{h}}\>{\mathsf{a}}\>(y\>{\mathsf{a}})$.

###### Lemma 3.31

Let $\succ_{\kern-0.5833pt{\mathsf{fo}}}$ be a strict partial order on
$\lambda$-free terms that is stable under grounding substitutions and whose
ground restriction is compatible with green contexts. If $t\succsim_{\kern
0.2917pt{\lambda}}s$, then $t\theta\succeq_{{\lambda}}s\theta$ for all
grounding substitutions $\theta$.

###### Proof

By induction on $t$. Let $\rho$ be the grounding substitution based on
$\theta$ and $\\{t,s\\}$ defined in the proof of Lemma 3.30. From the
hypothesis $t\succsim_{\kern 0.2917pt{\lambda}}s$ (i.e.,
$\mathcalx{\kern-0.41672ptO}(t)\succeq_{\kern-0.2917pt{\mathsf{fo}}}\mathcalx{\kern-0.41672ptO}_{\kern
0.2917ptt}(s)$), we have
$\mathcalx{\kern-0.41672ptO}(t)\rho\succeq_{\kern-0.2917pt{\mathsf{fo}}}\mathcalx{\kern-0.41672ptO}_{\kern
0.2917ptt}(s)\rho$ by stability of $\succ_{\kern-0.5833pt{\mathsf{fo}}}$ under
grounding substitutions. The crux is to show that
$\mathcalx{\kern-0.41672ptO}_{\kern
0.2917ptt}(s)\rho\succeq_{\kern-0.2917pt{\mathsf{fo}}}\mathcalx{\kern-0.41672ptO}(s)\rho$.
The rest follows easily: From
$\mathcalx{\kern-0.41672ptO}(t)\rho\succeq_{\kern-0.2917pt{\mathsf{fo}}}\mathcalx{\kern-0.41672ptO}_{\kern
0.2917ptt}(s)\rho\succeq_{\kern-0.2917pt{\mathsf{fo}}}\mathcalx{\kern-0.41672ptO}(s)\rho$,
$\mathcalx{\kern-0.41672ptO}(t\theta)\succeq_{\kern-0.2917pt{\mathsf{fo}}}\mathcalx{\kern-0.41672ptO}(s\theta)$
follows by construction of $\rho$, and thus
$t\theta\succeq_{{\lambda}}s\theta$ by injectivity of
$\mathcalx{\kern-0.41672ptO}$.

We show $\mathcalx{\kern-0.41672ptO}_{\kern
0.2917ptt}(s)\rho\succeq_{\kern-0.2917pt{\mathsf{fo}}}\mathcalx{\kern-0.41672ptO}(s)\rho$
by exploiting ground compatibility of $\succ_{\kern-0.5833pt{\mathsf{fo}}}$
with green contexts. The difference between
$\mathcalx{\kern-0.41672ptO}_{\kern 0.2917ptt}(s)$ and
$\mathcalx{\kern-0.41672ptO}(s)$ is that the former may have $z_{\kern
0.2917pty\kern 0.2917pt\bar{t}}$ where the latter has $z_{\kern 0.2917pty\kern
0.2917pt\bar{s}}$. We call each such pair $(t_{i},s_{i})$ with
$t_{i}\not=s_{i}$ a _mismatch_.

After applying $\rho$, the terms $\mathcalx{\kern-0.41672ptO}_{\kern
0.2917ptt}(s)\rho$ and $\mathcalx{\kern-0.41672ptO}(s)\rho$ have the form
$u[t^{\prime}_{1},\ldots,t^{\prime}_{n}]$ and
$u[s^{\prime}_{1},\ldots,s^{\prime}_{n}]$, respectively, where the holes in
$u[\phantom{i}]$ correspond to positions at or below variables $z_{\kern
0.2917pty\kern 0.2917pt\bar{t}}$ in $\mathcalx{\kern-0.41672ptO}_{\kern
0.2917ptt}(s)$ and, in parallel, $z_{\kern 0.2917pty\kern 0.2917pt\bar{s}}$ in
$\mathcalx{\kern-0.41672ptO}(s)$. Clearly, each pair
$(t^{\prime}_{\\!j},s^{\prime}_{\\!j})$ must be equal to a pair
$(\mathcalx{\kern-0.41672ptO}(t_{i}\theta),\allowbreak\mathcalx{\kern-0.41672ptO}(s_{i}\theta))$
of argument tuples of some applied variable. By ($*$), all mismatches are of
nonfunctional, nonvariable types, and this property is preserved by $\theta$
and $\mathcalx{\kern-0.41672ptO}$. Hence, all the holes in $u[\phantom{i}]$
are located at green positions.

For each $i$, we have $t_{i}\succsim_{\kern 0.2917pt{\lambda}}s_{i}$ by ($*$)
and hence $t_{i}\theta\succeq_{{\lambda}}s_{i}\theta$ by the induction
hypothesis. Thus,
$t^{\prime}_{\\!j}\succeq_{\kern-0.2917pt{\mathsf{fo}}}s^{\prime}_{\\!j}$ for
all $j$. Using these inequalities in turn together with ground compatibility
with green contexts, we form the following transitive chain, thereby resolving
the crux:

∎
$\underbrace{u\begin{picture}(5.0,7.0)\put(1.1,2.5){\rotatebox{45.0}{\line(1,0){6.0}}}
\put(1.1,2.5){\rotatebox{315.0}{\line(1,0){6.0}}}
\end{picture}\,t^{\prime}_{1},\ldots,t^{\prime}_{n}\begin{picture}(5.0,7.0)\put(0.0,2.5){\rotatebox{135.0}{\line(1,0){6.0}}}
\put(0.0,2.5){\rotatebox{225.0}{\line(1,0){6.0}}}
\end{picture}}_{\mathcalx{\kern-0.2917ptO}_{\kern
0.20836ptt}(s)\rho}\>\succeq_{\kern-0.2917pt{\mathsf{fo}}}\>u\begin{picture}(5.0,7.0)\put(1.1,2.5){\rotatebox{45.0}{\line(1,0){6.0}}}
\put(1.1,2.5){\rotatebox{315.0}{\line(1,0){6.0}}}
\end{picture}\,s^{\prime}_{1},t^{\prime}_{2},\ldots,t^{\prime}_{n}\begin{picture}(5.0,7.0)\put(0.0,2.5){\rotatebox{135.0}{\line(1,0){6.0}}}
\put(0.0,2.5){\rotatebox{225.0}{\line(1,0){6.0}}}
\end{picture}\>\succeq_{\kern-0.2917pt{\mathsf{fo}}}\,\cdots\,\succeq_{\kern-0.2917pt{\mathsf{fo}}}\>u\begin{picture}(5.0,7.0)\put(1.1,2.5){\rotatebox{45.0}{\line(1,0){6.0}}}
\put(1.1,2.5){\rotatebox{315.0}{\line(1,0){6.0}}}
\end{picture}\,s^{\prime}_{1},\ldots,s^{\prime}_{n-1},t^{\prime}_{n}\begin{picture}(5.0,7.0)\put(0.0,2.5){\rotatebox{135.0}{\line(1,0){6.0}}}
\put(0.0,2.5){\rotatebox{225.0}{\line(1,0){6.0}}}
\end{picture}\>\succeq_{\kern-0.2917pt{\mathsf{fo}}}\>\underbrace{u\begin{picture}(5.0,7.0)\put(1.1,2.5){\rotatebox{45.0}{\line(1,0){6.0}}}
\put(1.1,2.5){\rotatebox{315.0}{\line(1,0){6.0}}}
\end{picture}\,s^{\prime}_{1},\ldots,s^{\prime}_{n}\begin{picture}(5.0,7.0)\put(0.0,2.5){\rotatebox{135.0}{\line(1,0){6.0}}}
\put(0.0,2.5){\rotatebox{225.0}{\line(1,0){6.0}}}
\end{picture}}_{\mathcalx{\kern-0.2917ptO}(s)\rho}$ ∎

##  4 Refutational Completeness

Besides soundness, the most important property of the Boolean-free
$\lambda$-superposition calculus introduced in Sect. 3 is refutational
completeness. We will prove 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 4.1 (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 _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 4.2 (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 a _derivation_ if $N_{i}\setminus
N_{i+1}\subseteq\mathit{Red}_{\mathrm{C}}(N_{i+1})$ for all $i$. It is _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 _dynamically refutationally complete_ w.r.t.
$(\mathit{Red}_{\mathrm{I}},\mathit{Red}_{\mathrm{C}})$ if for every fair
derivation $(N_{i})_{i}$ such that $N_{0}\models\bot$, we have $\bot\in N_{i}$
for some $i$.

###  4.1 Outline of the Proof

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

  1. 1.

We use Bachmair and Ganzinger’s work on the refutational completeness of
standard (first-order) superposition bachmair-ganzinger-1994  to prove static
refutational completeness of $\mathit{GFInf}$.

  2. 2.

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

  3. 3.

We use the saturation framework by Waldmann et al. waldmann-et-
al-2020-saturation  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 can make use of Bachmair and Ganzinger’s results.
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 first step deals exclusively
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 the first step to derive a clausal higher-
order interpretation that is a model of $N$. Under the encoding
$\mathcalx{F}$, occurrences of the same symbol with different numbers of
arguments are regarded as different symbols—e.g.,
$\mathcalx{F}\\!({\mathsf{f}})={\mathsf{f}}_{0}$ and
$\mathcalx{F}\\!({\mathsf{f}}\>{\mathsf{a}})={\mathsf{f}}_{1}({\mathsf{a}}_{0})$.
All $\lambda$-expressions $\lambda x.\>t$ are regarded as uninterpreted
symbols ${\mathsf{lam}}_{\lambda x.\>t}$. The difficulty is to construct a
higher-order interpretation that merges the first-order denotations of all
${\mathsf{f}}_{i}$ into a single higher-order denotation of ${\mathsf{f}}$ and
to show that the symbols ${\mathsf{lam}}_{\lambda x.\>t}$ behave like $\lambda
x.\>t$. This step relies on saturation w.r.t. the GArgCong rule—which connects
a term of functional type with its value when applied to an argument $x$—and
on the presence of the extensionality rule GExt.

In the third step, we employ the saturation framework by Waldmann et al.
waldmann-et-al-2020-saturation , which is based on Bachmair and Ganzinger’s
framework (bachmair-ganzinger-2001-resolution, , Sect. 4), to prove
refutational completeness of $\mathit{HInf}$. Both saturation frameworks help
calculus designers prove static and dynamic refutational completeness of
nonground calculi. In addition, the framework by Waldmann et al. explicitly
supports the redundancy criterion defined in Sect. 3.4, which can be used to
justify the deletion of subsumed clauses. Moreover, their saturation framework
provides completeness theorems for prover architectures, such as the DISCOUNT
loop.

The main proof obligation we must discharge to use the framework is that there
should exist nonground inferences in $\mathit{HInf}$ corresponding to all
nonredundant inferences in $\mathit{GHInf}$. We face two specifically higher-
order difficulties. First, in standard superposition, 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 higher-order
variables $x$ that occur applied in $C$, because the order lacks compatibility
with arguments. This is why our Sup rule must perform some inferences into
variables. The other difficulty also concerns applied variables. We must show
that any nonredundant Sup inference in level ${\mathrm{GH}}$ into a position
corresponding to a fluid term or a deeply occurring variable in level
${\mathrm{H}}$ can be lifted to a FluidSup inference. This involves showing
that the $z$ variable in FluidSup can represent arbitrary contexts around a
term $t$.

For the entire proof of refutational completeness, $\beta\eta$-normalization
is the proverbial dog that did not bark. On level ${\mathrm{GH}}$, the rules
Sup, ERes, and EFact preserve $\eta$-short $\beta$-normal form, and so does
first-order term rewriting. Thus, we can completely ignore
$\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}}_{\beta}$
and
$\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}}_{\eta}$.
On level ${\mathrm{H}}$, instantiation can cause $\beta$\- and
$\eta$-reduction, but this poses no difficulties thanks to the clause order’s
stability under grounding substitutions.

###  4.2 The Ground First-Order Level

We use Bachmair and Ganzinger’s results on standard superposition bachmair-
ganzinger-1994  to prove refutational completeness of ${\mathrm{GF}}$. In the
subsequent steps, we will also make use of specific properties of the model
Bachmair and Ganzinger construct. 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 $\mathscr{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}^{\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:

###### Definition 4.3

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. (a)

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

  2. (b)

$s\approx t$ is $\succsim$-maximal in $C$;

  3. (c)

$s\succ t$;

  4. (d)

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

  5. (e)

$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}.$

Based on Bachmair and Ganzinger’s work, Bentkamp et al. (bentkamp-et-al-
lfhosup-arxiv, , Lemma 4.2 and Theorem 4.3) prove the following properties of
$R_{N}$:

###### Lemma 4.4

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 $\succeq$-eligible in $C$ and $C^{\prime}$ is
false in $R_{N}$.

######  Theorem 4.5 (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$.

###  4.3 The Ground Higher-Order Level

In this subsection, let $\mathit{GHSel}$ be a selection function on
$\mathcalx{C}_{\mathrm{GH}}$, let $N\subseteq\mathcalx{C}_{\mathrm{GH}}$ be a
clause set saturated w.r.t. $\mathit{GHInf}^{\mathit{GHSel}}$ and
$\mathit{GHRed}_{\mathrm{I}}^{\mathit{GHSel}}$ such that $\bot\not\in N$.
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$. Given two terms
$s,t\in\mathcalx{T}_{\mathrm{GH}}$, we write $s\sim t$ to abbreviate
$R\models\mathcalx{F}\\!(s)\approx\mathcalx{F}\\!(t)$, which is equivalent to
$\smash{\llbracket\mathcalx{F}\\!(s)\rrbracket_{R}}=\smash{\llbracket\mathcalx{F}\\!(t)\rrbracket_{R}}$.

###### Lemma 4.6

For all terms $t,s:\tau\rightarrow\upsilon$ in $\mathcalx{T}_{\mathrm{GH}}$,
the following statements are equivalent:

  1. 1.

$t\sim s$;

  2. 2.

$t\>({\mathsf{diff}}\>t\>s)\sim s\>({\mathsf{diff}}\>t\>s)$;

  3. 3.

$t\>u\sim s\>u$ for all $u\in\mathcalx{T}_{\mathrm{GH}}$.

###### Proof

(3) $\Rightarrow$ (2): Take $u:={\mathsf{diff}}\>t\>s$.

(2) $\Rightarrow$ (1): Since $N$ is saturated, the GExt inference that
generates the clause $C=t\>({\mathsf{diff}}\>t\>s)\not\approx
s\>({\mathsf{diff}}\>t\>s)\mathrel{\lor}t\approx s$ is redundant—i.e., $C\in
N\mathrel{\cup}\mathit{GHRed}_{\mathrm{C}}(N)$—and hence
$R\models\mathcalx{F}\\!(C)$ by Theorem 4.5 and the assumption that
$\bot\not\in N$. Therefore, it follows from $t\>({\mathsf{diff}}\>t\>s)\sim
s\>({\mathsf{diff}}\>t\>s)$ that $t\sim s$.

(1) $\Rightarrow$ (3): We assume that $t\sim s$—i.e.,
$\mathcalx{F}\\!(t)\mathrel{\leftarrow\kern-7.25482pt\rightarrow}^{*}_{R}\mathcalx{F}\\!(s)$.
By induction on the number of rewrite steps between $\mathcalx{F}\\!(t)$ and
$\mathcalx{F}\\!(s)$ and by transitivity of $\sim$, it suffices to show that
$\mathcalx{F}\\!(t)\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}\\!(s)$
implies $t\>u\sim s\>u$. If the rewrite step
$\mathcalx{F}\\!(t)\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}\\!(s)$
is not at the top level, then neither $s\kern
0.83328pt{\downarrow}_{\beta\eta}$ nor $t\kern
0.83328pt{\downarrow}_{\beta\eta}$ can be $\lambda$-expressions. Therefore,
$(s\kern 0.83328pt{\downarrow}_{\beta\eta})\>(u\kern
0.83328pt{\downarrow}_{\beta\eta})$ and $(t\kern
0.83328pt{\downarrow}_{\beta\eta})\>(u\kern
0.83328pt{\downarrow}_{\beta\eta})$ are in $\eta$-short $\beta$-normal form,
and there is an analogous rewrite step
$\mathcalx{F}\\!(t\>u)\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}\\!(s\>u)$
using the same rewrite rule. It follows that $t\>u\sim s\>u$. If the rewrite
step
$\mathcalx{F}\\!(t)\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}\\!(s)$
is at the top level,
$\mathcalx{F}\\!(t)\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}\\!(s)$
must be a rule of $R$. This rule must originate from a productive clause of
the form $\mathcalx{F}\\!(C)=\mathcalx{F}\\!(C^{\prime}\mathrel{\lor}t\approx
s)$. By Lemma 4.4, $\mathcalx{F}\\!(t\approx s)$ is strictly
$\succeq$-eligible in $\mathcalx{F}\\!(C)$ w.r.t.
$\mathcalx{F}\\!(\mathit{GHSel})$, and hence $t\approx s$ is strictly
$\succeq$-eligible in $C$ w.r.t. $\mathit{GHSel}$. Thus, the following
GArgCong inference $\iota$ is applicable:

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

By saturation, $\iota$ is redundant w.r.t. $N$—i.e., $\mathit{concl}(\iota)\in
N\mathrel{\cup}\mathit{GHRed}_{\mathrm{C}}(N)$. By Theorem 4.5 and the
assumption that $\bot\not\in N$, $\mathcalx{F}\\!(\mathit{concl}(\iota))$ is
then true in $R$. By Lemma 4.4, $\mathcalx{F}\\!(C^{\prime})$ is false in $R$.
Therefore, $\mathcalx{F}\\!(t\>u\approx s\>u)$ must be true in $R$. ∎

###### Lemma 4.7

Let $s\in\mathcalx{T}_{\mathrm{H}}$ and $\theta$, $\theta^{\prime}$ grounding
substitutions such that $x\theta\sim x\theta^{\prime}$ for all variables $x$
and $\alpha\theta=\alpha\theta^{\prime}$ for all type variables $\alpha$. Then
$s\theta\sim s\theta^{\prime}$.

###### Proof

In this proof, we work directly on $\lambda$-terms. To prove the lemma, it
suffices to prove it for any $\lambda$-term $s$. Here, for $\lambda$-terms
$t_{1}$ and $t_{2}$, the notation $t_{1}\sim t_{2}$ is to be read as
$t_{1}\kern 0.83328pt{\downarrow}_{\beta\eta}\sim{t_{2}}\kern
0.83328pt{\downarrow}_{\beta\eta}$ because $\mathcalx{F}$ is only defined on
$\eta$-short $\beta$-normal terms.

Definition We extend the syntax of $\lambda$-terms with a new polymorphic
function symbol
$\oplus:\mathsf{\Pi}\alpha.\;\alpha\rightarrow\alpha\rightarrow\alpha$. We
will omit its type argument. It is equipped with two reduction rules:
$\oplus\>t\>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$
and
$\oplus\>t\>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}}s$.
A _$\beta\oplus$ -reduction step_ is either a rewrite step following one of
these rules or a $\beta$-reduction step.

The computability path order $\succ_{\mathsf{CPO}}$ blanqui-et-al-2015
guarantees that

  * –

$\oplus\>t\>s\succ_{\mathsf{CPO}}s$ by applying rule $@\rhd$;

  * –

$\oplus\>t\>s\succ_{\mathsf{CPO}}t$ by applying rule $@\rhd$ twice;

  * –

$(\lambda x.\>t)\>s\succ_{\mathsf{CPO}}t[x\mapsto s]$ by applying rule
$@\beta$.

Since this order is moreover monotone, it decreases with
$\beta\oplus$-reduction steps. The order is also well founded; thus,
$\beta\oplus$-reductions terminate. And since the $\beta\oplus$-reduction
steps describe a finitely branching term rewriting system, by Kőnig’s lemma
koenigs-lemma-1927 , there is a maximal number of $\beta\oplus$-reduction
steps from each $\lambda$-term.

Definition A $\lambda$-term is _term-ground_ if it does not contain free term
variables. It may contain polymorphic type arguments.

Definition We introduce an auxiliary function $\mathscr{S}$ that essentially
measures the size of a $\lambda$-term but assigns a size of $1$ to term-ground
$\lambda$-terms.

$\mathscr{S}(s)=\begin{cases}1&\text{if $s$ is term-ground or is a bound or
free variable or a symbol}\\\ 1+\mathscr{S}(t)&\text{if $s$ is not term-ground
and has the form $\lambda x.\>t$}\\\ \mathscr{S}(t)+\mathscr{S}(u)&\text{if
$s$ is not term-ground and has the form $t\>u$}\end{cases}$

We prove $s\theta\sim s\theta^{\prime}$ by well-founded induction on $s$,
$\theta$, and $\theta^{\prime}$ using the left-to-right lexicographic order on
the triple $\bigl{(}n_{1}(s),n_{2}(s),n_{3}(s)\bigr{)}\in\mathbb{N}^{3}$,
where

  * –

$n_{1}(s)$ is the maximal number of $\beta\oplus$-reduction steps starting
from $s\sigma$, where $\sigma$ is the substitution mapping each term variable
$x$ to $\oplus\>x\theta\>x\theta^{\prime}$;

  * –

$n_{2}(s)$ is the number of free term variables occurring more than once in
$s$;

  * –

$n_{3}(s)=\mathscr{S}(s)$.

Case 1: The $\lambda$-term $s$ is term-ground. Then the lemma is trivial.

Case 2: The $\lambda$-term $s$ contains $k\geq 2$ free term variables. Then we
can apply the induction hypothesis twice and use the transitivity of $\sim$ as
follows. Let $x$ be one of the free term variables in $s$. Let
$\rho=\\{x\mapsto x\theta\\}$ the substitution that maps $x$ to $x\theta$ and
ignores all other variables. Let $\rho^{\prime}=\theta^{\prime}[x\mapsto x]$.

We want to invoke the induction hypothesis on $s\rho$ and $s\rho^{\prime}$.
This is justified because $s\sigma$ $\oplus$-reduces to $s\rho\sigma$ and to
$s\rho^{\prime}\sigma$. These $\oplus$-reductions have at least one step
because $x$ occurs in $s$ and $k\geq 2$. Hence, $n_{1}(s)>n_{1}(s\rho)$ and
$n_{1}(s)>n_{1}(s\rho^{\prime})$.

This application of the induction hypothesis gives us $s\rho\theta\sim
s\rho\theta^{\prime}$ and $s\rho^{\prime}\theta\sim
s\rho^{\prime}\theta^{\prime}$. Since $s\rho\theta=s\theta$ and
$s\rho^{\prime}\theta^{\prime}=s\theta^{\prime}$, this is equivalent to
$s\theta\sim s\rho\theta^{\prime}$ and $s\rho^{\prime}\theta\sim
s\theta^{\prime}$. Since moreover $s\rho\theta^{\prime}=s\rho^{\prime}\theta$,
we have $s\theta\sim s\theta^{\prime}$ by transitivity of $\sim$. The
following illustration visualizes the above argument:

${s\rho}$${s\rho^{\prime}}$${s\theta}$${\underset{\scriptscriptstyle\text{IH}}{\sim}}$${s\rho\theta^{\prime}}$${=}$${s\rho^{\prime}\theta}$${\underset{\scriptscriptstyle\text{IH}}{\sim}}$${s\theta^{\prime}}$$\theta$
$\theta^{\prime}$$\theta$ $\theta^{\prime}$

Case 3: The $\lambda$-term $s$ contains a free term variable that occurs more
than once. Then we rename variable occurrences apart by replacing each
occurrence of each free term variable $x$ by a fresh variable $x_{i}$, for
which we define $x_{i}\theta=x\theta$ and
$x_{i}\theta^{\prime}=x\theta^{\prime}$. Let $s^{\prime}$ be the resulting
$\lambda$-term. Since $s\sigma=s^{\prime}\sigma$, we have
$n_{1}(s)=n_{1}(s^{\prime})$. All free term variables occur only once in
$s^{\prime}$. Hence, $n_{2}(s)>0=n_{2}(s^{\prime})$. Therefore, we can invoke
the induction hypothesis on $s^{\prime}$ to obtain $s^{\prime}\theta\sim
s^{\prime}\theta^{\prime}$. Since $s\theta=s^{\prime}\theta$ and
$s\theta^{\prime}=s^{\prime}\theta^{\prime}$, it follows that $s\theta\sim
s\theta^{\prime}$.

Case 4: The $\lambda$-term $s$ contains only one free term variable $x$, which
occurs exactly once.

Case 4.1: The $\lambda$-term $s$ is of the form
${\mathsf{f}}{\langle\bar{\tau}\rangle\kern-0.83328pt}\>\bar{t}$ for some
symbol ${\mathsf{f}}$, some types $\bar{\tau}$, and some $\lambda$-terms
$\bar{t}$. Then let $u$ be the $\lambda$-term in $\bar{t}$ that contains $x$.
We want to apply the induction hypothesis to $u$, which can be justified as
follows. Consider the longest sequence of $\beta\oplus$-reductions from
$u\sigma$. This sequence can be replicated inside
$s\sigma=({\mathsf{f}}{\langle\bar{\tau}\rangle\kern-0.83328pt}\>\bar{t})\sigma$.
Therefore, the longest sequence of $\beta\oplus$-reductions from $s\sigma$ is