# AdvSV: An Over-the-Air Adversarial Attack Dataset
for Speaker Verification

###### Abstract

It is known that deep neural networks are vulnerable to adversarial attacks.
Although Automatic Speaker Verification (ASV) built on top of deep neural
networks exhibits robust performance in controlled scenarios, many studies
confirm that ASV is vulnerable to adversarial attacks. The lack of a standard
dataset is a bottleneck for further research, especially reproducible
research. In this study, we developed an open-source adversarial attack
dataset for speaker verification research. As an initial step, we focused on
the over-the-air attack. An over-the-air adversarial attack involves a
perturbation generation algorithm, a loudspeaker, a microphone, and an
acoustic environment. The variations in the recording configurations make it
very challenging to reproduce previous research. The AdvSV dataset is
constructed using the Voxceleb1 Verification test set as its foundation. This
dataset employs representative ASV models subjected to adversarial attacks and
records adversarial samples to simulate over-the-air attack settings. The
scope of the dataset can be easily extended to include more types of
adversarial attacks. The dataset will be released to the public under the CC-
BY license. In addition, we also provide a detection baseline for reproducible
research.

Index Terms—  Adversarial attack, over-the-air attack, automatic speaker
verification, benchmark dataset

##  1 Introduction

An Automatic Speaker Verification (ASV) system is to decide whether a claimed
identify is an impostor or a genuine speaker by comparing a presented
utterance against an enrolled voice. Although deep learning has significantly
enhanced the performance of ASV [1], it is known that ASV is vulnerable to
impersonation, replay, voice conversion, and speech synthesis as discussed in
[2]. It is also known that deep neural networks are vulnerable to adversarial
attacks [3]. An adversarial attack is an attack on deep learning by adding a
perturbation. ASV systems built on top of deep neural networks are no
exception.

There are two types of adversarial attacks in the context of ASV, namely
digital and over-the-air (OTA) adversarial attacks. A digital attack is to
send a digital copy of an adversarial sample directly to an ASV system, and an
OTA adversarial attack is to play a pre-generated adversarial sample in front
of an ASV system. This process involves a loudspeaker, a microphone and
acoustic environment or conditions (e.g. room reverberation and background
noise). To perform attacks, the projected gradient descent (PGD) [4] algorithm
is commonly used to generate perturbations, and it was initially used in image
classification. It has since been modified to attack ASV systems digitally.
For instance, FoolHD [5] employs a multi-objective loss function to generate
adversarial samples that are hard for humans to perceive. FakeBob [6]
introduces a threshold estimation algorithm, combined with gradient
estimation, to achieve black-box attacks. Zuo et al. [7] propose a speaker-
specific utterance ensemble method to enhance the generalization of
adversarial attack samples.

Several studies have focused on OTA adversarial attacks.Xie et al. [8] use
room impulse response to simulate room reverberation, increasing success rates
of OTA adversarial attacks, employing the VCTK corpus. O’Reilly et al.[9]
transform bonafide samples into adversarial ones with adaptive filtering using
the VoxCeleb2 dataset. With a combination of Common Voice, CommanderSong [10]
and LibriSpeech datasets, Zheng et al. [11] treats decision-only black-box
adversarial attacks as a discontinuous large-scale global optimization
problem, adaptively decomposing it into subproblems and collaboratively
optimizing each one to find a solution. Both digital and OTA adversarial
studies confirm security concerns. However, each study develops their dataset
with a specific setting.

Various studies have addressed ASV system security concerns with
countermeasures against adversarial attacks [12, 13, 14, 15, 16]. Adversarial-
aware training approaches have been proposed in [17, 18, 19] to enhance the
ASV model’s resilience to attacks. An x-vector-based attack signature has been
proposed in [20] to detect adversarial perturbations. A diffusion-based
approach has been proposed in [15] to remove perturbations for discrimination.
In these studies, the VoxCeleb1, VoxCeleb2, Speech Commands, TIMIT,
ASVspoof2019, and Librispeech datasets are used. Each individual study
constructs its dataset for countermeasure research. Without a benchmark
dataset, it is not feasible to perform benchmark comparisons, making
reproducible research even more challenging.

Although there is a growing concern about the threat of adversarial attacks,
the lack of a benchmark dataset is a bottleneck for further research,
especially reproducible research. Existing studies on adversarial attacks and
countermeasures develop their own datasets, usually for specific purposes. To
promote reproducible research, this work presents an open-source dataset on
adversarial attacks for speaker verification (AdvSV). OTA adversarial attacks
involve a loudspeaker, a microphone, and acoustic environment or conditions
(e.g. room reverberation and background noise). Due to the potential
variations of OTA configurations, it is more challenging to conduct
reproducible research. Hence, the AdvSV dataset is designed to serve that
purpose. The focus of this study is over-the-air adversarial attacks, and the
scope of the dataset can be easily extended to include more types of
adversarial attacks. The AdvSV dataset will be released to the public under
the CC-BY license111https://creativecommons.org/about/cclicenses/.

##  2 Over-the-air Adversarial Attack Dataset

This section presents a framework for producing the proposed AdvSV dataset. In
this study, we focus on the over-the-air target attack, which modifies a
sample to attack a specific target speaker’s verification model. Fig. 1
presents an illustration of the over-the-air (OTA) adversarial attack, which
consists of two steps: perturbation generation and OTA attack. Both steps will
be described in this section.

Fig. 1: Illustration of an over-the-air adversarial attack, consisting of (a)
perturbation generation and (b) over-the-air attack steps.

###  2.1 Perturbation generation

To synthesize adversarial samples, this study employs the project gradient
descent (PGD) [4] algorithm. The PGD algorithm is to add a perturbation to a
testing sample, aiming to manipulate the ASV decision. The adversarial sample
synthesis process is formulated in Eq. 1,

