for the implementation of FALSEELIM, BOOLRW, FORALLRW, EXISTSRW, and all HOIST rules.

The implementation of oSup relies heavily on BOOLSIMP, and we keep this rule as the basis of our Boolean simplification machinery. As a result, BOOLRW can be reduced to two cases: (1) all arguments $\bar{s}_n$ of $u = h\bar{s}_n$ are variable-headed terms, and thus we must unify $s_i$ with all combinations of $\top$ and $\bot$; or (2) either $u = s \not\approx t$ or $u = s \not\sqsubseteq t$, and thus we must compute the unifiers of $s$ and $t$.

As in the implementation of $\lambda$Sup, we approximate fluid terms as terms that are either nonground $\lambda$-expressions or terms of the form $x\bar{s}_n$ with $n > 0$. Two slight, accidental discrepancies are that we also count variable occurrences below quantifiers as deep and perform EFACT inferences even if the maximal literal is selected. Since we expect FLUIDBOOLHOIST and FLUIDLOOBHOIST to be highly explosive, we penalize them and all of their offspring. In addition to various $\lambda$Sup extensions [10, Sect. 5], we also use all the rules for Boolean reasoning described by Vukmirović and Nummelin [39] except for the Boolean $\mathbf{BoolEF}$ rules. The $\mathbf{BoolEF}$ rules have been removed from Zipperposition because they did not seem to improve the prover's performance.

Our implementation is a graceful extension of oSup. For the rules EQHOIST, NEQHOIST, FORALLHOIST, and EXISTSHOIST, if the subterm $u$ is not variable-headed, there is an obvious most general unifier, which allows us to avoid invoking the unification procedure and to generate the conclusion directly, as in oSup.

# 6 Evaluation

We evaluate our implementation and compare it with other higher-order provers. Our experiments were performed on StarExec Miami servers equipped with Intel Xeon E5-2620 v4 CPUs clocked at 2.10 GHz. We used all 2606 TH0 theorems from the TPTP 7.3.0 library [35] and 1253 "Judgment Day" problems [15] generated using Sledgehammer (SH) [32] as our benchmark set. An archive containing the benchmarks and the raw evaluation results is publicly available.<fnref n="2" /> We divide the evaluation in two parts: evaluation of the calculus rules and comparison with other higher-order provers.

**Calculus Evaluation.** In this first part, we evaluate selected parameters of Zipperposition by varying only the studied parameter in a fixed well-performing configuration. This base configuration disables axioms (CHOICE) and (EXT) and the FLUID- rules. It uses the unification procedure of Vukmirović et al. [38] in its complete variant—i.e., the variant that produces a complete set of unifiers. It uses none of the early Boolean rules described by Vukmirović and Nummelin [39]. The preprocessor $Q_{\mathfrak{S}}$ is disabled as well. All of the completeness-preserving simplification rules described in Sect. 3.7 are enabled, except for the simplifying BOOLHOIST (combined with LOOBHOIST). The configuration uses immediate clausification. We set the CPU time limit to 30 s in all three experiments.

In the first experiment, we assess the overhead incurred by the FLUID- rules. These rules unify with a term whose head is a fresh variable. Thus, we expected that they needed to be tightly controlled to achieve good performance. To test our hypothesis, we simultaneously modified the parameters of these three rules. In Fig. 1, the *off* mode simply disables the rules, the *pragmatic* mode uses a terminating incomplete unification algorithm (the pragmatic variant of Vukmirović et al. [38]), and the *complete* mode uses a complete unification algorithm.

<footnote n="2">² https://doi.org/10.5281/zenodo.4534759</footnote>
The results show that disabling FLUID- rules altogether achieves the best performance. When the complete variant of the unification algorithm is used, inferences are scheduled in a queue designed to postpone explosive inferences [10, Sect. 6]. In contrast, in the pragmatic variant, a terminating algorithm is employed, but still flooding the proof state with FLUID- rules conclusions severely hinders performance. Even though enabling FLUID- rules degrades performance overall, *complete* finds 35 proofs not found by *off*, and *pragmatic* finds 22 proofs not found by *off*. On Sledgehammer benchmarks, this effect is much weaker, likely because the Sledgehammer benchmarks require less higher-order reasoning: *complete* finds only one new proof over *off*, and *pragmatic* finds only four.