$x_{t+1}=\prod_{x+S}\left(x_{t}+\alpha\cdot\operatorname{sign}\left(\nabla_{x}J\left(x_{t},x_{enroll},y\right)\right)\right.,$
(1)

where $x_{enroll}$ is an enrollment sample, $x_{t}$ is an adversarial sample
at the t-th iteration, $y$ stands for a label (i.e. genuine or impostor),
$\alpha$ is the step size, $S$ is the number of steps, $J$ signifies the loss
function, and $sign$ is the sign function. When we apply the PGD algorithm, we
assume the algorithm knows everything about the model including model
architecture and parameters.

Algorithm 1 Ensemble PGD Attack

1:Victim models $\\{M_{1},M_{2},\ldots,M_{n}\\}$, enrollment sample
$x_{enroll}$

2:Adversarial sample $\mathbf{x}_{\text{adv}}$

3:function EnsemblePGD($\mathbf{x}$)

4: Initialize $\mathbf{x}_{\text{adv}}\leftarrow\mathbf{x}$

5: repeat

6: for $i\leftarrow 1$ to $n$ do

7: Compute adversarial sample of

8: $M_{i}$: $x_{adv}\leftarrow PGD(x_{enroll},x_{adv},y)$

9: end for

10: until Adversarial sample attacks all surrogate models

11: return $x_{adv}$

12:end function

The PGD algorithm presented in Eq. 1 is to attack a single target ASV model.
Different from the PGD algorithm, an ensemble PGD algorithm is to attack a few
ASV systems at the same time [21]. The algorithm is presented in algorithm 1.
The idea of the ensemble PGD algorithm is to iteratively attack each victim
model until the adversarial sample can spoof all the victim ASV models [21].

Both PGD and ensemble PGD algorithms require access to the victim model’s
parameters for gradient calculations. In practice, obtaining all the
information about the target ASV model is not feasible. A practical way to
perform a transfer attack is to synthesize an adversarial sample using one or
a few known victim models and then use that adversarial sample to attack the
target ASV system.

Implementation details: The PGD Attack is configured with a step size
($\alpha$) of 0.004, 20 steps ($S$), and uses cosine similarity as the loss
function. For the Ensemble PGD Attack, three ASV models are used as victim
models, while the remaining one serves as a test for transfer attacks.

###  2.2 Over-the-air attack setup

An OTA adversarial attack involves a perturbation generation algorithm, a
loudspeaker, a microphone, and a replaying environment. In this work, we
simulated the OTA adversarial attack in a soundproof studio to reduce the
impact of environmental noise and focus the dataset on the impact of
perturbation generation, loudspeakers, and microphones. These three variables
already result in a significant number of combinations.

We chose three types of loudspeakers and three types of recording devices
(i.e., microphones). The high-end, medium-end, and low-end loudspeakers are
priced at around $300 USD, $90 USD, and $50 USD, respectively. For the
recording devices, we chose mobile devices, which are common in our daily
lives. The iOS, Android-high, and Android-low devices are priced at around
$900 USD, $750 USD, and $310 USD, respectively.

The distance and angle between the microphone and loudspeaker are other
factors. In this study, we simplified this factor. The distance between the
loudspeaker and microphone is set to 0.3 meters, and the angle is set to 90
degrees.

###  2.3 Dataset

To align with existing ASV research, we design the AdvSV dataset based on the
Voxceleb1222https://www.robots.ox.ac.uk/ vgg/data/voxceleb/vox1.html dataset.
The Voxceleb1 dataset is one of the most commonly-used dataset for speaker
verification. We choose the Voxceleb1 verification set as the base set to
generate adversarial samples. This set comprises 18,860 samples labeled with
different speakers333Voxceleb1 verification test list:
https://www.robots.ox.ac.uk/ vgg/data/
voxceleb/meta/veri_test.txt.

To reduce the burden of replay and recording, 25% of the samples were retained
(with the same speaker distribution). The proposed AdvSV dataset consists of a
total of 314,496 samples444314,496 = 4368 x 4 victim models(section 4.1) x 2
attack methods x 3 replay devices x 3 recording devices. Audio demo available
on the webpage 555AdvSV dataset demo: https://advsv.github.io/.

##  3 Detection of Adversarial Attacks

Fig. 2: Framework of the baseline system to detect adversarial attacks. ‘-’
means subtracting re-synthesized spectrogram from the original spectrogram.

In this paper, we provide a countermeasure baseline based on the one-class
classification method [22], which is currently the mainstream approach for
audio spoofing detection. Its pipeline is shown in Fig. 2. During the training
phase, we use the World 666https://github.com/JeremyCCHsu/Python-Wrapper-for-
World-Vocoder vocoder and Opus Codec 777https://opus-codec.org/ to re-
synthesize the input audio, and subtract the re-synthesized audio from the
input audio to remove irrelevant information for spoofing detection, such as
speaker and speech content information. The subtracted audio is then fed into
a one-class classifier. The world vocoder is used during the inference phase.

##  4 Experiment

Table 1: Performance of ASV systems used as victim models in study. The
performance is measured with Equal Error Rates (EER).

Abbr. Model EER (Vox1 Full) EER (Vox1 25%) ECAPA ECAPATDNN[23] 1.26% 1.26%
RawNet RawNet3[1] 1.06% 1.17% ResNet ResNetSE34V2[24] 1.03% 0.92% XVec
XVector[25] 2.08% 2.04%

Table 2: Attack Success Rates (%) of Various Attacks. S represents the
surrogate model, and V represents the victim model.

Attack S V RawNet ECAPA ResNet XVec PGD RawNet 98.9 10.6 8.8 14.1 ECAPA 54.9
100 43.5 62.5 ResNet 25.1 38.0 100 46.7 XVec 34.2 49.1 38.4 100 Ensemble PGD
w/o RawNet 86.0 100 100 100 w/o ECAPA 100 62.3 100 100 w/o ResNet 100 100 62.5
100 w/o XVec 100 100 100 79.5

Table 3: Success rate(%) of over-the-air adversarial attacks. Light gray areas
represent PGD white-box attacks, and dark gray areas represent ensemble
transfer attacks (i.e. blackbox attacks).

Surrogate Victim RawNet ECAPA ResNet XVec Attack Speaker Mic iOS Android
Android iOS Android Android iOS Android Android iOS Android Android Method
High Low High Low High Low High Low PGD RawNet High 31.9 18.5 26.6 9.2 8.5 9.0
8.3 8.1 8.0 12.2 11.8 11.3 Medium 27.1 18.0 23.1 9.5 9.2 8.4 8.3 8.0 7.9 12.2
11.8 10.1 Low 20.6 17.2 20.5 7.9 8.2 7.5 7.5 7.4 8.1 10.3 10.8 7.4 ECAPA High
52.6 39.8 46.6 100 100 100 41.3 40.5 39.0 56.9 53.3 47.6 Medium 49.8 39.7 44.0
100 100 99.9 41.0 41.2 38.0 56.7 55.0 44.5 Low 41.0 39.2 35.9 100 100 99.7
36.8 39.3 32.7 49.6 54.2 36.6 ResNet High 24.8 19.3 21.5 31.3 29.5 30.4 100
99.8 99.7 41.8 39.0 37.1 Medium 24.1 17.2 21.2 30.6 29.8 29.3 99.9 99.7 99.7
41.1 38.4 33.3 Low 18.6 17.2 16.8 26.0 28.0 24.7 99.8 99.9 99.6 34.4 38.8 27.8
XVec High 35.3 25.1 30.3 41.3 39.9 40.2 36.7 35.3 34.2 100 100 100 Medium 33.0
25.4 29.3 40.9 40.0 37.5 36.4 35.1 32.4 100 100 99.7 Low 27.8 23.9 23.5 36.3
39.1 33.5 30.9 34.3 27.5 100 100 98.7 Ensemble PGD w/o RawNet High 84.1 70.2
77.9 100 100 99.9 99.4 97.7 98.0 99.3 99.0 98.2 Medium 81.3 71.1 77.2 100 100
100 99.4 99.0 98.0 99.5 99.5 96.7 Low 78.8 67.9 70.5 100 100 100 98.6 98.4
94.8 98.7 98.9 93.8 w/o ECAPA High 77.4 65.3 69.7 53.8 52.9 53.4 99.8 98.7
98.6 98.7 97.3 95.1 Medium 74.9 57.3 68.8 54.3 54.0 51.5 99.7 99.4 98.9 98.9
98.5 91.8 Low 69.1 55.9 63.6 50.5 49.9 45.8 99 98.8 95.5 95.9 96.7 85.5 w/o
ResNet High 91.6 75.4 85.7 100 99.9 99.8 58.1 56.4 55.4 98.8 98.0 95.6 Medium
87.0 76.5 84.4 99.9 99.9 99.9 57.8 58.2 54.2 99.0 98.9 94.3 Low 86.9 73.3 80.6
99.9 99.7 99.4 54.9 54.9 49.7 97.6 97.9 89.0 w/o XVec High 89.1 76.4 82.6 100
99.9 99.9 91.6 85.6 85.9 71.4 68.5 63.6 Medium 83.5 72.7 81.8 99.9 99.9 99.8
91.6 89.8 87.5 71.9 71.4 62.2 Low 84.1 68.8 77.9 99.8 99.9 99.4 87.6 85.4 78.1
66.9 67.4 55.5

Table 4: Detection results of over-the-air adversarial attacks (EER%
$\downarrow$). The results for the four victim models are averaged to obtain
the results for both PGD and ensemble PGD attacks. The training set for row 4a
and 4b are bonafide samples go through the OTA process, while training samples
of other rows use bonafide samples. The setting of testing set is indicated in
2nd column. The column ‘overall’ pools all the testing samples together to
calculate EERs.

Row Spoof Sample of Speaker High Medium Low Overall Index the Test Set Attack
Mic iOS Android Android iOS Android Android iOS Android Android High Low High
Low High Low 1 OTA NA 4.90 4.97 4.63 8.24 10.04 6.53 4.68 7.05 4.73 6.66 2a
Digital PGD N/A N/A N/A 66.73 2b Ensemble 69.83 3a OTA PGD 3.66 1.24 1.14 1.27
1.02 0.67 4.27 3.85 4.06 3.49 3b Ensemble 4.65 1.09 1.13 1.58 1.07 0.48 4.06
2.60 3.20 3.20 4a OTA PGD 55.38 19.96 9.13 4.74 2.27 3.74 65.13 34.48 47.67
33.53 4b (Bonafide: OTA) Ensemble 61.39 15.32 8.34 6.76 2.39 1.71 66.76 24.54
44.81 34.61

###  4.1 Experimental Setup

ASV Models: We use four state-of-the-art ASV systems to generate adversarial
samples. The ASV models are trained and tested with open-source
toolkit888https://github.com/clovaai/voxceleb_trainer. The ASV systems are
trained on Voxceleb2 and tested on either the full dataset or a 25% subset of
Voxceleb1. The EERs are summarized in Table 1. It is observed that the
difference between EERs on the full dataset and the subset is trivial. We
presume the subset can represent the distribution of the full dataset, and
hence we use the subset to construct the AdvSV dataset.

Detection Model: The model is trained on the bonafide or replayed bonafide
samples from the Voxceleb2 dataset, and is tested on the AdvSV dataset,
assuming the detector has zero knowledge or limited knowledge of the
adversarial attacks.

Evaluation metric: We use attack success rates and equal error rates(EER) [26]
as evaluation metrics to evaluate adversarial attack performance and detection
performance. The success rate is defined as, $\textit{Attack Success
Rate}=\frac{\text{Number of Successful Attacks}}{\text{Number of Attacks}}$

###  4.2 Digital Adversarial Attack

We first examine the performance of digital adversarial attacks with the AdvSV
dataset. The results are presented in Table 2. It is observed that if a
surrogate model is the same as the victim model (i.e. white-box attack), the
success rates are always high, 100% or close to 100%. Note that a white-box
attack is expecting to achieve 100% success rate if there are enough PGD
steps. In the experiments, we keep the same PGD steps for a fair comparison.
Ensemble attacks achieve higher transferability than the single PGD attack.
Transferability measures the performance of transfer attacks. In particular,
with the PGD algorithm, the success rates are 10.6%, 8.8% and 14.1% when using
RawNet to transfer attack ECAPA, ResNet and XVec, respectively. However, the
ensemble PGD will increase success rates of transfer attacks to 62.3%, 62.5%
and 79.5% for ECAPA, ResNet and XVec, respectively.

In summary, the success rates of PGD white-box attack are as high as 100% or
close to 100%. Ensemble attacks can dramatically increase the success rates of
transfer attacks.

###  4.3 Over-the-Air Adversarial Attack

We then assess the performance of over-the-air(OTA) adversarial attacks with
the AdvSV dataset. Table 3 presents the success rates of OTA adversarial
attacks.

For the PGD white-box attacks, the RawNet system behaves differently from
other systems. The success rates are considerably lower than those of other
systems. This is because we set the same fixed number of PGD steps for all
systems, and RawNet requires more PGD steps to achieve a higher success rate.
From the loudspeaker perspective, a high-end speaker produces higher success
rates than a low-end speaker. Similarly, a high-end phone/microphone achieves
higher success rates than low-end phones or microphones. Additionally, the
success rates of transfer attacks are considerably lower than those of white-
box attacks. However, the success rates of transfer attacks still fall within
the range of 30% - 60%, with RawNet being an exception.

For the ensemble attacks, the success rates of transfer attacks are
considerably higher than those of PGD transfer attacks. For example, when
attacking the XVec system, the ensemble PGD can increase the success rates
from the range of 7.4% - 56.9% to the range of 55.5% - 71.9%. The phenomenon
in RawNet is similar to that in PGD, which is due to the fixed number of PGD
steps. Similar to PGD attacks, high-end loudspeakers or phones give higher
success rates than low-end ones.

In summary, when facing OTA adversarial attacks, ASV systems are still
vulnerable to transfer attacks, even if the ensemble PGD algorithm has no
access to the target system. Different OTA settings could result in different
success rates.

###  4.4 Detection of Over-the-Air Adversarial Attacks

Last but not least, we provide a baseline for detecting both digital and OTA
adversarial attacks with the AdvSV dataset. The detection results are
presented in Table 4.

In row 1, the classifier is trained on bonafide data without the OTA process,
but the testing data is processed with the OTA process. The overall detection
EER is 6.66%. Rows 1a and 2b present the detection of digital adversarial
attack samples, with both training and testing data being digital adversarial
attack samples. In comparison with row 1, the EER increases to 66.73% and
69.83% for PGD and ensemble attacks, respectively. Rows 3a and 3b present the
detection results of OTA adversarial attacks. Note that the training data are
bonafide samples without the OTA process. The overall EER is 3.49% and 3.20%
for PGD and ensemble attacks, respectively. The only difference between row
3a/3b and row 1 is whether perturbations are added. The results indicate that
the OTA process plays a more important role in the detection of attacks. Rows
4a and 4b use the same testing set as that in 3a and 3b, however, the training
set of 4a and 4b are bonafide samples passing through the OTA process. In
comparison to 2a and 2b, both training and testing sets of 4a and 4b go
through the OTA process. Both settings have considerably high EERs (i.e.
higher than 30%).

From the detection results, it suggests that detecting the adversarial attacks
or adversarial perturbations is a more challenging task than detecting whether
an audio sample has gone through the OTA process.

##  5 Conclusions and Future Work

We designed an over-the-air adversarial attack dataset for speaker
verification, called the AdvSV dataset, which will be released under the CC-BY
license. To develop the dataset, we used three loudspeakers, three
microphones, two perturbation generation algorithms and four state-of-the-art
ASV systems. In terms of adversarial attack success rate, the dataset presents
a genuine problem; the success rates can be higher than 50% in transfer
blackbox attacks. In terms of baseline detection performance, there is still a
long way to go to develop a successful countermeasure. In future work, we will
continue to expand the dataset by considering more realistic product
scenarios.

## References

  * [1] Jee weon Jung, Youjin Kim, Hee-Soo Heo, Bong-Jin Lee, Youngki Kwon, and Joon Son Chung,  “Pushing the limits of raw waveform speaker recognition,”  in Proc. Interspeech, 2022, pp. 2228–2232.
  * [2] Zhizheng Wu, Tomi Kinnunen, Nicholas Evans, Junichi Yamagishi, Cemal Hanilçi, Md. Sahidullah, and Aleksandr Sizov,  “ASVspoof 2015: the first automatic speaker verification spoofing and countermeasures challenge,”  in Proc. Interspeech, 2015, pp. 2037–2041.
  * [3] Arindam Jati, Chin-Cheng Hsu, Monisankha Pal, Raghuveer Peri, Wael AbdAlmageed, and Shrikanth Narayanan,  “Adversarial attack and defense strategies for deep speaker recognition systems,”  Computer Speech & Language, vol. 68, pp. 101199, 2021.
  * [4] Aleksander Madry, Aleksandar Makelov, Ludwig Schmidt, Dimitris Tsipras, and Adrian Vladu,  “Towards deep learning models resistant to adversarial attacks,”  in ICLR, 2018.
  * [5] Ali Shahin Shamsabadi, Francisco Sepúlveda Teixeira, Alberto Abad, Bhiksha Raj, Andrea Cavallaro, and Isabel Trancoso,  “Foolhd: Fooling speaker identification by highly imperceptible adversarial disturbances,”  in IEEE ICASSP, 2021, pp. 6159–6163.
  * [6] Guangke Chen, Sen Chenb, Lingling Fan, Xiaoning Du, Zhe Zhao, Fu Song, and Yang Liu,  “Who is real bob? adversarial attacks on speaker recognition systems,”  in 2021 IEEE Symposium on SP, 2021, pp. 55–72.
  * [7] Chu-Xiao Zuo, Jia-Yi Leng, and Wu-Jun Li,  “Speaker-Specific Utterance Ensemble based Transfer Attack on Speaker Identification,”  in Proc. Interspeech 2022, 2022, pp. 3203–3207.
  * [8] Yi Xie, Cong Shi, Zhuohang Li, Jian Liu, Yingying Chen, and Bo Yuan,  “Real-time, universal, and robust adversarial attacks against speaker recognition systems,”  in IEEE ICASSP, 2020, pp. 1738–1742.
  * [9] Patrick O’Reilly, Pranjal Awasthi, Aravindan Vijayaraghavan, and Bryan Pardo,  “Effective and inconspicuous over-the-air adversarial examples with adaptive filtering,”  in IEEE ICASSP, 2022, pp. 6607–6611.
  * [10] Xuejing Yuan, Yuxuan Chen, Yue Zhao, Yunhui Long, Xiaokang Liu, Kai Chen, Shengzhi Zhang, Heqing Huang, Xiaofeng Wang, and Carl A Gunter,  “Commandersong: A systematic approach for practical adversarial voice recognition,”  in 27th USENIX security symposium (USENIX security 18), 2018, pp. 49–64.
  * [11] Baolin Zheng, Peipei Jiang, Qian Wang, Qi Li, Chao Shen, Cong Wang, Yunjie Ge, Qingyang Teng, and Shenyi Zhang,  “Black-box adversarial attacks on commercial speech platforms with minimal information,”  in Proceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security, 2021, p. 86–107.
  * [12] Haibin Wu, Po-Chun Hsu, Ji Gao, Shanshan Zhang, Shen Huang, Jian Kang, Zhiyong Wu, Helen Meng, and Hung-Yi Lee,  “Adversarial sample detection for speaker verification by neural vocoders,”  in IEEE ICASSP, 2022, pp. 236–240.
  * [13] Haibin Wu, Xu Li, Andy T. Liu, Zhiyong Wu, Helen Meng, and Hung-Yi Lee,  “Improving the adversarial robustness for speaker verification by self-supervised learning,”  IEEE/ACM TASLP, vol. 30, pp. 202–217, 2022.
  * [14] Haibin Wu, Yang Zhang, Zhiyong Wu, Dong Wang, and Hung yi Lee,  “Voting for the Right Answer: Adversarial Defense for Speaker Verification,”  in Proc. Interspeech, 2021, pp. 4294–4298.
  * [15] Shutong Wu, Jiongxiao Wang, Wei Ping, Weili Nie, and Chaowei Xiao,  “Defending against adversarial audio via diffusion model,”  in ICLR, 2023.
  * [16] Zhiyuan Peng, Xu Li, and Tan Lee,  “Pairing Weak with Strong: Twin Models for Defending Against Adversarial Attack on Speaker Verification,”  in Proc. Interspeech, 2021, pp. 4284–4288.
  * [17] Qing Wang, Pengcheng Guo, Sining Sun, Lei Xie, and John H.L. Hansen,  “Adversarial Regularization for End-to-End Robust Speaker Verification,”  in Proc. Interspeech, 2019, pp. 4010–4014.
  * [18] Haibin Wu, Songxiang Liu, Helen Meng, and Hung-yi Lee,  “Defense against adversarial attacks on spoofing countermeasures of asv,”  in IEEE ICASSP, 2020, pp. 6564–6568.
  * [19] Monisankha Pal, Arindam Jati, Raghuveer Peri, Chin-Cheng Hsu, Wael AbdAlmageed, and Shrikanth Narayanan,  “Adversarial defense for deep speaker recognition using hybrid adversarial training,”  in IEEE ICASSP, 2021, pp. 6164–6168.
  * [20] Jesús Villalba, Sonal Joshi, Piotr Żelasko, and Najim Dehak,  “Representation Learning to Classify and Detect Adversarial Attacks Against Speaker and Speech Recognition Systems,”  in Proc. Interspeech, 2021, pp. 4304–4308.
  * [21] Yuekai Zhang, Ziyan Jiang, Jesús Villalba, and Najim Dehak,  “Black-Box Attacks on Spoofing Countermeasures Using Transferability of Adversarial Examples,”  in Proc. Interspeech, 2020, pp. 4238–4242.
  * [22] Xingming Wang, Xiaoyi Qin, Tinglong Zhu, Chao Wang, Shilei Zhang, and Ming Li,  “The DKU-CMRI System for the ASVspoof 2021 Challenge: Vocoder based Replay Channel Response Estimation,”  in Proc. Edition of the Automatic Speaker Verification and Spoofing Countermeasures Challenge, 2021, pp. 16–21.
  * [23] Brecht Desplanques, Jenthe Thienpondt, and Kris Demuynck,  “ECAPA-TDNN: Emphasized Channel Attention, Propagation and Aggregation in TDNN Based Speaker Verification,”  in Proc. Interspeech, 2020, pp. 3830–3834.
  * [24] Yoohwan Kwon, Hee-Soo Heo, Bong-Jin Lee, and Joon Son Chung,  “The ins and outs of speaker recognition: lessons from voxsrc 2020,”  in IEEE ICASSP, 2021, pp. 5809–5813.
  * [25] David Snyder, Daniel Garcia-Romero, Gregory Sell, Daniel Povey, and Sanjeev Khudanpur,  “X-vectors: Robust dnn embeddings for speaker recognition,”  in IEEE ICASSP, 2018, pp. 5329–5333.
  * [26] Marcus Karnan, Muthuramalingam Akila, and Nishara Krishnaraj,  “Biometric personal authentication using keystroke dynamics: A review,”  Applied Soft Computing, vol. 11, no. 2, pp. 1565–1573, 2011.


# Concurrent normals problem for convex polytopes and Euclidean distance
degree

Ivan Nasonov, Gaiane Panina, Dirk Siersma  I. Nasonov: StPetersburg State
University<EMAIL_ADDRESS>G. Panina: St. Petersburg department
of Steklov institute of mathematics<EMAIL_ADDRESS>; D. Siersma:
Mathematisch Instituut, Universiteit Utrecht<EMAIL_ADDRESS>
###### Abstract.

It is conjectured since long that for any convex body $P\subset\mathbb{R}^{n}$
there exists a point in its interior which belongs to at least $2n$ normals
from different points on the boundary of $P$. The conjecture is known to be
true for $n=2,3,4$.

We treat the same problem for convex polytopes in $\mathbb{R}^{3}$. It turns
out that the PL concurrent normals problem differs a lot from the smooth one.
One almost immediately proves that a convex polytope in $\mathbb{R}^{3}$ has
$8$ normals to its boundary emanating from some point in its interior.
Moreover, we conjecture that each simple polytope has a point in its interior
with $10$ normals to the boundary. We confirm the conjecture for all
tetrahedra and triangular prisms and give a sufficient condition for a simple
polytope to have a point with $10$ normals.

Other related topics (average number of normals, minimal number of normals
from an interior point, other dimensions) are discussed.

###### Key words and phrases:

Morse theory, bifurcations, polyhedra. MSC 52B70

Consider a compact convex polytope $P\subset\mathbb{R}^{n}$, pick a point $y$
from the interior of $P$, and study normals to the boundary $\partial P$
emanating from $y$. In the smooth case the normals to $\partial P$ are in a
natural bijection with the critical points of the squared distance function

$|x-y|^{2}:\partial P\rightarrow\mathbb{R}$

(abbreviated as $SQD_{y}$).

Smooth bodies, their normals, and $SQD_{y}$ fit nicely in the Milnor’s Morse
theory. The total number of critical points plays a role in the discussion on
tight and taut embeddings [1]. Also the bifurcations of critical points
(equivalently, birth-death of normals) played an important role in [6] and
[2]. Recently the study of the average number of critical points and
comparison with the complex case was published in [3] and is a part of an
ongoing research.

With some effort, Morse-theoretic approach extends also to polytopes. So
counting normals to the boundary is equivalent to counting critical points of
$SQD_{y}$.

In this paper we address the following questions. Assume $P$ is a compact
convex polytope in $\mathbb{R}^{3}$.

Q1: What is the analog of concurrent normals conjecture for convex polytopes?
That is, what is the maximal number of normals emanating from $y$ if $y$
ranges in the interior of $P$?

Q2: What is the minimal number of normals if $y$ ranges in the interior of
$P$?

This minimality question is important because of interest in the average
number of normals [3] which can be interpreted as an indicator of the shape of
the poytope, see Section 6.

######  Definition 1.

For a polytope $P$ and a point $y\in Int\,P$, denote by $n(P,y)$ the number of
normals to $\partial P$ emanating from $y$.

Set also

$\mathcal{N}(P)=\max_{y}n(P,y),$

where $y$ ranges over the interior of $P$.

Our main results are:

  * •

We show that $\mathcal{N}(P)\geq 2n+2$ for $P\subset\mathbb{R}^{n}$ (Theorem
1).

  * •

We propose the $10$-normals conjecture: $\mathcal{N}(P)\geq 10$ for any convex
polytope $P\subset\mathbb{R}^{3}$.

  * •

We confirm the conjecture for tetrahedra and triangular prisms (Proposition 6)
and give sufficient criteria for a simple polytope $P$ to satisfy
$\mathcal{N}(P)\geq 10$ (Theorem 4, Corollary 1, Corollary 3).

  * •

We also deduce some result concerning Q2 (Theorem 3).

##  1\. Definitions and preliminaries

Let $P\subset\mathbb{R}^{n}$ be a compact convex polytope with non-empty
interior. A face of $P$ is the intersection of $P$ with a support plane. So
the dimension of a face ranges from $0$ to $n-1$.

The faces of dimension $n-1$ are called facets. The $0$-dimensional faces are
vertices, and the $1$-dimensional faces are edges.

Given a face $F$, assume that the origin $O$ lies in the interior of $F$. The
inner normal cone of $F$ is

$Cone(F)=\\{x\in\mathbb{R}^{n}|\langle p,x\rangle\geq 0\ \ \forall p\in P\\}.$

Normals and active regions

Throughout the paper we assume that a point $y$ lies in the interior of $P$.
Let there is a support hyperplane $h$ to the polytope $P$ and a point $z\in
h\cap P$ such that $yz$ is orthogonal to $h$. Then $yz$ is called a normal to
the boundary of $P$ emanating from $y$. The point $z$ is called the base of
the normal.

Given a polytope $P$ and a face $F$, the active region $\mathcal{AR}(F)$ is
the set of all points $y\in Int\,P$ such that $F$ contains the base of some
normal emanating from $y$.

######  Lemma 1.

Assume that the origin $O$ lies in the interior of a face $F$. Then
$\mathcal{AR}(F)=\Big{(}Cone(F)+F\Big{)}\cap P$.

Bifurcation set and its sheets

The bifurcation set $\mathcal{B}(P)$ is the union of the boundaries of active
regions. It is the counterpart of the focal set that appears in the smooth
case. For all points $y$ not lying on $\mathcal{B}(P)$, the function $SQD_{y}$
is a Morse function.

The bifurcation set is piecewise linear. For $P\subset\mathbb{R}^{3}$, its
linear parts not lying on $\partial P$ (sheets) fall into two types, red and
blue, see the below explanation and Fig. 1.

Figure 1.  Active regions of a face and an edge

We have:

  1. (1)

The active region of a facet $F$ is the intersection of the infinite right
angled prism based on $F$ and the polytope $P$.

The side facets of the prism are called  blue sheets of $\mathcal{B}(P)$.

  2. (2)

The active region of an edge $E$ sharing two facets $F_{1}$ and $F_{2}$ is the
intersection of the polytope $P$ with the wedge-like polyhedron bounded by two
planes containing $E$ and orthogonal to $F_{1}$ and $F_{2}$ (these are blue
sheets), and another two planes containing the endpoints of $E$ and orthogonal
to $E$ (red sheets).

  3. (3)

The active region of a vertex $V$ is the inner normal cone of $P$ at the
vertex $V$ (bounded by red sheets) intersected with the polytope $P$.

It is worthy mentioning that the theory changes a lot if one allows non-convex
polytopes and/or points $y$ lying outside $P$.

######  Lemma 2.

(Birth-death of normals.)

If a point $y$ crosses transversally exactly one sheet of the bifurcation set,
either two normals emanating from $y$ die or two normals are born.

More precisely, if $y$ crosses transversally a blue sheet, we have a birth-
death of a normal with the base at a facet, and a normal with the base at an
edge.

If $y$ crosses transversally a red sheet, we have a birth-death of a normal
with the base at a vertex, and a normal with the base at an edge. When $y$
crosses the sheet, these two normals coincide.

##  2\. Squared distance function $SQD_{y}$ and its Morse-theoretic analysis

The function

$SQD_{y}=|x-y|^{2}:\partial P\rightarrow\mathbb{R}$

is a non-smooth function defined on a PL sphere.

We apply a construction used in [4]: consider the Minkowski sum
$P_{\varepsilon}:=P+\varepsilon B$, where $B$ is the unit ball and
$\varepsilon>0$. The boundary $\partial P_{\varepsilon}$ is a
$C^{1}$-manifold, and the normals of $\partial P$ and $\partial
P_{\varepsilon}$ are in a natural bijection: each base $z$ of a normal from
$y$ to $\partial P$ corresponds to a base $z_{\epsilon}\in\partial
P_{\varepsilon}$, see Fig. 2.

There is a natural stratification of $\partial P_{\varepsilon}$ into
$C^{\infty}$-smooth strata. Each face $F$ gives rise to a well-defined stratum
$F_{\varepsilon}$ which is a subset of the product of the face $F$ with a
sphere in the complementary plane. The gluing of these strata is directly
related to the bifurcations.

We will now use the critical point theory of $SQD_{y}$ on $\partial
P_{\varepsilon}$ (with notation $SQD_{y,\varepsilon}$) for the study of
normals on $\partial P$.

Figure 2.  $P_{\varepsilon}$ and the correspondence of critical points

######  Proposition 1.

For $y\notin\mathcal{B}(P)$ all critical points of $SQD_{y,\varepsilon}$ on
$\partial P_{\varepsilon}$ are the bases of normals to $\partial
P_{\varepsilon}$.

These critical points are Morse, and the Morse index of a critical point $z\in
F_{\varepsilon}$ equals $n-1-\dim F$.

###### Proof.

Since $y\notin\mathcal{B}(P)$, the base $z_{\varepsilon}$ of the normal lies
in the $C^{\infty}$ part of $\partial P_{\varepsilon}$. Therefore we can use
Milnor’s index formula: the Morse index is equal to the number of focal points
between $z_{\varepsilon}$ and $y$, counted with multiplicity [5]. Clearly the
focal point on the normal at $z_{\varepsilon}$ is $z$, which is the center of
the complementary sphere and has multiplicity $n-1-\dim F$. Since $z$ lies
between $z_{\varepsilon}$ and $y$ and there are no other focal points, the
proposition follows. ∎

So counting critical points of $SQD_{y}$ amounts to counting normals, exactly
as it is in the smooth case. We will use the machinery of Morse theory:

######  Proposition 2.

  1. Let $P\subset\mathbb{R}^{n}$.

  2. (1)

For $y\notin\mathcal{B}(P)$, the squared distance $SQD_{y}$ is a Morse
function.

  3. (2)

We have the Morse Theorem:

$\chi(\partial P)=1+(-1)^{n-1}=\sum_{i=o}^{n-1}(-1)^{i}m_{i},$

where $m_{i}$ is the number of critical points with Morse index $i$.

  4. (3)

Morse inequalities are valid. In particular we have

$m_{1}\geq m_{0}-1.$

###### Proof.

The proof literally repeats that of Milnor [5], one checks that all the
arguments are applicable to our non-smooth case. That is, we have the the
regular interval theorem, the cell attaching statement (in the $C^{2}$ part),
and therefore all the Morse counts.

∎

The following proposition is a Morse-theoretic counterpart of Lemma 2:

######  Proposition 3.

If $y$ crosses transversally one sheet of $\mathcal{B}(P)$, a pair of critical
points of $SQD_{y,\varepsilon}$ either dies or is born. In $\mathbb{R}^{3}$
there are simple rules:

  1. (1)

Crossing a blue sheet amounts to death-birth of a minimum and a saddle.

  2. (2)

Crossing a red sheet amounts to death-birth of a maximum and a saddle.

######  Lemma 3.

Let $y\in\mathcal{B}(P)$, then arbitrary close to $y$ there is a point
$y^{\prime}\in P\setminus\mathcal{B}(P)$ such that $n(P,y^{\prime})\geq
n(P,y)$. Therefore $\mathcal{N}(P)$ can be computed, using only points
$y\notin\mathcal{B(P)}$, and $\mathcal{N}(P)$ is always even.

###### Proof.

The statement is clear for a point lying on a unique sheet. If several sheets
are involved, choose a line through $y\in\mathcal{B}(P)$, which is transversal
to all sheets. Passing through $y$ in one direction will either increase or
decrease the number of normals by $1$ for each of the involved sheets. So
there is a direction and a point $y^{\prime}$ on the line such that
$n(P,y^{\prime})\geq n(P,y)$.

The number $n(P,y)$ is even for a generic $y$ since the number of critical
points of a Morse function on a closed manifold is even. ∎

Since normals to $\partial P_{\varepsilon}$ are in bijection with normals to
$\partial P$, we shall use the Morse theory for $\partial P$, keeping in mind
this correspondence. We will quote this below as ’’a critical point is
attained at a face of $P$.’’

##  3\. First results

For a polytope $P$, its face $F$ and a point $y\in Int\,P$ say that $y$
projects to $F$, if the orthogonal projection of $y$ to the affine hull
$aff(F)$ belongs to $F$.

###  3.1. Polygons in $\mathbb{R}^{2}$

Let $P$ be a planar convex polygon. If a point $y$ lies outside the
bifurcation set $\mathcal{B}(P)$, all the local minima of $SQD_{y}$ are
attained at the edges, and (local) maxima are attained at vertices.

An edge contributes a local minimum iff of $y$ projects to the edge.

######  Proposition 4.

  1. (1)

$\mathcal{N}(P)\geq 6$ for every convex polygon.

  2. (2)

$\mathcal{N}(P)=6$ for all triangles.

###### Proof.

(1) Take a circle inscribed in $P$. Its center $y$ contributes at least three
minima since there are at least three tangent points. Therefore there are at
least three maxima.

(2) is now clear since between two local minima there is always exactly one
point of local maximum. ∎

Example. Figure 3 depicts an obtuse triangle. Each point in the shaded domain
has $3$ maxima and $3$ minima of $SQD_{y}$. Points outside it have $2$ maxima
and $2$ minima.

Figure 3.  An obtuse triangle and a point with $4$ normals.

###  3.2. Convex polytopes in $\mathbb{R}^{3}$

Let $P\subset\mathbb{R}^{3}$ be a compact convex polytope.

Local minima of $SQD_{y}$ are attained at (some of the) facets, saddles are
attained at edges, and local maxima are attained at vertices.

######  Lemma 4.

Let $P\subset\mathbb{R}^{3}$ be a convex polytope, and let the dihedral angle
at its edge $e$ be acute. Then for a point $y\notin\mathcal{B}(P)$, the
function $SQD_{y}$ attains a saddle at the edge $e$ iff $y$ projects to $e$.

###### Proof.

Follows from Lemma 1. ∎

######  Lemma 5.

For a convex $P\subset\mathbb{R}^{3}$ and a point $y\notin\mathcal{B}(P)$, we
have

$n(P,y)=2+2s,$

where $s$ is the number of saddles.

###### Proof.

Follows from Proposition 2 and $n(P,y)=m+M+s,$ where $M$ is the number of
maxima, and $m$ is the number of minima. ∎

######  Theorem 1.

  1. For any convex polytope $P\subset\mathbb{R}^{n}$,

  2. (1)

There is always a point in $P$ with at least $2n+2$ normals to $\partial P$.

In other words,

$\mathcal{N}(P)\geq 2n+2.$

  3. (2)

$\mathcal{N}(P)$ never exceeds the number of faces of $P$.

###### Proof.

(1) Let $y$ be the center of the inscribed sphere (the sphere of maximal
radius contained in $P$).

There are at least $n+1$ tangential points with the facets of $P$. Each of
them contributes a minimum, each of them lies strictly inside some facet, and
therefore survives under small perturbations of the center $y$. So if
$y\in\mathcal{B}(P)$ (and therefore $SQD_{y}$ is not a Morse function),
perturb $y$ and get a Morse function with at least $n+1$ local minima.
Besides, there is at least one maximum, and, by Proposition 2, there are at
least $n$ other critical points with Morse index $1$.

(2) Each face contributes at most one critical point. ∎

######  Theorem 2.

There exists tetrahedra with $\mathcal{N}(P)=10,12,$ and $14$.

###### Proof.

(1) For the center $y$ of a regular tetrahedron one clearly has $n(P,y)=14$:
each face contributes a critical point ($4$ maxima, $4$ minima and $6$
saddles).

(2) Now prove the existence of a tetrahedron with $\mathcal{N}(P)=10$. Take
the following quadrilateral $ABCD$ lying in the horizontal plane as in Fig. 4.
Perturb it a little bit by shifting $B$ upwards from the plane. Now we have a
spatial tetrahedron $ABCD$.

i:

No point $y\in Int\,ABCD$ has saddles on both $AD$ and $BC$ simultaneously.
Indeed, no point from the tetrahedron projects orthogonally to both of the
edges (due to the chosen quadrilateral).

ii:

If $y$ has saddles on both $AC$ and $BD$, then $y$ has a saddle neither on
$AD$, nor on $BC$. Indeed, the dihedral angles at these two edges are very
obtuse (can be arbitrarily close to $\pi$), and therefore the active regions
almost degenerate to planes. So their intersection is a neighborhood of a line
that is transverse to the horizontal plane.

One concludes that the number of saddles does not exceed $4$. Lemma 5
completes the proof.

(3) Basing on this example, it is possible to construct generic tetrahedra
with $\mathcal{N}=12$: deform continuously the above constructed tetrahedron
to a regular one. ∎

Figure 4. A tetrahedron with at most $10$ normals from an inner point.

######  Theorem 3.

  1. (1)

For a tetrahedron $P$ and a point $y\in Int\,P$,
$n(P,y)$ is at least $4$.

  2. (2)

There exists a tetrahedron $P$ and a point $y$ with $n(P,y)=4$.

Remark. Statement (1) of the theorem is no longer valid for arbitrary convex
polytopes. It is easy to cook a polytope $P$ and a point $y$ inside $P$ (lying
very close to a facet) with $n(P,y)=2$.

###### Proof.

(1). Assume the contrary: for $P=ABCD$ and some point $y$ there is no saddle
point of the $SQD_{y}$. Then there is exactly one minimum and exactly one
maximum. Assume that the minimum point $z$ of the $SQD_{y}$ belongs to the
facet $ABC$. The point $z$ projects to at least two edges of the triangle
$ABC$. Let them be $BA$ and $CA$.

We prove a number of statements, using lemmata 4 and 5.

(a): The dihedral angles at the edges $BA$ and $CA$ are obtuse. The dihedral
angle at $BC$ is acute.

Indeed, otherwise the edges $BA$ and $CA$ contain saddle points of the
$SQD_{y}$. Besides, the dihedral angles at $AB$, $AC$ and $BC$ cannot be all
obtuse.

(b): the angle $BAC$ is acute.

Indeed, otherwise, $z$ projects to $BC$ as well, and there is a saddle point
on $BC$.

(c):  The projection of the vertex $D$ to the plane $ABC$ lies in the shaded
domain on the left, see Fig. 5. Therefore the angles $\angle DAB$ and $\angle
DAC$ are obtuse.

Figure 5. An illustration for (c).

(d): One of the two dihedral angles at the edges $DC$ and $DB$ is obtuse.

Indeed, otherwise all dihedral angles at the edges of the face $DBC$ are
acute, which means that all the points of $P$ (including the point $y$)
project to $DBC$. A contradiction to the uniqueness of minimum.

So without loss of generity we may assume that the dihedral angle $DC$ is
obtuse. Then, at the vertex $C$ there are two obtuse dihedral angles at the
edges $DC,AC$, and an acute planar angle $DCA$ (since $\angle DAC$ is obtuse).
It follows from here that $\angle DCB$ and $\angle ACB$ are obtuse (we have
already used such fact above, at the vertex $A$).

We are going to show that there is a saddle point of $SQD_{y}$ on $DB$. This
follows from statements (e) and (f) below.

(e): the dihedral angle at $DB$ is acute.

Let the dihedral angle $DB$ be obtuse. Then the planar angle $DBC$ is obtuse,
and the triangle $DBC$ has two obtuse angles. A contradiction.

(f):  $y$ projects to $DB$.

Consider the plane $b$ (respectively, $d$) through $B$ (respectively, $D$)
which is perpendicular to $DB$. Since $\angle DCB$ and $\angle DAB$ are
obtuse, all the angles $BDC,BDA,DBC,DBA$ are acute. It means that all the
points of $P$ (including the point $y$) lie between $b$ and $c$, and
therefore, project to $DB$.

(2) Here is an example: consider the tetrahedron $ABCD$ with following
properties:

i:

The dihedral angles at the edges $AC,DC,DB$ are obtuse, and the others are
acute,

ii:

The planar angles $ADB,ACB,DCB,ADC$ are obtuse, others are acute.

Such a tetrahedron exists, although it is a very subtle one: the obtuse angles
are almost right angles, so Figure 6 is unfortunately not much instructive.
Set, for example, $A=(-5;0;0),\ B=(2;0;0),\ C=(-1,54;-2,02;0),\
D=(-3,87;-1,11;1,52)$.

There exists a point $y$ inside $ABCD$, close to the vertex $C$ such that: the
angles between the three pairs of planes $(yDB,DBA),\ (yDC,DCB),$ and
$(yAC,ACD)$ are obtuse.

The $SQD_{y}$ has (the unique) saddle at the edge $AB$. Indeed, there are no
saddles at the edges $DB,DC,AC$ since the above angles are obtuse.
Additionally, we can request $yCB$ and $yDA$ be obtuse, because such condition
doesn’t contradict the condition above. So, there are no saddles at $AD$ and
$CB$.

In this example the function $SQD_{y}$ has two local maxima attained at the
vertices $A$ and $B$, and one minimum at the face $ABC$.

Figure 6. A tetrahedron $P$ with a point $n(y,P)=4$.

∎

##  4\. Trihedral angles and spherical triangles

We need to develop a spherical counterpart of the concurrent normals and
$SQD_{y}$ theory.

A spherical triangle is a triangle with geodesic edges lying in the standard
sphere $S^{2}$. It is always supposed to fit in an open hemisphere.

For points $X,Y\in S^{2}$ denote by $|XY|$ the spherical distance between the
two points.

Say that $X$ projects to a geodesic segment $s$ connecting $Y$ and $Z$, if the
segment and the point $X$ fit in an open hemisphere, and $s$ contains a point
$W$ such that the geodesic segment $XW$ is orthogonal to the segment. In this
case $|XW|$ realizes the Hausdorff distance between the point $X$ and the
segment $s$.

######  Definition 2.

A spherical triangle $ABC$ is nice if there is a point $X$ in its interior
such that

(a) $X$ projects to all the three edges of the triangle, and

(b) $|XA|<\pi/2$, $|XB|<\pi/2$, and $|XC|<\pi/2$.

Otherwise a spherical triangle is called skew.

######  Lemma 6.

A spherical triangle $ABC$ is skew iff (up to relabeling of the vertices)

  1. (1)

$|CA|>\pi/2$

  2. (2)

$|BC|<\pi/2$

  3. (3)

$\angle ABC>\pi/2$

  4. (4)

$\angle BAC<\pi/2$

  5. (5)

$\angle BCA<\pi/2$

  6. (6)

$|BA|>\pi/2$

  7. (7)

$|AZ|>\pi/2$ for point $Z\in AC$ such that $ZB$ is orthogonal to $BC$.

###### Proof.

Assume $ABC$ is skew. Take the smallest circle $Circ$ lying in the sphere that
contains $ABC$. Two cases are possible:

i:

All the three vertices $A,B,C$ lie on $Circ$. Set $X$ be the center of the
circle. The (spherical) distance from $X$ to the boundary of the triangle has
three maxima (at the vertices $A,B,C$), therefore also three minima. This
means that $X$ projects to the three edges.

Besides, the radius of $Circ$ is smaller than $\pi/2$, so the triangle is
nice, and we are done in this case.

ii:

$Circ$ contains only two vertices, say, $A$ and $C$. Then the center of $Circ$
is the centerpoint $O$ of the edge $AC$.

(1). Take a point $X$ on the bisector of the angle $ABC$ lying very close to
the edge $AC$. $X$ projects to all the three edges, and since $ABC$ is skew,
its distance to either $A$ or $C$ is greater than $\pi/2$. So we may assume
that $|AC|>\pi/2$.

Figure 7.  A skew triangle

(2). Take a point $X$ lying inside the triangle, very close to $O$. The
condition (b) from Definition 2 is satisfied. Besides, $X$ projects to $AC$.
The points $A$ and $C$ are maxima of the distance, so $X$ projects to one of
the other edges, say, to $AB$, but not to $BC$. Then $B$ and $C$ belong to one
and the same octant of the sphere obtained by the following construction (see
Fig. 8): the triangle $ABC$ lies in a hemisphere with a pole at $O$. $AC$ cuts
off a quarter of the sphere containing $ABC$. The orthogonal (to $AC$) line
passing through $O$ cuts off an octant, see Fig. 8.

Figure 8. The octant.

All distances in this octant don’t exceed $\pi/2$, so $|BC|<\pi/2$.

(3) is true because $B$ lies inside the circle $Circ$.

(4) and (5) follow directly from (3).

(6). If $|AB|<\pi/2$, then a point $X$ lying on bisector of the angle $ABC$ in
the interior of the triangle, very close to $B$, satisfies (a) and (b) from
Definition 2.

(7) Pick a point $X$ in the interior of $ABC$, inside the (spherical) active
region of the edge $BC$, and very close to $Z$. The edges contribute three
minima of spherical $SQD_{y}$, so if $ABC$ is skew then $|XA|>\pi/2$, since
all other conditions of the definition are fulfilled (point $X$ lies inside
the octant from (6)). Therefore, $|ZA|>\pi/2$.

Now let’s proof the converse. Let $ABC$ satisfy the conditions (1) — (7), and
a point $X$ exists. Then $X$ lies inside the (spherical) active region of
$BC$, which is bounded by $BZ$. But for every point $X$ inside it, the
distance $|AX|>\pi/2$. Indeed, this is true for $B$ and $Z$. Besides, the
angle $AZB$ is obtuse, so $|AX|$ is monotone on the segment $BZ$. Therefore,
$ABC$ is skew.

∎

######  Definition 1.

Let $A\subset S^{2}\subset\mathbb{R}^{3}$ be a spherically convex set
contained in a hemisphere. Its polar dual is defined as

$A^{\circ}=\\{x\in S^{2}|\langle x,y\rangle\geq 0\ \ \ \forall y\in A.\\}.$

######  Proposition 5.

A spherical triangle is skew iff its polar dual is skew.

###### Proof.

Duality turnes edges to vertices and vice versa. An edge length $\alpha$
turnes to the angle $\pi-\alpha$. Basing on Lemma 6, let us check that
conditions (1) — (7) are self-dual. It’s quite clear for (1) — (6). Condition
(7) is equivalent to folowing: $\angle CBZ^{\prime}>\pi/2$ for point
$Z^{\prime}\in AC$ such that $AZ^{\prime}=\pi/2$. This condition turns to (7)
for the dual triangle. ∎

Let $P\subset\mathbb{R}^{3}$ be a simple polytope. Each of its vertices $V$ is
associated a spherical triangle $Tr(V)$ which is the intersection of $P$ with
a small sphere centered at $V$. We equip the small sphere by the metric of the
standard sphere (with the unit radius).

The edges (resp., vertices) of $Tr(V)$ correspond to facets (resp., edges) of
$P$ incident to $V$.

Let $y$ be a point lying in $P$ very close to $V$. Denote by $Y$ the
intersection of the ray $Vy$ with the sphere. The critical points of $SQD_{y}$
can be easily translated into the language of spherical geometry of $Tr(V)$:

######  Lemma 7.

In the above notation,

  1. (1)

$V$ is a local maximum of $SQD_{y}$ iff spherical distances $|AY|$, $|BY|$,
and $|CY|$ are smaller than $\pi/2$, where $ABC$ is the spherical triangle
$Tr(V)$.

  2. (2)

Let $e$ be an edge of $P$ incident to $V$. Assume $A=Tr(V)\cap e$. The edge
$e$ contributes a saddle of $SQD_{y}$ iff

    1. (a)

$A$ is a local maximum of $|Yx|^{2}$, where $x$ ranges over the boundary of
the spherical triangle $ABC$.

    2. (b)

$|AY|<\pi/2$.

  3. (3)

A facet of $P$ incident to $V$ contributes a minimum of $SQD_{y}$ iff

    1. (a)

$Y$ projects to the corresponding edge (let it be $AB$).

    2. (b)

The spherical Hausdorff distance between $Y$ and $AB$ is less than $\pi/2$.

##  5\. The $10$-normals conjecture for simple polytopes in $\mathbb{R}^{3}$

Genericity assumption

In the section we bound ourselves by generic simple polytopes. This means that

i:

There are no right dihedral angles, and also no right planar angles of the
facets.

ii:

The boundaries of two active regions of non-incident facets intersect
transversally.

######  Definition 3.

A vertex $V$ of a simple polytope $P$ is nice if $Tr(V)$ is a nice triangle.

######  Theorem 4.

If a simple convex polytope $P$ has at least one nice vertex, then
$\mathcal{N}(P)\geq 10$.

###### Proof.

Assume that $V$ is a nice vertex of a polytope $P$. Take the small sphere
centered at $V$ and the spherical triangle $Tr(V)$. Since the triangle is
nice, Definition 2 guarantees the existence of a point $X$ with special
properties.

Take the ray $VX$. It belongs to the active region $\mathcal{AR}(V)$, that is,
for every point on the ray, $V$ is a local maximum. Take a point $y$ lying on
the ray very close to $V$. By Definition 2 and Lemma 7, $y$ belongs to active
regions of all three edges and all three facets incident to $V$.

Now let the point $y$ travel along the ray starting at $V$. Initially
$SQD_{y}$ has (at least) three minima $m_{1},m_{2},$ and $m_{3}$, lying on the
faces incident to $V$, three saddles $s_{1},s_{2},$ and $s_{3}$, one local
maximum $V$, which cannot be a global one. Therefore there is also a global
maximum $V^{\prime}\neq V$. Altogether we have at least $8$ critical points of
$SQD_{y}$, or, equivalently, $8$ normals emanating from $y$.

Keep moving until the first bifurcation or until the point $y$ leaves the
interior of $P$. Let us analyze the first event.

  1. (1)

The point $y$ leaves the polytope $P$. This means that $y$ hits one of the
facets which is not incident to the vertex $V$. Just before $y$ leaves the
polytope $P$, there are (at least) $4$ minima and $2$ maxima, therefore at
least $4$ saddles.

  2. (2)

A birth of two new critical points. This gives us $10$ normals.

  3. (3)

One of the saddles $s_{i}$ dies. This happens in two cases:

    1. (a)

$s_{i}$ meets a (local) maximum of $SQD_{y}$. The maximum cannot be $V$ since
by construction, $s_{i}$ slides away from $V$.

Let us prove that the maximum is not $V^{\prime}$. Indeed, recall that $s_{i}$
is the orthogonal projection of $y$ to the edge. If $s_{i}$ meets $V^{\prime}$
before $y$ leaves $P$, then $|Vy|>|VV^{\prime}|$. A contradiction.

So just before the bifurcation $SQD_{y}$ has $3$ minima and $3$ maxima, which
proves the desired.

    2. (b)

$s_{i}$ meets a minimum. It can be none of $m_{1},m_{2}$, and $m_{3}$, so just
before the bifurcation $SQD_{y}$ has $4$ minima and $2$ maxima, which proves
the claim.

    3. (c)

The point $V^{\prime}$ meets a saddle point and dies. This happens if
$V^{\prime}$ meets one of the saddles. This cannot be one of
$s_{1},s_{2},s_{3}$ (already discussed above). So just before the bifurcation
$SQD_{y}$ has $4$ saddles, which proves the claim.

∎

It is still an open question if there exist a polytope with
$\mathcal{N}(P)=8$. But we anyhow have the following:

######  Corollary 1.

Assume $P$ is a simple polytope, $\mathcal{N}(P)<10$. Then

  1. (1)

Each vertex has exactly two incident acute dihedral angles.

  2. (2)

Each vertex has exactly one incident acute planar angle. This angle is not
between two edges that give acute dihedral angles.

######  Corollary 2.

Assume that $\partial P$ lies between two concentric spheres whose radii
relate as $\sqrt{2}$. Then $\mathcal{N}(P)\geq 10$.

###### Proof.

It’s easy to see that in this case there are no acute dihedral angles in $P$.
A contradiction to Corollary 1. ∎

######  Corollary 3.

Assume that $\mathcal{N}(P)<10$. Then the outer normal fan of $P$ yields a
tiling of the sphere $S^{2}$ into skew triangles.

###### Proof.

By Proposition 5, a dual to a skew triangle is also a skew triangle. It
remains to remind that the outer normal fan tiles the sphere into spherical
polytopes dual to $Tr(V)$, where $V$ ranges over the vertices of $P$. ∎

######  Proposition 6.

  1. (1)

For any triangular prism $P$, $\mathcal{N}(P)\geq 10$.

  2. (2)

For any tetrahedron $P$, $\mathcal{N}(P)\geq 10$.

###### Proof.

(1) Assume the contrary. This means that each of the six vertices is skew, and
therefore, there are exactly six acute planar angles of the facets of the
prism. However, each triangular facet of a prism has at least two acute
angles, whereas each quadrilateral facet has at least one. Altogether there at
least seven acute angles. A contradiction.

(2) We give two proofs.

(a) A similar count of acute planar angles as in (1) proves the statement.

(b)The outer normal fan of a tetrahedron tiles the sphere into four triangles
with vertices, say, $A,B,C,D$. If $\mathcal{N}(P)<10$, then all these
triangles are skew. Take the longest of their edges, say, $AB$. By Lemma 6,
the vertices $C$ and $D$ (as well as $A$ and $B$) lie in the hemisphere
centered at the midpoint of $AB$. A contradiction. ∎

Corollary 3 hints that for the majority of simple polytopes,
$\mathcal{N}(P)\geq 10$. However, the problem which is still open:
is $\mathcal{N}(P)\geq 10$ always true for simple polytopes?

##  6\. Averaging normals, Euclidean Distance Degree

Following the idea of Euclidean distance degree for smooth bodies or algebraic
subsets of Draisma et al [3], let us define for a convex compact polytope the
average number of normals:

$\mathcal{EN}(P)=\frac{1}{Vol(P)}\int_{P}n(P,y)dy$

The bifurcation set $\mathcal{B}(P)$ divides $P$ into chambers $\sigma$ such
that the number $n(P,y)$ is constant on each of the chambers (we use the
notation $n(P,\sigma)$).

We immediately have an upper bound:

######  Proposition 7.

$\mathcal{EN}(P)\leq\frac{1}{Vol(P)}\mbox{\rm\Big{(}Total number of
faces\Big{)}}.$

######  Proposition 8.

$\mathcal{EN}(P)=\frac{\sum_{\sigma}Vol(\sigma)n(P,\sigma)}{Vol(P)}$

This average contains information about the shape of $P$ which seems to be
related to obtuse angles.

######  Proposition 9.

For a triangle in the plane,

  1. (1)

$\mathcal{EN}(P)$ equals $6$ iff the triangle is not obtuse.

  2. (2)

For an obtuse triangle, $\mathcal{EN}(P)$ is between $4$ and $6$, depending on
the value of the obtuse angle. It tends to $6$ if the obtuse angle tends to
$\pi/2$, and tends to $4$ if the obtuse angle tends to $\pi$.

######  Proposition 10.

For a tetrahedron,

  1. (1)

$\mathcal{EN}(P)\leq 14$.

  2. (2)

$\mathcal{EN}(P)=14$ iff all planar angles of the faces and all the dihedral
angles are acute.

###### Proof.

$\mathcal{EN}(P)=14$ iff each inner point $y$ of the tetrahedron has $14$
emanating normals. This happens iff $y$ projects to all the edges, and all the
dihedral edges are acute. ∎

Since $\mathcal{EN}(P)$ measures the overlaps between active regions it
depends on the shape of the polytope within the given the combinatorial type,
although the concept of shape is not well-defined. One could use
$\mathcal{EN}(P)$, but also $\mathcal{N}(P)$ as one of the indicators for
shape. Another Morse theorectic approach to the shape of a tetrahedron can be
found in [7].

### Acknowledgements

The authors acknowledge useful discussions with George Khimshiashvili and
hospitality of CIRM, Luminy, where this research was completed in framework of
”Research in Pairs” program in January, 2024.

## References

  * [1] T.E.Cecil, R.J.Ryan, Tight and Taut Immersions of Manifolds, Pitman, 1985.
  * [2] A. Grebennikov, G. Panina, A note on the concurrent normal conjecture, Acta Mathematica Hungarica, 167 (2022), 529-532.
  * [3] J. Draisma, E. Horobet, G. Ottaviani, B. Sturmfels, R. Thomas, The Euclidean distance degree of an algebraic variety, Found. Comput. Math. 16 (2016), no. 1, 99–149.
  * [4] E. Heil, Concurrent normals and critical points under weak smoothness assumptions, In: Discrete geometry and convexity (New York, 1982), volume 440 of Ann. New York Acad. Sci., 170-178. New York Acad. Sci., New York, 1985.
  * [5] J. Milnor, Morse theory, Annals of Math. Studies 51, Princeton University Press, Princeton, 1963.
  * [6] J. Pardon, Concurrent normals to convex bodies and spaces of morse functions, Math. Ann., 352(2012), no. 1, 55-71.
  * [7] D. Siersma, M. van Manen, The Nine Morse Generic Tetrahedra, SIAM Journal on Discrete Mathematics 22 (2004), no. 2, 737-746.


better termination behavior, produces fewer redundant unifiers, and can be
implemented more efficiently than procedures such as Jensen and
Pietrzykowski’s jensen-pietrzykowski-1976  and Snyder and Gallier’s snyder-
gallier-1989 . The set of fluid terms is overapproximated in the
implementation by the set of terms that are either nonground
$\lambda$-expressions or terms of the form $y\>\bar{u}_{n}$ with $n>0$. To
efficiently retrieve candidates for Abs inferences without slowing down
superposition term indexing structures, we implemented dedicated indexing for
clauses that are eligible for Abs inferences (vukmirovic-
nummelin-2020-boolean, , Sect. 3.3).

Zipperposition implements a DISCOUNT-style given clause procedure avenhaus-et-
al-1995 . The proof state is represented by a set $A$ of active clauses and a
set $P$ of passive clauses. To interleave nonterminating unification with
other computation, we added a set $T$ containing possibly infinite sequences
of scheduled inferences. These sequences are stored as finite instructions of
how to compute the inferences. Initially, all clauses are in $P$. At each
iteration of the main loop, the prover heuristically selects a _given clause_
$C$ from $P$. If $P$ is empty, sequences from $T$ are evaluated to generate
more clauses into $P$; if no clause can be produced in this way, $A$ is
saturated and the prover stops. Assuming a given clause $C$ could be selected,
it is first simplified using $A$. Clauses in $A$ are then simplified w.r.t.
$C$, and any simplified clause is moved to $P$. Then $C$ is added to $A$ and
all sequences representing nonredundant inferences between $C$ and $A$ are
added to $T$. This maintains the invariant that all nonredundant inferences
between clauses in $A$ have been scheduled or performed. Then some of the
scheduled inferences in $T$ are performed and the conclusions are put into
$P$.

We can view the above loop as an instance of the abstract Zipperposition loop
prover ZL of Waldmann et al. (waldmann-et-al-2020-saturation, , Example 34).
Their Theorem 32 allows us to obtain dynamic completeness for this prover
architecture from our static completeness result (Theorem 54). This requires
that the sequences in $T$ are visited fairly, that clauses in $P$ are chosen
fairly, and that simplification terminates, all of which are guaranteed by our
implementation.

The unification procedure we use returns a sequence of either singleton sets
containing the unifier or an empty set signaling that a unifier is still not
found. Empty sets are returned to give back control to the caller of
unification procedure and avoid getting stuck on nonterminating problems.
These sequences of unifier subsingletons are converted into sequences
containing subsingletons of clauses representing inference conclusions.

##  7 Evaluation

We evaluated our prototype implementation of the calculus in Zipperposition
with other higher-order provers and with Zipperposition’s modes for less
expressive logics. All of the experiments were performed on StarExec nodes
equipped with Intel Xeon E5-2609 0 CPUs clocked at 2.40 GHz. Following CASC
2019,222http://tptp.cs.miami.edu/CASC/27/ we use 180 s as the CPU time limit.

We used both standard TPTP benchmarks sutcliffe-2017-tptp  and Sledgehammer-
generated benchmarks meng-paulson-2008-trans . From the TPTP, version 7.2.0,
we used 1000 randomly selected first-order (FO) problems in CNF, FOF, or TFF
syntax without arithmetic and all 499 monomorphic higher-order theorems in TH0
syntax without interpreted Booleans and arithmetic. We partitioned the TH0
problems into those containing no $\lambda$-expressions (TH0$\lambda$f, 452
problems) and those containing $\lambda$-expressions (TH0$\lambda$, 47
problems). The Sledgehammer benchmarks, corresponding to Isabelle’s Judgment
Day suite boehme-nipkow-2010 , were regenerated to target clausal higher-order
logic. They comprise 2506 problems, divided in two groups: SH-$\lambda$
preserves $\lambda$-expressions, whereas SH-ll encodes them as
$\lambda$-lifted supercombinators meng-paulson-2008-trans  to make the
problems accessible to $\lambda$-free clausal higher-order provers. Each group
of problems is generated from 256 Isabelle facts (definitions and lemmas). Our
results are publicly available.333https://doi.org/10.5281/zenodo.4032969

#### Evaluation of Extensions

To assess the usefulness of the extensions described in Sect. 5, we fixed a
_base_ configuration of Zipperposition parameters. For each extension, we then
changed the corresponding parameters and observed the effect on the success
rate. The base configuration uses the complete variant of the unification
procedure of Vukmirović et al. vukmirovic-et-al-2020-unif . It also includes
the optional rules NegExt and PruneArg, substitutes FlexSup for the highly
explosive FluidSup, and excludes axiom (Ext). The base configuration is not
refutationally complete.

|  $-$NE,$-$PA |  $-$NE |  $-$PA | Base
---|---|---|---|---
TH0 | 446 (0) | 446 (0) | 447 (0) | 447 (0)
SH-$\lambda$ | 431 (0) | 433 (0) | 433 (0) | 436 (1)

Figure 1: Number of problems proved without rules included in the base
configuration

| Base |  $+\lambda$D |  $+\lambda$S0 |  $+\lambda$S1 |  $+\lambda$S2 |  $+\lambda$S4 |  $+\lambda$S8 |  $+\lambda$S1024
---|---|---|---|---|---|---|---|---
TH0 | 447 (0) | 448 (0) | 449 (0) | 449 (0) | 449 (0) | 449 (0) | 449 (0) | 449 (0)
SH-$\lambda$ | 436 (1) | 435 (4) | 430 (1) | 429 (0) | 429 (0) | 429 (0) | 429 (0) | 429 (0)

Figure 2: Number of problems proved using rules that perform rewriting under
$\lambda$-binders

| Base |  $+$Abs |  $+$ExtInst |  $+$(Ext)
---|---|---|---|---
TH0 | 447 (0)0 | 450 (1)0 | 450 (1) | 376 (0)
SH-$\lambda$ | 436 (11) | 430 (11) | 402 (1) | 365 (2)

Figure 3: Number of problems proved using rules that perform extensionality
reasoning

|  $-$FlexSup | Base |  $-$FlexSup,$+$DupSup |  $-$FlexSup,$+$FluidSup
---|---|---|---|---
TH0 | 446 (0)0 | 447 (0) | 448 (1) | 447 (0)
SH-$\lambda$ | 469 (10) | 436 (4) | 451 (3) | 461 (7)

Figure 4: Number of problems proved with rules that perform superposition into
fluid terms

The rules NegExt (NE) and PruneArg (PA) were added to the base configuration
because our informal experiments showed that they usually help. Fig. 4
confirms this, although the effect is small. In all tables, $+R$ denotes the
inclusion of a rule $R$ not present in the base, and $-R$ denotes the
exclusion of a rule $R$ present in the base. Numbers given in parentheses
denote the number of problems that are solved only by the given configuration
and no other configuration in the same table.

The rules $\lambda$Demod ($\lambda$D) and $\lambda$Sup extend the calculus to
perform some rewriting under $\lambda$-binders. While experimenting with the
calculus, we noticed that, in some configurations, $\lambda$Sup performs
better when the number of fresh Skolem symbols it introduces overall is
bounded by some parameter $n$. As Fig. 4 shows, inclusion of these rules has
different effect on the two benchmark sets. Different choices of $n$ for
$\lambda$Sup (denoted by $\lambda$S$n$) do not seem to influence the success
rate much.

The evaluation of the Abs and ExtInst rules and axiom (Ext), presented in Fig.
4, confirms our intuition that including the extensionality axiom is severely
detrimental to performance. The $+$(Ext) configuration solved two unique
problems on SH-$\lambda$ benchmarks, but the success of the $+$(Ext)
configuration on these problems appears to be due to a coincidental influence
of the axiom on heuristics—the axiom is not referenced in the generated
proofs.

The FlexSup rule included in the base configuration did not perform as well as
we expected. Even the FluidSup and DupSup rules outperformed FlexSup, as shown
in Fig. 4. This effect is especially visible on SH-$\lambda$ benchmarks. On
TPTP, the differences are negligible.

Most of the extensions had a stronger effect on SH-$\lambda$ than on TH0. A
possible explanation is that the Boolean-free TH0 benchmark subset consists
mostly of problems that are simple to solve using most prover parameters. On
the other hand, SH-$\lambda$ benchmarks are of varying difficulty and can thus
benefit more from changing prover parameters.

#### Main Evaluation

We selected all contenders in the THF division of CASC 2019 as representatives
of the state of the art: CVC4 1.8 prerelease barbosa-et-al-2019 , Leo-III 1.4
steen-benzmueller-2018 , Satallax 3.4 brown-2012-ijcar , and Vampire 4.4
bhayat-reger-2019-restricted . We also included Ehoh vukmirovic-et-al-2019 ,
the $\lambda$-free clausal higher-order mode of E 2.4. Leo-III and Satallax
are cooperative higher-order provers that can be set up to regularly invoke
first-order provers as terminal proof procedures. To assess the performance of
their core calculi, we evaluated them with first-order backends disabled. We
denote these “uncooperative” configurations by Leo-III-uncoop and Satallax-
uncoop respectively, as opposed to the standard versions Leo-III-coop and
Satallax-coop.

| FO | TH0$\lambda$f | TH0$\lambda$ | SH-ll | SH-$\lambda$
---|---|---|---|---|---
CVC4 | 539 | 424 | 31 | 696 | 650
Ehoh | 681 | 418 | – | 691 | –
Leo-III-uncoop | 198 | 389 | 42 | 226 | 234
Leo-III-coop | 582 | 438 | 43 | 683 | 674
Satallax-uncoop | – | 398 | 43 | 489 | 507
Satallax-coop | – | 432 | 43 | 602 | 616
Vampire | 729 | 432 | 42 | 718 | 707
FOZip | 399 | – | – | – | –
@+FOZip | 363 | 400 | – | 478 | –
$\lambda$freeZip | 395 | 398 | – | 538 | –
$\lambda$Zip-base | 388 | 408 | 39 | 420 | 436
$\lambda$Zip-pragmatic | 396 | 411 | 33 | 496 | 503
$\lambda$Zip-full | 177 | 339 | 34 | 353 | 361
Zip-uncoop | 514 | 426 | 46 | 661 | 677
Zip-coop | 625 | 434 | 46 | 710 | 717
Figure 5: Number of problems proved by the different provers

To evaluate the overhead our calculus incurs on first-order or $\lambda$-free
higher-order problems, we ran Zipperposition in first-order (FOZip) and
$\lambda$-free ($\lambda$freeZip) modes, as well as in a mode that encodes
curried applications using a distinguished binary symbol ${\mathsf{@}}$ before
using first-order Zipperposition (@+FOZip). We evaluated the implementation of
our calculus in Zipperposition ($\lambda$Zip) in three configurations: base,
pragmatic, and full. Pragmatic builds on base by disabling FlexSup and
replacing complete unification with the pragmatic variant procedure
pv${}^{2}_{1121}$ of Vukmirović et al. Full is a refutationally complete
extension of base that substitutes FluidSup for FlexSup and includes axiom
(Ext). Finally, we evaluated Zipperposition in a portfolio mode that runs the
prover in various configurations (Zip-uncoop). We also evaluated a cooperative
version of the portfolio which, in some configurations, after a predefined
time invokes Ehoh as backend on higher-order problems (Zip-coop). In this
version, Zipperposition encodes heuristically selected clauses from the
current proof state to lambda-free higher-order logic supported by Ehoh
vukmirovic-et-al-2019 . On first-order problems, we ran Ehoh, Vampire, and
Zip-uncoop using the provers’ respective first-order modes.

A summary of these experiments is presented in Figure 5. In the pragmatic
configuration, our calculus outperformed $\lambda$freeZip on TH0$\lambda$f
problems and incurred less than 1% overhead compared with FOZip, but fell
behind $\lambda$freeZip on SH-ll problems. The full configuration suffers
greatly from the explosive extensionality axiom and FluidSup rule.

Except on TH0$\lambda$ problems, both base and pragmatic configurations
outperformed Leo-III-uncoop, which runs a fixed configuration, by a
substantial margin. Zip-uncoop outperformed Satallax-uncoop, which uses a
portfolio. Our most competitive configuration, Zip-coop, emerges as the winner
on both problem sets containing $\lambda$-expressions.

On higher-order TPTP benchmarks this configuration does not solve any problems
that no other (cooperative) higher-order prover solves. By contrast, on SH-ll
benchmarks Zip-coop solves 21 problems no other higher-order prover solves,
and on SH-$\lambda$ benchmarks, it uniquely solves 27 problems.

##  8 Discussion and Related Work

Bentkamp et al. bentkamp-et-al-2018  introduced four calculi for
$\lambda$-free clausal higher-order logic organized along two axes:
_intensional_ versus _extensional_ , and _nonpurifying_ versus _purifying_.
The purifying calculi flatten the clauses containing applied variables,
thereby eliminating the need for superposition into variables. As we extended
their work to support $\lambda$-expressions, we found the purification
approach problematic and gave it up because it needs $x$ to be smaller than
$x\;t$, which is impossible to achieve with a term order on
$\beta\eta$-equivalence classes. We also quickly gave up our attempt at
supporting intensional higher-order logic. Extensionality is the norm for
higher-order unification dowek-2001  and is mandated by the TPTP THF format
sutcliffe-et-al-2009  and in proof assistants such as HOL4, HOL Light,
Isabelle/HOL, Lean, Nuprl, and PVS.

Bentkamp et al. viewed their approach as “a stepping stone towards full
higher-order logic.” It already included a notion analogous to green subterms
and an ArgCong rule, which help cope with the complications occasioned by
$\beta$-reduction.

Our Boolean-free $\lambda$-superposition calculus joins the family of proof
systems for higher-order logic. It is related to Andrews’s higher-order
resolution andrews-1971 , Huet’s constrained resolution huet-1973 , Jensen and
Pietrzykowski’s $\omega$-resolution jensen-pietrzykowski-1976 , Snyder’s
higher-order $E$-resolution snyder-1990 , Benzmüller and Kohlhase’s
extensional higher-order resolution benzmueller-kohlhase-1998 , Benzmüller’s
higher-order unordered paramodulation and RUE resolution benzmueller-1999 ,
and Bhayat and Reger’s combinatory superposition bhayat-reger-2020-combsup . A
noteworthy variant of higher-order unordered paramodulation is Steen and
Benzmüller’s higher-order ordered paramodulation steen-benzmueller-2018 ,
whose order restrictions undermine refutational completeness but yield better
empirical results. Other approaches are based on analytic tableaux
robinson-1969 ; kohlhase-1995 ; konrad-1998 ; backes-brown-2011 , connections
andrews-1989 , sequents lindblad-2014 , and satisfiability modulo theories
(SMT) barbosa-et-al-2019 . Andrews andrews-2001  and Benzmüller and Miller
benzmueller-miller-2014  provide excellent surveys of higher-order automation.

Combinatory superposition was developed shortly after $\lambda$-superposition
and is closely related. It is modeled on the intensional nonpurifying calculus
by Bentkamp et al. and targets extensional polymorphic clausal higher-order
logic. Both combinatory and $\lambda$-superposition gracefully generalize the
highly successful first-order superposition rules without sacrificing
refutational completeness, and both are equipped with a redundancy criterion,
which earlier refutationally complete higher-order calculi lack. In
particular, PruneArg is a versatile simplification rule that could be useful
in other provers. Combinatory superposition’s distinguishing feature is that
it uses ${\mathsf{SKBCI}}$ combinators to represent $\lambda$-expressions.
Combinators can be implemented more easily starting from a first-order prover;
$\beta$-reduction amounts to demodulation. However, according to its
developers bhayat-reger-2020-combsup , “Narrowing terms with combinator axioms
is still explosive and results in redundant clauses. It is also never likely
to be competitive with higher-order unification in finding complex unifiers.”
Among the drawbacks of $\lambda$-superposition are the need to solve flex–flex
pairs eagerly and the explosion caused by the extensionality axiom. We believe
that this is a reasonable trade-off, especially for large problems with a
substantial first-order component.

Our prototype Zipperposition joins the league of automatic theorem provers for
higher-order logic. We list some of its rivals. TPS andrews-et-al-1996  is
based on the connection method and expansion proofs. LEO benzmueller-
kohlhase-1998  and Leo-II benzmuller-2015-leo2  implement variants of RUE
resolution. Leo-III steen-benzmueller-2018  is based on higher-order
paramodulation. Satallax brown-2012-ijcar  implements a higher-order tableau
calculus guided by a SAT solver. Leo-II, Leo-III, and Satallax integrate
first-order provers as terminal procedures. AgsyHOL lindblad-2014  is based on
a focused sequent calculus guided by narrowing. The SMT solvers CVC4 and veriT
have recently been extended to higher-order logic barbosa-et-al-2019 . Vampire
now implements both combinatory superposition and a version of standard
superposition with first-order unification replaced by restricted combinatory
unification bhayat-reger-2019-restricted .

Half a century ago, Robinson robinson-1970  proposed to reduce higher-order
logic to first-order logic via a translation. “Hammer” tools such as
Sledgehammer paulson-blanchette-2010 , Miz$\mathbb{AR}$ urban-et-al-2013 ,
HOLyHammer kaliszyk-urban-2015 , and CoqHammer czajka-kaliszyk-2018  have
since popularized this approach in proof assistants. The translation must
eliminate the $\lambda$-expressions, typically using ${\mathsf{SKBCI}}$
combinators or $\lambda$-lifting meng-paulson-2008-trans , and encode typing
information blanchette-et-al-2016-types .

##  9 Conclusion

We presented the Boolean-free $\lambda$-superposition calculus, which targets
a clausal fragment of extensional polymorphic higher-order logic. With the
exception of a functional extensionality axiom, it gracefully generalizes
standard superposition. Our prototype prover Zipperposition shows promising
results on TPTP and Isabelle benchmarks. In future work, we plan to pursue
five main avenues of investigation.

We first plan to _extend the calculus to support Booleans and Hilbert choice._
Booleans are notoriously explosive. We want to experiment with both
axiomatizations and native support in the calculus. Native support would
likely take the form of a primitive substitution rule that enumerates
predicate instantiations andrews-1989 , delayed clausification rules
ganzinger-stuber-2005 , and rules for reasoning about Hilbert choice.

We want to investigate techniques to _curb the explosion caused by functional
extensionality._ The extensionality axiom reintroduces the search space
explosion that the calculus’s order restrictions aim at avoiding. Maybe we can
replace it by more restricted inference rules without compromising
refutational completeness.

We will also look into approaches to _curb the explosion caused by higher-
order unification._ Our calculus suffers from the need to solve flex–flex
pairs. Existing procedures jensen-pietrzykowski-1976 ; snyder-gallier-1989 ;
vukmirovic-et-al-2019  enumerate redundant unifiers. This can probably be
avoided to some extent. It could also be useful to investigate unification
procedures that would delay imitation/projection choices via special schematic
variables, inspired by Libal’s representation of regular unifiers libal-2015 .

We clearly need to _fine-tune and develop heuristics._ We expect heuristics to
be a fruitful area for future research in higher-order reasoning. Proof
assistants are an inexhaustible source of easy-looking benchmarks that are
beyond the power of today’s provers. Whereas “hard higher-order” may remain
forever out of reach, we believe that there is a substantial “easy higher-
order” fragment that awaits automation.

Finally, we plan to _implement the calculus in a state-of-the-art prover._ A
suitable basis for an optimized implementation of the calculus would be Ehoh,
the $\lambda$-free clausal higher-order version of E developed by Vukmirović,
Blanchette, Cruanes, and Schulz vukmirovic-et-al-2019 .

###### Acknowledgements.

Simon Cruanes patiently explained Zipperposition’s internals and allowed us to
continue the development of his prover. Christoph Benzmüller and Alexander
Steen shared insights and examples with us, guiding us through the literature
and clarifying how the Leos work. Maria Paola Bonacina and Nicolas Peltier
gave us some ideas on how to treat the extensionality axiom as a theory axiom,
ideas we have yet to explore. Mathias Fleury helped us set up regression tests
for Zipperposition. Ahmed Bhayat, Tomer Libal, and Enrico Tassi shared their
insights on higher-order unification. Andrei Popescu and Dmitriy Traytel
explained the terminology surrounding the $\lambda$-calculus. Haniel Barbosa,
Daniel El Ouraoui, Pascal Fontaine, Visa Nummelin, and Hans-Jörg Schurr were
involved in many stimulating discussions. Christoph Weidenbach made this
collaboration possible. Ahmed Bhayat, Wan Fokkink, Mark Summerfield, and the
anonymous reviewers suggested several textual improvements. The maintainers of
StarExec let us use their service for the evaluation. We thank them all.
Bentkamp, Blanchette, and Vukmirović’s research has received funding from the
European Research Council (ERC) under the European Union’s Horizon 2020
research and innovation program (grant agreement No. 713999, Matryoshka).
Bentkamp and Blanchette also benefited from the Netherlands Organization for
Scientific Research (NWO) Incidental Financial Support scheme. Blanchette has
received funding from the NWO under the Vidi program (project No.
016.Vidi.189.037, Lean Forward).

## References

  * (1) Andrews, P.B.: Resolution in type theory.  J. Symb. Log. 36(3), 414–432 (1971)
  * (2) Andrews, P.B.: On connections and higher-order logic.  J. Autom. Reason. 5(3), 257–291 (1989)
  * (3) Andrews, P.B.: Classical type theory.  In: J.A. Robinson, A. Voronkov (eds.) Handbook of Automated Reasoning, vol. II, pp. 965–1007. Elsevier and MIT Press (2001)
  * (4) Andrews, P.B., Bishop, M., Issar, S., Nesmith, D., Pfenning, F., Xi, H.: TPS: A theorem-proving system for classical type theory.  J. Autom. Reason. 16(3), 321–353 (1996)
  * (5) Avenhaus, J., Denzinger, J., Fuchs, M.: DISCOUNT: A system for distributed equational deduction.  In: J. Hsiang (ed.) RTA-95, _LNCS_ , vol. 914, pp. 397–402. Springer (1995)
  * (6) Bachmair, L., Ganzinger, H.: Rewrite-based equational theorem proving with selection and simplification.  J. Log. Comput. 4(3), 217–247 (1994)
  * (7) Bachmair, L., Ganzinger, H.: Resolution theorem proving.  In: J.A. Robinson, A. Voronkov (eds.) Handbook of Automated Reasoning, vol. I, pp. 19–99. Elsevier and MIT Press (2001)
  * (8) Backes, J., Brown, C.E.: Analytic tableaux for higher-order logic with choice.  J. Autom. Reason. 47(4), 451–479 (2011)
  * (9) Barbosa, H., Reynolds, A., Ouraoui, D.E., Tinelli, C., Barrett, C.W.: Extending SMT solvers to higher-order logic.  In: P. Fontaine (ed.) CADE-27, _LNCS_ , vol. 11716, pp. 35–54. Springer (2019)
  * (10) Bentkamp, A., Blanchette, J., Cruanes, S., Waldmann, U.: Superposition for lambda-free higher-order logic.  arXiv preprint arXiv:2005.02094v1 (2020).  https://arxiv.org/abs/2005.02094v1
  * (11) Bentkamp, A., Blanchette, J., Tourret, S., Vukmirović, P., Waldmann, U.: Superposition with lambdas.  In: P. Fontaine (ed.) CADE-27, _LNCS_ , vol. 11716, pp. 55–73. Springer (2019)
  * (12) Bentkamp, A., Blanchette, J.C., Cruanes, S., Waldmann, U.: Superposition for lambda-free higher-order logic.  In: D. Galmiche, S. Schulz, R. Sebastiani (eds.) IJCAR 2018, _LNCS_ , vol. 10900, pp. 28–46. Springer (2018)
  * (13) Benzmüller, C.: Extensional higher-order paramodulation and RUE-resolution.  In: H. Ganzinger (ed.) CADE-16, _LNCS_ , vol. 1632, pp. 399–413. Springer (1999)
  * (14) Benzmüller, C., Kohlhase, M.: Extensional higher-order resolution.  In: C. Kirchner, H. Kirchner (eds.) CADE-15, _LNCS_ , vol. 1421, pp. 56–71. Springer (1998)
  * (15) Benzmüller, C., Miller, D.: Automation of higher-order logic.  In: J.H. Siekmann (ed.) Computational Logic, _Handbook of the History of Logic_ , vol. 9, pp. 215–254. Elsevier (2014)
  * (16) Benzmüller, C., Paulson, L.C.: Multimodal and intuitionistic logics in simple type theory.  Log. J. IGPL 18(6), 881–892 (2010)
  * (17) Benzmüller, C., Sultana, N., Paulson, L.C., Theiss, F.: The higher-order prover Leo-II.  J. Autom. Reason. 55(4), 389–404 (2015)
  * (18) Bhayat, A., Reger, G.: Restricted combinatory unification.  In: P. Fontaine (ed.) CADE-27, _LNCS_ , vol. 11716, pp. 74–93. Springer (2019)
  * (19) Bhayat, A., Reger, G.: A combinator-based superposition calculus for higher-order logic.  In: N. Peltier, V. Sofronie-Stokkermans (eds.) IJCAR 2020, Part I, _LNCS_ , vol. 12166, pp. 278–296. Springer (2020)
  * (20) Blanchette, J.C., Böhme, S., Popescu, A., Smallbone, N.: Encoding monomorphic and polymorphic types.  Log. Meth. Comput. Sci. 12(4) (2016)
  * (21) Blanchette, J.C., Paskevich, A.: TFF1: The TPTP typed first-order form with rank-1 polymorphism.  In: M.P. Bonacina (ed.) CADE-24, _LNCS_ , vol. 7898, pp. 414–420. Springer (2013)
  * (22) Blanqui, F., Jouannaud, J.P., Rubio, A.: The computability path ordering.  Log. Meth. Comput. Sci. 11(4) (2015)
  * (23) Böhme, S., Nipkow, T.: Sledgehammer: Judgement Day.  In: J. Giesl, R. Hähnle (eds.) IJCAR 2010, _LNCS_ , vol. 6173, pp. 107–121. Springer (2010)
  * (24) Brown, C.E.: Satallax: An automatic higher-order prover.  In: B. Gramlich, D. Miller, U. Sattler (eds.) IJCAR 2012, _LNCS_ , vol. 7364, pp. 111–117. Springer (2012)
  * (25) de Bruijn, N.G.: Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church–Rosser theorem.  Indag. Math 75(5), 381–392 (1972)
  * (26) Cervesato, I., Pfenning, F.: A linear spine calculus.  J. Log. Comput. 13(5), 639–688 (2003)
  * (27) Cruanes, S.: Extending superposition with integer arithmetic, structural induction, and beyond.  Ph.D. thesis, École polytechnique (2015)
  * (28) Cruanes, S.: Superposition with structural induction.  In: C. Dixon, M. Finger (eds.) FroCoS 2017, _LNCS_ , vol. 10483, pp. 172–188. Springer (2017)
  * (29) Czajka, Ł., Kaliszyk, C.: Hammer for Coq: Automation for dependent type theory.  J. Autom. Reason. 61(1-4), 423–453 (2018)
  * (30) Dowek, G.: Higher-order unification and matching.  In: J.A. Robinson, A. Voronkov (eds.) Handbook of Automated Reasoning, vol. II, pp. 1009–1062. Elsevier and MIT Press (2001)
  * (31) Fitting, M.: Types, Tableaus, and Gödel’s God.  Kluwer (2002)
  * (32) Ganzinger, H., Stuber, J.: Superposition with equivalence reasoning and delayed clause normal form transformation.  Information and Computation 199(1–2), 3–23 (2005)
  * (33) Gordon, M.J.C., Melham, T.F. (eds.): Introduction to HOL: A Theorem Proving Environment for Higher Order Logic.  Cambridge University Press (1993)
  * (34) Gupta, A., Kovács, L., Kragl, B., Voronkov, A.: Extensional crisis and proving identity.  In: F. Cassez, J. Raskin (eds.) ATVA 2014, _LNCS_ , vol. 8837, pp. 185–200. Springer (2014)
  * (35) Henkin, L.: Completeness in the theory of types.  J. Symb. Log. 15(2), 81–91 (1950)
  * (36) Huet, G.P.: A mechanization of type theory.  In: N.J. Nilsson (ed.) IJCAI-73, pp. 139–146. William Kaufmann (1973)
  * (37) Huet, G.P.: A unification algorithm for typed lambda-calculus.  Theor. Comput. Sci. 1(1), 27–57 (1975)
  * (38) Jensen, D.C., Pietrzykowski, T.: Mechanizing $\omega$-order type theory through unification.  Theor. Comput. Sci. 3(2), 123–171 (1976)
  * (39) Jouannaud, J.P., Rubio, A.: Rewrite orderings for higher-order terms in eta-long beta-normal form and recursive path ordering.  Theor. Comput. Sci. 208(1–2), 33–58 (1998)
  * (40) Jouannaud, J.P., Rubio, A.: Polymorphic higher-order recursive path orderings.  J. ACM 54(1), 2:1–2:48 (2007)
  * (41) Kaliszyk, C., Sutcliffe, G., Rabe, F.: TH1: The TPTP typed higher-order form with rank-1 polymorphism.  In: P. Fontaine, S. Schulz, J. Urban (eds.) PAAR-2016, _CEUR Workshop Proceedings_ , vol. 1635, pp. 41–55. CEUR-WS.org (2016)
  * (42) Kaliszyk, C., Urban, J.: HOL(y)Hammer: Online ATP service for HOL Light.  Math. Comput. Sci. 9(1), 5–22 (2015)
  * (43) Kamin, S., Lévy, J.J.: Two generalizations of the recursive path ordering.  Unpublished manuscript, University of Illinois (1980)
  * (44) Kőnig, D.: Über eine Schlussweise aus dem Endlichen ins Unendliche.  Acta Sci. Math. (Szeged) 3499/2009(3:2–3), 121–130 (1927)
  * (45) Knuth, D.E., Bendix, P.B.: Simple word problems in universal algebras.  In: J. Leech (ed.) Computational Problems in Abstract Algebra, pp. 263–297. Pergamon Press (1970)
  * (46) Kohlhase, M.: Higher-order tableaux.  In: P. Baumgartner, R. Hähnle, J. Posegga (eds.) TABLEAUX ’95, _LNCS_ , vol. 918, pp. 294–309. Springer (1995)
  * (47) Konrad, K.: HOT: A concurrent automated theorem prover based on higher-order tableaux.  In: J. Grundy, M.C. Newey (eds.) TPHOLs ’98, _LNCS_ , vol. 1479, pp. 245–261. Springer (1998)
  * (48) Kovács, L., Voronkov, A.: First-order theorem proving and Vampire.  In: N. Sharygina, H. Veith (eds.) CAV 2013, _LNCS_ , vol. 8044, pp. 1–35. Springer (2013)
  * (49) Libal, T.: Regular patterns in second-order unification.  In: A.P. Felty, A. Middeldorp (eds.) CADE-25, _LNCS_ , vol. 9195, pp. 557–571. Springer (2015)
  * (50) Lindblad, F.: A focused sequent calculus for higher-order logic.  In: S. Demri, D. Kapur, C. Weidenbach (eds.) IJCAR 2014, _LNCS_ , vol. 8562, pp. 61–75. Springer (2014)
  * (51) Mayr, R., Nipkow, T.: Higher-order rewrite systems and their confluence.  Theor. Comput. Sci. 192(1), 3–29 (1998)
  * (52) Meng, J., Paulson, L.C.: Translating higher-order clauses to first-order clauses.  J. Autom. Reason. 40(1), 35–60 (2008)
  * (53) Miller, D.: A logic programming language with lambda-abstraction, function variables, and simple unification.  J. Log. Comput. 1(4), 497–536 (1991)
  * (54) Paulson, L.C., Blanchette, J.C.: Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers.  In: G. Sutcliffe, S. Schulz, E. Ternovska (eds.) IWIL-2010, _EPiC_ , vol. 2, pp. 1–11. EasyChair (2012)
  * (55) Robinson, J.: Mechanizing higher order logic.  In: B. Meltzer, D. Michie (eds.) Machine Intelligence, vol. 4, pp. 151–170. Edinburgh University Press (1969)
  * (56) Robinson, J.: A note on mechanizing higher order logic.  In: B. Meltzer, D. Michie (eds.) Machine Intelligence, vol. 5, pp. 121–135. Edinburgh University Press (1970)
  * (57) Schulz, S.: E - a brainiac theorem prover.  AI Commun. 15(2-3), 111–126 (2002)
  * (58) Schulz, S.: Fingerprint indexing for paramodulation and rewriting.  In: B. Gramlich, D. Miller, U. Sattler (eds.) IJCAR 2012, _LNCS_ , vol. 7364, pp. 477–483. Springer (2012)
  * (59) Schulz, S., Cruanes, S., Vukmirovic, P.: Faster, higher, stronger: E 2.3.  In: P. Fontaine (ed.) CADE-27, _LNCS_ , vol. 11716, pp. 495–507. Springer (2019)
  * (60) Snyder, W.: Higher order $E$-unification.  In: M.E. Stickel (ed.) CADE-10, _LNCS_ , vol. 449, pp. 573–587. Springer (1990)
  * (61) Snyder, W., Gallier, J.H.: Higher-order unification revisited: Complete sets of transformations.  J. Symb. Comput. 8(1/2), 101–140 (1989)
  * (62) Steen, A., Benzmüller, C.: The higher-order prover Leo-III.  In: D. Galmiche, S. Schulz, R. Sebastiani (eds.) IJCAR 2018, _LNCS_ , vol. 10900, pp. 108–116. Springer (2018)
  * (63) Sutcliffe, G.: The TPTP problem library and associated infrastructure—from CNF to TH0, TPTP v6.4.0.  J. Autom. Reason. 59(4), 483–502 (2017)
  * (64) Sutcliffe, G., Benzmüller, C., Brown, C.E., Theiss, F.: Progress in the development of automated theorem proving for higher-order logic.  In: R.A. Schmidt (ed.) CADE-22, _LNCS_ , vol. 5663, pp. 116–130. Springer (2009)
  * (65) Urban, J., Rudnicki, P., Sutcliffe, G.: ATP and presentation service for Mizar formalizations.  J. Autom. Reason. 50(2), 229–241 (2013)
  * (66) Vukmirović, P., Bentkamp, A., Nummelin, V.: Efficient full higher-order unification.  In: Z.M. Ariola (ed.) FSCD 2020, _LIPIcs_ , vol. 167, pp. 5:1–5:17. Schloss Dagstuhl—Leibniz-Zentrum für Informatik (2020)
  * (67) Vukmirović, P., Blanchette, J.C., Cruanes, S., Schulz, S.: Extending a brainiac prover to lambda-free higher-order logic.  In: T. Vojnar, L. Zhang (eds.) TACAS 2019, _LNCS_ , vol. 11427, pp. 192–210. Springer (2019)
  * (68) Vukmirović, P., Nummelin, V.: Boolean reasoning in a higher-order superposition prover.  In: Practical Aspects of Automated Reasoning (PAAR 2020) (2020)
  * (69) Waldmann, U., Tourret, S., Robillard, S., Blanchette, J.: A comprehensive framework for saturation theorem proving.  In: N. Peltier, V. Sofronie-Stokkermans (eds.) IJCAR 2020, Part I, _LNCS_ , vol. 12166, pp. 316–334. Springer (2020)