In the second experiment, we explore the clausification methods introduced at the end of Sect. 3: *inner* delayed clausification, which relies on the core calculus to reason about logical symbols; *outer* delayed clausification, which clausifies step-by-step guided by the outermost logical symbols; and *immediate* clausification, which eagerly applies a monolithic clausification algorithm when encountering top-level logical symbols. The modes *inner* and *outer* employ oSup's RENAME rule, which renames Boolean terms headed by logical symbols using a Tseitin-like transformation if they occur at least four times in the proof state. Vukmirović and Nummelin [39] observed that *outer* clausification can greatly help prove higher-order problems, and we expected it to perform well for our calculus, too. The results are shown in Fig. 2. The results confirm our hypothesis: The *outer* mode outperforms *immediate* on both TPTP and Sledgehammer benchmarks. The *inner* mode performs worst, but on Sledgehammer benchmarks, it proves 17 problems beyond the reach of the other two. Looking at the proofs found by *inner*, we observed a pattern: in many cases (e.g., for the benchmarks *prob_295_3252866_1*, *prob_296_3252872_1*, *prob_366_5338-318_1*, *prob_419_5371618_1*) the problems contain axioms of the form $\phi \to \psi$. When such axioms are not clausified, superposition and demodulation can often reduce either $\phi$ or $\psi$ to $\top$ or $\bot$. At this point, simplification rules will act on the resulting term, simplifying it enough that the proof can easily be found.

In the third experiment, we investigate the effect of axiom (CHOICE), which is necessary to achieve refutational completeness. To evaluate (CHOICE), we either disabled it in a configuration labeled *off* or set the axiom's penalty *p* to different values. In Zipperposition, penalties are propagated through inference and simplification rules and are used to increase the heuristic weight of clauses, postponing the selection of penalized clauses. The results are shown in Fig. 3. As expected, disabling (CHOICE), or at least penalizing it heavily, improves performance. Yet enabling (CHOICE) can be crucial: For 19 TPTP problems, the proofs are found when (CHOICE) is enabled and *p* = 4, but not when the rule is disabled. On Sledgehammer problems, this effect is weaker, with only two new problems proved for *p* = 4.

**Prover Comparison.** In this second part, we compare Zipperposition's performance with other higher-order provers. Like at CASC-J10, the wall-clock time limit was 120 s, the CPU time limit was 960 s, and the provers were run on StarExec Miami. We used the following versions of all systems that took part in the THF division: CVC4 1.8 [5], Leo-III 1.5.2 [34], Satallax 3.5 [16], and Vampire 4.5 [13]. The developers of Vampire have informed us that its higher-order schedule is optimized for running on a single core. As a result, the prover suffers some degradation of performance when running on multiple cores. We evaluate both the version of Zipperposition that took part in CASC-J10 (Zip) and the updated version of Zipperposition that supports our new calculus (New Zip). Zip's portfolio of prover configurations is based on $\lambda$Sup and techniques described by Vukmirović and Nummelin [39]. New Zip's portfolio is specially designed for our new calculus and optimized for TPTP problems.
<table><caption>Fig. 1 Evaluation of FLUID- rules</caption><thead><tr><th></th><th>off</th><th>pragmatic</th><th>complete</th></tr></thead><tbody><tr><th>TPTP</th><td><strong>1642</strong></td><td>1591</td><td>1619</td></tr><tr><th>SH</th><td><strong>467</strong></td><td>431</td><td>437</td></tr></tbody></table>

<table><caption>Fig. 2 Evaluation of clausification method</caption><thead><tr><th></th><th>inner</th><th>outer</th><th>immediate</th></tr></thead><tbody><tr><th>TPTP</th><td>1323</td><td><strong>1670</strong></td><td>1642</td></tr><tr><th>SH</th><td>406</td><td><strong>470</strong></td><td>467</td></tr></tbody></table>

<table><caption>Fig. 3 Evaluation of axiom (CHOICE)</caption><thead><tr><th></th><th>off</th><th>p = 64</th><th>p = 16</th><th>p = 4</th><th>p = 1</th></tr></thead><tbody><tr><th>TPTP</th><td><strong>1642</strong></td><td>1617</td><td>1613</td><td>1615</td><td>1594</td></tr><tr><th>SH</th><td><strong>467</strong></td><td>458</td><td>458</td><td>459</td><td>445</td></tr></tbody></table>

<table><caption>Fig. 4 Evaluation of all competitive higher-order provers</caption><thead><tr><th></th><th>TPTP</th><th>ofSH</th><th>SH</th></tr></thead><tbody><tr><th>CVC4</th><td>1796</td><td>680</td><td>619</td></tr><tr><th>Leo-III</th><td>2104</td><td>681</td><td>621</td></tr><tr><th>Satallax</th><td>2162</td><td>573</td><td>587</td></tr><tr><th>Vampire</th><td>2131</td><td>692</td><td>681</td></tr><tr><th>Zip</th><td>2301</td><td><strong>734</strong></td><td><strong>736</strong></td></tr><tr><th>New Zip</th><td><strong>2320</strong></td><td>724</td><td>720</td></tr><tr><th>Leo-III-uncoop</th><td>1619</td><td>223</td><td>240</td></tr><tr><th>Satallax-uncoop</th><td>2038</td><td>467</td><td>482</td></tr><tr><th>Zip-uncoop</th><td>2223</td><td>667</td><td>673</td></tr><tr><th>New Zip-uncoop</th><td>2236</td><td>640</td><td>644</td></tr></tbody></table>

The portfolio does not contain a complete configuration, but the combination of configurations is close to complete. Leo-III, Satallax, and Zipperposition are cooperative theorem provers: They invoke a backend reasoner to finish the proof attempt. To test the performance of their calculi in isolation, we also invoked them in uncooperative mode. To assess the performance of Boolean reasoning, we used Sledgehammer benchmarks generated both with native Booleans (SH) and with an encoding into Boolean-free higher-order logic (ofSH). For technical reasons, the encoding also performs λ-lifting, but this minor transformation should have little impact on results [10, Sect. 7].

The results are shown in Fig. 4. The updated version of New Zip beats Zip on TPTP problems but lags behind Zip on Sledgehammer benchmarks as we have yet to further explore more general heuristics that work well with our new calculus. The Sledgehammer benchmarks fail to demonstrate the superiority of native Booleans reasoning compared with an encoding, and in fact CVC4 and Leo-III perform dramatically better on the encoded Boolean problems, suggesting that there is room for tuning.

The uncooperative versions of Zipperposition show strong performance on both benchmark sets. This suggests that, with thorough parameter tuning, higher-order superposition outperforms tableaux, which had been the state of the art in higher-order reasoning for a decade. Without backend reasoners, Zipperposition proves fewer Sledgehammer problems than Vampire. We conjecture that implementing our calculus in Vampire or E would remove the need for a backend reasoner and make the calculus even more useful in practice.

## 7 Conclusion

We have created a superposition calculus for higher-order logic and proved it sound and refutationally complete. Most of the key ideas have been developed in previous work by us and colleagues, but combining them in the right way has been challenging. A key idea was to Qₚₚ-normalize away inconvenient terms.
Unlike earlier refutationally complete calculi for full higher-order logic based on resolution or paramodulation, our calculus employs a term order, which restricts the proof search, and a redundancy criterion, which can be used to add various simplification rules while keeping refutational completeness. These two mechanisms are undoubtedly major factors in the success of first-order superposition, and it is very fortunate that we could incorporate both in a higher-order calculus. An alternative calculus with the same two mechanisms could be achieved by combining oSup with Bhayat and Reger’s combinatory superposition [12]. The article on $\Lambda$Sup [10, Sect. 8] discusses related work in more detail.

The evaluation results show that our calculus is an excellent basis for higher-order theorem proving. In future work, we want to experiment further with the different parameters of the calculus (for example, with Boolean subterm selection heuristics) and implement it in a state-of-the-art prover such as E.

**Acknowledgment.** Uwe Waldmann provided advice and carefully checked the completeness proof. Visa Nummelin led the design of the oSup calculus, which was a crucial stepping stone for this work. Simon Cruanes helped us with the implementation. Martin Desharnais generated (and regenerated) the Sledgehammer benchmarks. Ahmed Bhayat explained the higher-order Vampire schedule and suggested textual improvements. Christoph Benzmüller provided us insight into the pitfalls of higher-order reasoning. Alexander Steen explained the details of Leo-III scheduling. Geoff Sutcliffe let us use StarExec Miami for our experiments. Simon Cruanes, Herman Geuvers, Mathias Fleury, Nicolas Peltier, Giles Reger, Mark Summerfield, and the anonymous reviewers suggested textual improvements. 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's research has received funding from a Chinese Academy of Sciences President's International Fellowship for Postdoctoral Researchers (grant No. 2021PT0015). Blanchette's research has received funding from the Netherlands Organization for Scientific Research (NWO) under the Vidi program (project No. 016.Vidi.189.037, Lean Forward).

## References

1. Andrews, P.B.: On connections and higher-order logic. J. Autom. Reason. 5(3), 257–291 (1989)

2. Bachmair, L., Ganzinger, H.: Rewrite-based equational theorem proving with selection and simplification. J. Log. Comput. 4(3), 217–247 (1994)

3. 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)

4. Bachmair, L., Ganzinger, H., Lynch, C., Snyder, W.: Basic paramodulation and superposition. In: D. Kapur (ed.) CADE-11, LNCS, vol. 607, pp. 462–476. Springer (1992)

5. Barrett, C.W., Conway, C.L., Deters, M., Hadarean, L., Jovanovic, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: CAV, LNCS, vol. 6806, pp. 171–177. Springer (2011)

6. Benanav, D.: Simultaneous paramodulation. In: M.E. Stickel (ed.) CADE-10, LNCS, vol. 449, pp. 442–455. Springer (1990)

7. Bentkamp, A.: Superposition for higher-order logic. Ph.D. thesis, Vrije Universiteit Amsterdam (2021)

8. Bentkamp, A., Blanchette, J., Cruanes, S., Waldmann, U.: Superposition for lambda-free higher-order logic. Log. Meth. Comput. Sci. 17(2), 1:1–1:38 (2021)

9. Bentkamp, A., Blanchette, J., Tourret, S., Vukmirović, P.: Superposition for full higher-order logic. In: A. Platzer, G. Sutcliffe (eds.) CADE-28, LNCS, vol. 12699, pp. 396–412. Springer (2021)

10. Bentkamp, A., Blanchette, J., Tourret, S., Vukmirović, P., Waldmann, U.: Superposition with lambdas. J. Autom. Reason. 65, 893–940 (2021)

11. Benzmüller, C., Paulson, L.C., Theiss, F., Fietzke, A.: LEO-II—A cooperative automatic theorem prover for higher-order logic. In: A. Armando, P. Baumgartner, G. Dowek (eds.) IJCAR 2008, LNCS, vol. 5195, pp. 162–170. Springer (2008)
12. Bhayat, A., Reger, G.: Set of support for higher-order reasoning. In: B. Konev, J. Urban, P. Rümmer (eds.) PAAR-2018, *CEUR Workshop Proceedings*, vol. 2162, pp. 2–16. CEUR-WS.org (2018)

13. 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)

14. Blanqui, F., Jouannaud, J.P., Rubio, A.: The computability path ordering. Log. Meth. Comput. Sci. 11(4), 2–98 (2015)

15. 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)

16. 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)

17. Cervesato, I., Pfenning, F.: A linear spine calculus. J. Log. Comput. 13(5), 639–688 (2003)

18. Fitting, M.: Types, Tableaus, and Gödel's God. Kluwer (2002)

19. Ganzinger, H., Stuber, J.: Superposition with equivalence reasoning and delayed clause normal form transformation. Inform. Comput. 199(1–2), 3–23 (2005)

20. Gordon, M.J.C., Melham, T.F. (eds.): Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press (1993)

21. Huet, G.P.: A mechanization of type theory. In: N.J. Nilsson (ed.) IJCAI-73, pp. 139–146. William Kaufmann (1973)

22. Huet, G.P.: A unification algorithm for typed lambda-calculus. Theor. Comput. Sci. 1(1), 27–57 (1975)

23. Jensen, D.C., Pietrzykowski, T.: Mechanizing ω-order type theory through unification. Theor. Comput. Sci. 3(2), 123–171 (1976)

24. 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)

25. 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)

26. König, D.: Über eine Schlussweise aus dem Endlichen ins Unendliche. Acta Sci. Math. (Szeged) 3499/2009(3:2–3), 121–130 (1927)

27. Kotelnikov, E., Kovács, L., Suda, M., Voronkov, A.: A clausal normal form translation for FOOL. In: C. Benzmüller, G. Sutcliffe, R. Rojas (eds.) GCAI 2016, EPiC, vol. 41, pp. 53–71. EasyChair (2016)

28. Ludwig, M., Waldmann, U.: An extension of the Knuth-Bendix ordering with LPO-like properties. In: N. Dershowitz, A. Voronkov (eds.) LPAR-14, LNCS, vol. 4790, pp. 348–362. Springer (2007)

29. Mayr, R., Nipkow, T.: Higher-order rewrite systems and their confluence. Theor. Comput. Sci. 192(1), 3–29 (1998)

30. Nonnengart, A., Weidenbach, C.: Computing small clause normal forms. In: Handbook of Automated Reasoning, pp. 335–367. Elsevier and MIT Press (2001)

31. Nummelin, V., Bentkamp, A., Tourret, S., Vukmirović, P.: Superposition with first-class Booleans and inprocessing clausification (technical report). https://matryoshka-project.github.io/pubs/boolsup_report.pdf

32. 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)

33. Schulz, S.: E - a brainiac theorem prover. AI Commun. 15(2-3), 111–126 (2002)

34. 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)

35. 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)

36. Tseitin, G.: On the complexity of derivation in propositional calculus. In: Automation of Reasoning: Classical Papers on Computational Logic, vol. 2, pp. 466–483. Springer (1983)

37. Vukmirović, P., Bentkamp, A., Blanchette, J., Cruanes, S., Nummelin, V., Tourret, S.: Making higher-order superposition work. In: A. Platzer, G. Sutcliffe (eds.) CADE-28, LNCS. Springer (2021)

38. 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)

39. Vukmirović, P., Nummelin, V.: Boolean reasoning in a higher-order superposition prover. In: PAAR-2020, CEUR Workshop Proceedings, vol. 2752, pp. 148–166. CEUR-WS.org (2020)

40. 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)