Next, we refine the model-guided prover into a locking prover that temporarily locks away A-formulas that are redundant locally w.r.t. some J but not globally. means that C ← A is "locally redundant" in interpretations J ⊇ B. The function - erases the locks: -L = {C | (B, C) ∈ L for some B}. Initial states have the form (J,N, ∅), where N ⊆ **F**. The *locking prover* is defined by these two rules: The states are triples (J, N ,L), with L⊆Pfin(**A**)×**AF**. Intuitively,(B, C←A)∈ L

We note that =⇒L-derivations refine =⇒MG-derivations, with states (J, N ,L) mapped to (J, N ∪ -L).

Locking can cause incompleteness, because an A-formula can be locally redundant at every point in the derivation and yet not be so at any limit point, thereby breaking local saturation. For example, if we have derived p(x) ← {¬vk} for every k, then p(c) is locally redundant in any J that contains ¬vk. For the models Ji = {v1,..., vi, ¬vi+1,...}, the clause p(c) would always be locally redundant and ignored. Yet p(c) might not be locally redundant at the unique limit point J = **V**. We could rule out this counterexample by requiring that derivations are strongly fair—that is, every inference possible infinitely often must eventually be made redundant. However, we have found a counterexample showing that strong fairness does not ensure completeness [8, Example 46]. It would seem that this counterexample could arise with Vampire if the underlying SAT solver produces this specific sequence of interpretations.

Our solution is as follows.  To achieve fairness, we now consider N ∞, the A-formulas persistent in the unlocked subsequence (N j )j . By contrast, fairness of =⇒MG-derivations used N∞.

Definition 18. An =⇒L-derivation (Ji, Ni,Li)i is *fair* if either (1) ⊥ ∈ i Ni or (2) Ji |= (Ni)⊥ for infinitely many indices i and there exists a subsequence (J j )j converging to a limit point J such that *FInf*((N ∞)J ∪ ((lim supj→∞-L j)J \ -L∞)J) ⊆ i *FRed*I((Ni ∪-Li)J), where (N j )j and (L j )j correspond to (J j )j .

Fairness of an =⇒L-derivation implies fairness of the corresponding =⇒MGderivation. The condition on the sets L j ensures that inferences from A-formulas that are locked infinitely often, but not infinitely often with the same lock, are redundant at the limit point. In particular, if we know that each A-formula is locked at most finitely often, then lim supj→∞-L j = -L∞ and the inclusion in the definition above simplifies to *FInf*((N ∞)J) ⊆ i *FRed*I((Ni ∪ -Li)J).

## 6 AVATAR-Based Provers

AVATAR was unveiled in 2014 by Voronkov [22]. Since then, he and his colleagues studied many options and extensions [3, 17]. A second implementation, in Lean's super tactic, is due to Ebner [9]. Here we attempt to capture AVATAR's essence.

The abstract AVATAR-based prover we define in this section extends the locking prover L with a given clause procedure [13]. A-formulas are moved in turn from the passive to the active set, where inferences are performed. The heuristic for choosing the next *given* A-formula to move is guided by timestamps indicating when the A-formulas were derived, to ensure fairness.

Let **TAF** = **AF** × N be the set of *timestamped A-formulas*. Given N ⊆ **TAF**, we define N = {C | (C, t) ∈ N for some t}, and we overload existing notations to erase timestamps. Thus, N = N, N⊥ = N⊥, and so on. Note that we use a new set of calligraphic letters (e.g., C, N) to range over timestamped A-formulas and A-formulas sets. Using the saturation framework [23, Sect. 3], we lift (*SInf* , *SRed*) to a calculus (*TSInf* , *TSRed*) on **TAF** with the tiebreaker order > on timestamps, so that (C, t + k) ∈ *TSRed* F({(C, t)}) for any k > 0.

where A, P, and Q are respectively the sets of *active*, *passive*, and other (disabled or propositional) timestamped A-formulas, and L is the set of locked timestamped A-formulas such that (1) A⊥ = P⊥ = ∅, (2) A ∪ P is enabled in J, and (3) QJ ⊆ {⊥}. The *AVATAR-based prover* AV is defined as follows: A state is a tuple (J, A, P, Q, L) ∈ P(**A**) × P(**TAF**)3 × P(Pfin(**A**) × **TAF**),

There is also a LockP rule that is identical to LockA except that it starts in the state (J, A, P {(C ← A, t)}, Q, L). An AV-derivation is *well timestamped* if every A-formula introduced by a rule is assigned a unique timestamp.

Let (Ji, Ai, Pi, Qi, Li)i be an =⇒AV-derivation. It is easy to see that it refines the =⇒L-derivation (Ji, Ai ∪ Pi ∪ Qi, Li)i and that the saturation invariant *TSInf*(Ai) ⊆ *TSRed*I(Ai ∪ Pi ∪ Qi ∪ -Li) holds if A0 = ∅.

In contrast with nonsplitting provers, for AV, fairness w.r.t. formulas does not imply fairness w.r.t. inferences. A problematic scenario involves two premises C, D of an inference ι and four transitions repeated forever, possibly with other steps interleaved: Infer makes C active; Switch disables it; Infer makes D active; Switch disables it. Even though C and D are selected in a strongly fair fashion, ι is never performed. We need an even stronger fairness criterion.

Definition 19. An =⇒AV-derivation (Ji, Ai, Pi, Qi, Li)i is *fair* if (1) ⊥ ∈ i Qi or (2) Ji |= (Qi)⊥ for infinitely many indices i and there exists a subsequence (J j ) converging to a limit point J ∞ such that (3) lim infj→∞ *TSInf*(A j , P j ) = ∅ and (4) (lim supj→∞-L j)J \ -L∞J ⊆ i *FRed* F((Ai ∪ Pi ∪ Qi ∪ -Li)J).

Condition (3) ensures that all inferences involving passive A-formulas are redundant at the limit point. It would not suffice to require P ∞ = ∅ because A-formulas can move back and forth between A, P, and Q, as we just saw. Condition (4) is similar to the condition on locks in Definition 18. If the =⇒AVderivation is fair, the corresponding =⇒L-derivation is also fair.

Many selection strategies are combinations of basic strategies, such as choosing the smallest formula by weight or the oldest by age. We capture such strategies using selection orders -. Intuitively, C -D if the prover will always select C before D if both are present. We use two selection orders: -**TAF**, based on timestamps, must be followed infinitely often; -**F** must be followed otherwise. For the first one, we can use age defined so that (C, t) age (C , t ) if t<t .

Definition 20. Let X be a set. A *selection order* on X is an irreflexive and transitive relation such that {y | y x} is finite for all x ∈ X.

The intersection of two orders -1 and -2 corresponds to the nondeterministic alternation between them. The prover may choose either a -1-minimal or a -2-minimal A-formula, at its discretion.

To ensure completeness, we must restrict the inferences that the prover may perform; otherwise, it could derive infinitely many A-formulas with different assertions, causing it to switch between two branches of the split tree without making progress. Given N ⊆ **AF**, let N = {A | C ← A ∈ N for some C}.

Definition 21. A function F : P(**AF**) → P(**AF**) is *strongly finitary* if F(N ) and F(N ) \ N are finite for any N ⊆ **AF** such that N is finite.

Intuitively, a strongly finitary function F returns finitely many base formulas and finitely many new assertions, although it may return infinitely many Aformulas. Clearly, F(N ) is finite for any finite N ⊆ **AF**. If *FInf*(N) is finite for any finite N ⊆ **F**, then performing *SInf* -inferences is strongly finitary. Deterministic Split rules, such as AVATAR's, are also strongly finitary. We can lift a strongly finitary F to any N ⊆ **TAF** by taking F**TAF**(N) = F(N) × N. If F and G are strongly finitary, then so is N → F(N ) ∪ G(N ).

Simplification rules used by the prover must be restricted even more to ensure completeness, because they can lead to new splits and assertions. For example, simplifying p(x ∗ 0) ∨ p(x) to p(0) ∨ p(x) transforms an unsplittable clause into a splittable one. If simplifications were to produce infinitely many such clauses, the prover might split and switch models forever without making progress.

Definition 22. Let ≺ be a well-founded relation on **F**, and let be its reflexive closure. A function S : **AF** → P(**AF**) is a *strongly finitary simplification bound* for ≺ if N → C∈N S(C) is strongly finitary and C C for all C ∈ S(C).

The prover may simplify an A-formula C to C only if C ∈ S(C). It may also delete C. Strongly finitary simplification bounds are closed under unions, allowing the combination of simplification techniques based on ≺. For superposition, a natural choice for ≺ is the clause order. The key property of strongly finitary simplification bounds is that if we saturate a finite set of A-formulas w.r.t. simplifications, the saturation is also finite.

Example 23. Let **F** be the set of first-order clauses and S(C ←A) = {C ←A | C is a subclause of C and A ⊆ A}. Then S is a strongly finitary simplification bound. This S covers many simplification techniques, including elimination of duplicate literals, deletion of resolved literals, and subsumption resolution.

Example 24. If the Knuth–Bendix order [12] is used and all weights are positive, then S(C ← A) = {C ← A | C ≺ C and A ⊆ A} is a strongly finitary simplification bound. This can be used to cover demodulation.

Equipped with the above definitions, we introduce a fairness criterion that is more concrete and easier to apply than fairness of =⇒AV-derivations. We could refine AV further and use this criterion to show the completeness of an imperative procedure such as Voronkov's extended Otter loop [22, Fig. 3], thus showing that Vampire with AVATAR is complete if locking is sufficiently restricted.

Lemma 25. *Let* I *be a strongly finitary function, and let* S *be a strongly finitary simplification bound. Then a well-timestamped* =⇒AV*-derivation* (Ji, Ai, Pi, Qi, Li)i *is fair if all of the following conditions hold:*

#### 7 Application to Other Architectures

AVATAR may be the most natural application of our framework, but it is not the only one. Below we complete the picture by studying splitting without backtracking, labeled splitting, and SMT with quantifiers.

Splitting without Backtracking. Before AVATAR, Riazanov and Voronkov [20] had already experimented with splitting in Vampire in a lighter variant without backtracking. They based their work on ordered resolution O with selection [2]. Weidenbach [24, end of Sect. 4.5] independently outlined the same technique. The basic idea is to extend the signature Σ with a countable set P of nullary predicate symbols and to augment the base calculus with a binary splitting rule that replaces a -clause C ∨D with twoΣP-clauses C ∨p and D∨¬p. Riazanov and Voronkov require that the precedence ≺ makes all P-literals smaller than the Σ-literals. Binary splitting is then a simplification. They also extend the selection function of the base calculus to support P-literals. Their *parallel* selection function imitates as much as possible the original selection function. ΣP

The calculus OP is closely related to an instance of our framework. Let **F** be the set of Σ-clauses, with the empty clause as ⊥. Let O = (*FInf* , *FRed*) be the base calculus. We take **V** = P. Let LA = (*SInf* , *SRed*), whose name stands for *lightweight AVATAR*, be the induced splitting calculus. Lightweight AVATAR amounts to the splitting architecture Cruanes implemented in Zipperposition [7, Sect. 2.5]. Binary splitting can be realized in LA as a Split-like simplification

rule. The calculi OP and LA disagree slightly because OP's order ≺ can break ties using P-literals and because LA can detect unsatisfiability early using the Unsat rule. Despite its slightly weaker order, LA is tighter than OP in the sense that saturation w.r.t. OP implies saturation w.r.t. LA but not vice versa.

Labeled Splitting. Labeled splitting, as originally described by Fietzke and Weidenbach [10] and implemented in SPASS, is a first-order resolution-based calculus with binary splitting that traverses the split tree in a depth-first way, using an elaborate backtracking mechanism inspired by CDCL [15]. It works on states (Ψ, N ), where Ψ is a stack storing the current state of the split tree and N is a set of *labeled clauses*—clauses annotated with finite sets of natural numbers.

We model labeled splitting as an instance of the locking prover L based on the splitting calculus LS = (*SInf* , *SRed*) induced by the resolution calculus R = (*FInf* , *FRed*), where |= and |≈ are as in Example 2 and **V** = i∈N{li,ri,si}. A-clauses correspond to labeled clauses. Splits are identified by unique *split levels*. Given a split on C ∨ D with level k, lk ∈ *asn*(C) and rk ∈ *asn*(D) represent the left and right branches. In practice, the prover would dynamically extend *fml* to ensure that *fml*(lk) = C and *fml*(rk) = D.

When splitting, if we simply added ⊥ ← {¬lk, ¬rk}, we would always need to consider either C ← {lk} or D ← {rk}, depending on the interpretation. However, labeled splitting can undo splits when backtracking. Yet fairness would require us to perform inferences with either C or D even when labeled splitting would not. We solve this as follows. Let = ∼⊥. We introduce the variable sk ∈ *asn*() so that we can enable or disable the split. The StrongUnsat rule then knows that sk is true, but we can still switch to propositional models that disable both C and D. A-clauses are then split using the following binary variant of Split:

$$\frac{C \lor D \gets A}{\bot \gets \{\neg \mathbb{I}\_k, \neg \mathsf{r}\_k, \mathsf{s}\_k\} \quad C \gets A \cup \{\mathsf{l}\_k\} \quad D \gets A \cup \{\mathsf{r}\_k\}} \text{ SOFTSPLIT}$$

where C and D share no variables and k is the next split level. Unlike AVATAR, labeled splitting keeps the premise and might split it again with another level.

To emulate the original, the locking prover based on LS must repeatedly apply the following three steps in any order until saturation:

Switch is powerful enough to support all of Fietzke and Weidenbach's backtracking rules, but to explore the tree in the same order as they do, we must choose the new model carefully. If a left branch is closed, the model must be updated so as to disable the splits that were not used to close this branch and to enable the right branch. If a right branch is closed, the split must be disabled,

and the model must switch to the right branch of the closest enabled split above it with an enabled left branch. If a right branch is closed but there is no split above with an enabled left branch, the entire tree has been visited. Then, a propositional clause ⊥ ← A with A ⊆ i{si} is |=-entailed by the A-clause set, and StrongUnsat can finish the refutation by exploiting *fml*(si) = .

The above strategy helps achieve fairness, because it ensures that there exists exactly one limit point. It also uses locks in a well-behaved way. This means we can considerably simplify the notion of fairness for =⇒L-derivations and obtain a criterion that is almost identical to, but slightly more liberal than, Fietzke and Weidenbach's—thereby re-proving the completeness of labeled splitting.

For terminating derivations, their fairness criterion coincides with ours. For diverging derivations, Fietzke and Weidenbach construct a limit subsequence (Φ i, N i )i of the derivation (Φi, Ni)i and require that every persistent inference in it be made redundant, exactly as we do for =⇒L-derivations. The subsequence consists of all states that lie on the split tree's unique infinite branch. Locks are well behaved, with lim supj→∞-L j = -L∞, because with the strategy above, once an A-clause is enabled on the rightmost branch, it remains enabled forever. Our definition of fairness allows more subsequences, although this is difficult to exploit without bringing in all the theoretical complexity of AVATAR.

SMT with Quantifiers. Satisfiability modulo theories (SMT) solvers based on DPLL(T) [15] combine a SAT solver with theory solvers. In the classical setup, the theories are decidable, and the SMT solver is a decision procedure for the union of the theories. Some SMT solvers also support quantified formulas via instantiation at the expense of decidability.

Complete instantiation strategies have been developed for various fragments of first-order logic [11, 18, 19]. In particular, enumerative quantifier instantiation [18] is complete under some conditions. An SMT solver following such a strategy ought to be refutationally complete, but this has never been proved. Although SMT is quite different from the architectures considered above, we can instantiate our framework to show the completeness of an abstract SMT solver. The model-guided prover MG will provide a suitable starting point.

Let **F** be the set of first-order Σ-formulas. We represent the SMT solver's underlying SAT solver by the Unsat rule and complement it with an inference system *FInf* that includes rules for clausification outside quantifiers, theory reasoning, and instantiation. The clausification rules derive C and D from a premise C ∧ D, among others; the theory rules derive ⊥ from some Σ-formula set N such that N |= {⊥}, ignoring quantifiers; and the instantiation rules derive ϕ(u) from premises ∀x. ϕ(x), where u is a ground term. For *FRed*, we take an arbitrary instance of standard redundancy. Its only purpose is to split disjunctions destructively. We define the "theories with quantifiers" calculus TQ = (*FInf* , *FRed*). For |= and |≈, we use entailment in the supported theories including quantifiers.

We use the same approximation function as in AVATAR (Example 3). Let us call C ← A a *subunit* if C is not a disjunction. Whenever a (ground) disjunction C ∨D←A emerges, we immediately apply Split. This delegates clausal reasoning to the SAT solver. It then suffices to assume that TQ is complete for subunits.

Theorem 26 (Dynamic completeness). *Assume* TQ *is statically complete for subunit sets. Let* (Ji, Ni)i *be a fair* =⇒MG*-derivation based on* TQ*. If* N0 |= {⊥} *and* N∞ *contains only subunits, then* ⊥∈Nj *for some* j.

Like AVATAR-based provers, SMT solvers will typically not perform all *SInf* inferences, not even up to *SRed*I. Given a ≈ b← {v0}, b ≈ c← {v1}, a ≈ d← {v2}, c ≈ d ← {v3}, and a ≈ c ← {v4}, an SMT solver will find only one of the conflicts ⊥←{v0, v1, v4} or ⊥←{v2, v3, v4} but not both. For decidable theories, a practical fair strategy is to instantiate quantifiers only if no other rules are applicable.

Our mathematization of AVATAR and SMT with quantifiers exposes their dissimilarities. With SMT, splitting is mandatory, and there is no subsumption or simplification, locking, or active and passive sets. And of course, theory inferences are n-ary and quantifier instantiation is unary, whereas superposition is binary. Nevertheless, their completeness follows from the same principles.

# 8 Conclusion

Our framework captures splitting calculi and provers in a general way, independently of the base calculus. Users can conveniently derive a dynamic refutational completeness result for a splitting prover based on a given statically refutationally complete calculus. As we developed the framework, we faced some tension between constraining the SAT solver's behavior and the saturation prover's. It seemed preferable to constrain the prover, because the prover is typically easier to modify than an off-the-shelf SAT solver. To our surprise, we discovered counterexamples related to locking, formula selection, and simplification, which may affect Vampire's AVATAR implementation, depending on the SAT solver used. We proposed some restrictions, but alternatives could be investigated.

We found that labeled splitting can be seen as a variant of AVATAR where the SAT solver follows a strict strategy and propositional variables are not reused across branches. A benefit of the strict strategy is that locking preserves completeness. As for the relationship between AVATAR and SMT, there are some glaring differences, including that splitting is necessary to support disjunctions in SMT but fully optional in AVATAR. For future work, we could try to complete the picture by considering other related architectures [4–6, 14].

Acknowledgment. Petar Vukmirović greatly helped us design the abstract notions related to A-formulas. Giles Reger patiently explained AVATAR and revealed some of its secrets. Simon Cruanes did the same regarding lightweight AVATAR. Simon Robillard, Andrei Voronkov, Uwe Waldmann, Christoph Weidenbach discussed splitting with us. Haniel Barbosa, Pascal Fontaine, Andrew Reynolds, and Cesare Tinelli explained some fine points of SMT. Natarajan Shankar pointed us to his work on the Shostak procedure. Ahmed Bhayat, Mark Summerfield, Dmitriy Traytel, Petar Vukmirović, and the anonymous reviewers suggested textual improvements. We thank them all.

This 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). The research has also received funding from the Nederlandse Organisatie voor Wetenschappelijk Onderzoek (NWO) under the Vidi program (project No. 016.Vidi.189.037, Lean Forward).

## References

Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

# **Integer Induction in Saturation**

Petra Hozzov´a1 , Laura Kov´acs1 , and Andrei Voronkov2,3

1 TU Wien, Vienna, Austria

{petra.hozzova<EMAIL_ADDRESS><EMAIL_ADDRESS>2 University of Manchester, Manchester, UK 3 EasyChair, Manchester, UK

**Abstract.** Integers are ubiquitous in programming and therefore also in applications of program analysis and verification. Such applications often require some sort of inductive reasoning. In this paper we analyze the challenge of automating inductive reasoning with integers. We introduce inference rules for integer induction within the saturation framework of first-order theorem proving. We implemented these rules in the theorem prover Vampire and evaluated our work against other state-of-the-art theorem provers. Our results demonstrate the strength of our approach by solving new problems coming from program analysis and mathematical properties of integers.

#### **1 Introduction**

One of the most commonly used data types in imperative/functional programs are integers. For example, iterating over arrays in imperative programs or recursively computing sums in functional programs include integer-valued program variables, as illustrated in Figure 1. While for many uses of integers in programming we only need to consider non-negative integers, there are also applications where integers are essential, for example, reasoning about memory. To formally prove functional correctness of such and similar programs, reasoning about integers is indispensable but so is handling some sort of induction over integers. In this paper we address these two reasoning challenges and fully automate inductive reasoning with integers within saturation-based theorem proving.

Induction in saturation-based theorem proving is a new exciting direction in the automation of induction, recently introduced in [5, 10, 16]. This work focused on induction on inductively defined data types, also called algebraic data types [12], such as natural numbers or lists. However, automating *integer induction*, that is, induction on integers, has not yet been addressed sufficiently.

While natural numbers have a well-founded order and induction over this order is very useful in automated inductive theorem proving, the standard order on integers is not well-founded, so it cannot be directly used as the induction ordering. In this paper we will use the observation that the standard ordering < is well-founded on every set of integers having a lower bound b and likewise, the inverse > of this ordering is well-founded on every set of integers having an upper bound b. This gives us two induction rules on such integer subsets: induction (with the base case b) using < and induction (with the base case b) using >, respectively, to prove that a property holds for all integers ≥ b and, respectively, ≤ b. We define these induction rules as *upward, respectively, downward induction rules with symbolic bounds*. We also consider two variations of these rules over integer intervals and refer to such rules as *interval upward, respectively, downward induction rules with symbolic bounds*.

For natural numbers, 0 is an obvious base case candidate, which also turns out to be successful in the theorem proving practice. It is also a natural base case candidate for induction. In this paper we will give some natural problems for which neither 0 nor any concrete integer is a good base case. Our paper focuses on the following three issues:

This paper is organized as follows. In Section 2 we illustrate our approach by considering properties of the functional and imperative programs of Figure 1. Then in Section 3 we define four induction rules over integers, called *(interval) downward, respectively upward, induction rules with symbolic bounds*, and prove their soundness. Section 4 introduces an extension of superposition calculus by our new integer induction rules. We demonstrate that, using this extension, superposition provers can prove integer properties similarly to how humans would do. This extension is especially successful when used together with the AVATAR architecture [19], since AVATAR helps in reasoning efficiently using constraints coming out of the integer induction rules.

We implemented our work in the Vampire theorem prover [13] and compare our implementation with other relevant provers, including Vampire without integer induction (Section 5). Our experiments show that integer induction can solve many new problems that could not so far be solved by any prover. For example, 75 problems coming from program analysis and/or mathematical integer properties could be solved only by Vampire with the new induction rules.

*Contributions.* This paper makes the following contributions:

**fun** sum(n, m) = **if** n = m **then** n **else** n + sum(n + 1, m); **assert** ∀n, m ∈ Z.(n ≤ m → 2 · sum(n, m) = m ·(m + 1) − n ·(n − 1)) (a) Sum of integers from [n, m]. **assume** 0 ≤ pos < A.size i := pos; **while** i + 1 < A.size **do** A[i + 1] := A[i]; i := i + 1; **inv** ∀j ∈ Z.(pos ≤ j<i → valA(j + 1) = valA(j)) **end assert** ∀j ∈ Z.(pos ≤ j < A.size → valA(j) = valA(pos)) (b) Array initialization, with valA(j) denoting A[j].

**Fig. 1.** Motivating examples for inductive reasoning with integers.

## **2 Motivating Examples**

#### **2.1 Preliminaries**

We assume familiarity with standard many-sorted first-order logic with equality. For details we refer to [13]. Throughout this paper we denote variables by x, y, e, j, n, m, constants by c, c , Skolem constants by σ, all possibly with indices. We denote terms by t, literals by L, formulas by F and clauses by C. We denote the equality predicate by = and write t1 = t2 for the literal ¬(t1 = t2).

We will focus on integer induction. To this end, we assume a distinguished *integer sort*, denoted by Z. When we use standard integer predicates <, ≤, >, ≥, functions +, −,... and constants 0, 1, 2,... , we assume that they denote the corresponding interpreted integer predicates and functions with their standard interpretations. All other symbols are uninterpreted. We will write quantifiers like ∀x ∈ Z to denote that x has the integer sort.

In what follows, we will sometimes write "this problem requires integer induction". This should not be regarded as a formal statement: this property is not easy to formalize in general and it is possible that some of these problems can be proved by certain combinations of decision procedures, first-order theorem proving with uninterpreted functions, and axiomatization of interpreted functions on integers. However, when we make such statements, one can see that these problems have relatively simple proofs involving induction and cannot be proved by existing provers without induction.

#### **2.2 Examples**

To illustrate problems arising in automating integer induction, let us consider the programs of Figure 1. Properties of both programs are specified using assertions expressed in first-order logic, with pre- and post-conditions specified by the keywords **assume** and **assert**, respectively.

*Functional programs.* The ML-style functional program of Figure 1(a) computes the sum sum(n, m) of integers in the interval [n, m], that is m i=n i, where m ≥ n. The function definition uses the following axioms of sum:

$$\forall n \in \mathbb{Z}. (\text{sum}(n, n) = n); \tag{1}$$

$$\forall n, m \in \mathbb{Z}. (n \neq m \to \texttt{sum}(n, m) = n + \texttt{sum}(n+1, m)). \tag{2}$$

We should prove the assertion

$$\forall n, m \in \mathbb{Z}. (n \le m \to 2 \cdot \mathfrak{sum}(n, m) = m \cdot (m + 1) - n \cdot (n - 1)). \tag{3}$$

Formally proving (3) requires inductive reasoning with both integers and quantifiers. Let F[x] be a formula with one or more occurrences of an integer variable x and b an integer term not containing x. Consider the following formula:

$$F[b] \land \forall x \in \mathbb{Z}. (x \le b \land F[x] \to F[x-1]) \to \forall x \in \mathbb{Z}. (x \le b \to F[x]). \tag{4}$$

This formula is valid. It is similar to the standard induction on natural numbers, yet with two essential differences. First, we use x−1 instead of x+ 1 and second, we use the term b where for the standard induction we would use 0. Note that b does not have to be a concrete integer, it can be any term. In the sequel we will refer to such terms b used in induction rules as *symbolic bounds*.

For proving (3) using a theorem prover, we first negate and skolemize (3), obtaining the following formula, where σn, σm are fresh skolem constants:

$$
\sigma\_n \le \sigma\_m \land 2 \cdot \text{sum}(\sigma\_n, \sigma\_m) \ne \sigma\_m \cdot (\sigma\_m + 1) - \sigma\_n \cdot (\sigma\_n - 1) \tag{5}
$$

Modern theorem provers implementing linear integer arithmetic and quantifiers can prove unsatisfiability of (1), (2) and (5) in a relatively straightforward way if we also add an instance of induction rule (4) with

$$\begin{array}{c} F[x] \stackrel{\text{def}}{=} 2 \cdot \mathsf{sum}(x, \sigma\_m) = \sigma\_m \cdot (\sigma\_m + 1) - x \cdot (x - 1); \\\ b \stackrel{\text{def}}{=} \sigma\_m. \end{array}$$

Here and in the sequel def = means "equal by definition" or "defined as". If we want to automate this kind of reasoning, the main question is finding the corresponding instance of induction rule (4), that is, finding the induction formula F[x] and the (symbolic) bound b.

*Imperative programs.* The C-style imperative program of Figure 1(b) initializes an integer-valued array A starting at the index *pos*. We should prove the assertion stating that all array elements at indices greater than or equal to *pos* are equal to each other. Proving such assertions typically requires loop invariants "summarizing" the loop behavior. One such invariant I is shown in the loop after the keyword **inv**. This invariant I could be derived by existing approaches to invariant generation [8, 9].

The assertion of Figure 1(b) is then proved using I, by establishing that the post-condition

$$\forall j \in \mathbb{Z}. (pos \le j < \text{A.size} \to \text{va} \mathbb{1}\_{\text{A}}(j) = \text{va} \mathbb{1}\_{\text{A}}(pos)) \tag{6}$$

is a logical consequence of the invariant I and the negation of the loop condition:

$$\begin{array}{l} \forall j \in \mathbb{Z}. (pos \le j < i \to \mathbf{va1}\_{\mathcal{A}}(j+1) = \mathbf{va1}\_{\mathcal{A}}(j)); \\\neg (i+1 < \mathbf{A}. \text{size}). \end{array} \tag{7}$$

Interestingly, modern theorem provers cannot perform such proofs. Similar to the first example, we can use an induction rule for integers formulated as follows:

$$\begin{array}{c} \left( F[b\_1] \land \forall x \in \mathbb{Z}. (b\_1 \le x < b\_2 \land F[x] \to F[x+1]) \right) \\ \to \forall x \in \mathbb{Z}. (b\_1 \le x \le b\_2 \to F[x]). \end{array} \tag{8}$$

If we add an instance of this rule defined as follows:

$$\begin{array}{c} F[x] \stackrel{\text{def}}{=} \operatorname{va1}\_{\mathcal{A}}(x) = \operatorname{va1}\_{\mathcal{A}}(pos); \\ b\_{1} \stackrel{\text{def}}{=} pos; \\ b\_{2} \stackrel{\text{def}}{=} \operatorname{A.size} - 1, \end{array}$$

then state-of-the-art theorem provers can easily prove that (6) is a logical consequence of (7) and the corresponding instance of (8). For example, Cvc4 [1], Z3 [6] and Vampire prove such an instance in essentially no time. However, similarly to the example of Figure 1(a), in order to find such proofs automatically using the induction rule of (8), we need to be able to discover, during the proof search, the induction formula F[x] and the symbolic bounds b1, b2. In what follows, we describe our solution to automating this discovery by integrating integer induction within saturation-based theorem proving.

#### **3 Integer Induction**

In this section we define four induction rules, or induction schemas, on integers. Two of them were already considered in Section 2 – namely (4) and (8).

**Definition 1 (Downward/Upward Induction).** A *downward, respectively upward, induction axiom with symbolic bounds* is any formula of the form

$$\begin{array}{l} F[b] \wedge \forall x. (x \le b \wedge F[x] \to F[x-1]) \to \forall x. (x \le b \to F[x]); & (downward) \\ F[b] \wedge \forall x. (x \ge b \wedge F[x] \to F[x+1]) \to \forall x. (x \ge b \to F[x]), & (upward) \end{array}$$

respectively, where F[x] is a formula with one or more occurrences of an integer variable x and b is an integer term not containing x.

Note that (4) is a downward induction axiom with symbolic bounds.

**Definition 2 (Interval Downward/Upward Induction).** An *interval downward, respectively upward, induction axiom with symbolic bounds* is any formula of the form

F[b2] ∧ ∀x.(b1 < x ≤ b2 ∧ F[x] → F[x − 1]) → ∀x.(b1 ≤ x ≤ b2 → F[x]); (down.) F[b1] ∧ ∀x.(b1 ≤ x<b2 ∧ F[x] → F[x + 1]) → ∀x.(b1 ≤ x ≤ b2 → F[x]), (up.)

respectively, where F[x] is a formula with one or more occurrences of an integer variable x and b1, b2 are integer terms not containing x.

Note that (8) is an interval upward induction axiom with symbolic bounds. The main motivation for interval induction rules is their utility in reasoning about loops, as illustrated by the example of Figure 1(a). While interval induction can be captured by induction with one bound, it would require additional case analysis, which is not efficient in saturation-based proving practice.

In the sequel, we will refer to the integer terms of b, b1, b2 from Definitions 1-2 as *symbolic bounds* and the formulas F[x] from the induction axioms of Definitions 1-2 as *induction formulas*.

**Definition 3 (Downward/Upward Induction Rules).** The *downward (respectively, upward) induction rule with symbolic bounds*, or simply *downward (respectively, upward) induction rule* is the inference rule whose instances are all downward (respectively, upward) induction axioms with symbolic bounds.

Likewise, the *interval downward (respectively, upward) induction rule with symbolic bounds*, or simply *interval downward (respectively, upward) induction rule* is the inference rule whose instances are all interval downward (respectively, upward) induction axioms with symbolic bounds.

It is easy to see that the following theorem holds.

**Theorem 1 (Soundness).** *The (interval) downward/upward induction rules of Definition 3 are sound, that is, all corresponding induction axioms from Definitions 1-2 are valid.*

#### **4 Integer Induction in Saturation-Based Proof Search**

Our next aim is to define analogues of the induction rules introduced in Section 3 that can be used in superposition theorem provers and their saturation algorithms. For a general discussion of superposition and saturation we refer to [13]. In this section we use to denote the empty clause and write CNF(F) to mean (any) clausal normal form of a formula F. We refer to the set of clauses on which a saturation algorithm operates as the *search space*.

The most general way to introduce our new induction rules at the calculus level is to add clausal forms of our new induction axioms to the search space. That is, for every induction axiom F from Section 3, we add the rule

CNF(F)

.

However, we cannot efficiently implement such a calculus, as any formula with one variable can be used as an induction formula. We will therefore introduce different, more specialized, rules, which still correspond to the previously defined induction rules. The new rules use variations of the following three ideas:

The first two ideas were already used in the first papers underlying our approach to induction in saturation theorem proving [10, 16]. For example, they can be implemented by using only induction formulas that are obtained from ground literals L[t] in the search space, where t is a ground term. The corresponding induction formula will be ¬L[x]. The idea is that, when we prove the induction formula, ¬L[x] will be resolved against L[t].

The third idea is new. Note that, if we use the first two ideas and the upward induction rule, instead of ¬L[x] we will derive b ≤ x → ¬L[x]. When we resolve this against L[t], we obtain the clause ¬(b ≤ t). However, if we already previously derived b ≤ t, we can also resolve away ¬(b ≤ t). This gives us the idea to only apply the upward induction rules when we have b ≤ t. 4

Based on the three ideas above, we introduce the following four induction rules on clauses. In these rules t is a ground term, b is a constant and L[x] is a literal containing at least one occurrence of a variable x and no other variables. The rules depend on which comparisons among t ≥ b, t>b, t ≤ b and t b \\ \hline \text{CNF} \left( \left( L[b] \land \forall x. (x \ge b \land L[x] \to L[x+1]) \right) \to \forall y. (y > b \to L[y]) \right) \\\\ \neg L[t] \lor C \qquad t \le b \\ \hline \text{CNF} \left( \left( L[b] \land \forall x. (x \le b \land L[x] \to L[x-1]) \right) \to \forall y. (y \le b \to L[y]) \right) \\\\ \neg L[t] \lor C \qquad t < b \\ \hline \text{CNF} \left( \left( L[b] \land \forall x. (x \le b \land L[x] \to L[x-1]) \right) \to \forall y. (y < b \to L[y]) \right) \\\\ \text{CNF} \left( \left( L[b] \land \forall x. (x \le b \land L[x] \to L[x-1]) \right) \to \forall y. (y < b \to L[y]) \right) \end{array}$$

Note that IntInd≥ and IntInd> are upward induction rules, whereas IntInd≤ and IntInd< are downward induction rules. One can also introduce non-ground analogues of these rules but we do not consider them in this paper.

4 Using the AVATAR architecture [19], we can easily obtain valid literals b ≤ t.

Similarly to the above rules on the clausal level, we also introduce the interval upward/downward induction rules on clauses to be used in saturation algorithms for the superposition calculus. Since these rules are similar to each other, here we only define one rule IntInd[≥] for interval upward induction. For a ground term t, constants b1, b2, and L[x] a literal containing at least one occurrence of a variable x and no other variables, an interval upward induction rule on clauses:

$$\begin{aligned} \frac{\neg L[t] \lor C \qquad t \ge b\_1 \qquad t \le b\_2}{\text{CNF}\left(\left(L[b\_1] \land \forall x. (b\_1 \le x , IntInd≤, IntInd< and IntInd[≥] on the clausal level are sound.

**Theorem 2 (Soundness).** *For every satisfiability preserving CNF function, the induction rules from Definition 3 are sound.*

*Example 1.* To illustrate again how the choice of induction formulas allows us to have shorter clauses, consider IntInd≤. The CNF in its conclusion consists of three clauses:

$$\begin{array}{l} \neg L[b] \lor \sigma \le b \lor \neg y \le b \lor L[y] \\\neg L[b] \lor L[\sigma] \lor \neg y \le b \lor L[y] \\\neg L[b] \lor \neg L[\sigma - 1] \lor \neg y \le b \lor L[y] \end{array} \tag{9}$$

These clauses can be resolved against premises of IntInd≤, yielding the following clauses:

$$\begin{array}{l}\neg L[b] \lor \sigma \le b \lor C\\\neg L[b] \lor L[\sigma] \lor C\\\neg L[b] \lor \neg L[\sigma-1] \lor C\end{array} \tag{10}$$

They have an especially simple form when C is the empty clause -. In this case we have three clauses:

$$\begin{array}{l}\neg L[b] \lor \sigma \le b\\\neg L[b] \lor L[\sigma] \\\neg L[b] \lor \neg L[\sigma-1] \end{array} \tag{11}$$

which subsume the original three longer clauses and are ground. Since they are ground, they can be handled efficiently by AVATAR.

*Example 2.* Let us now demonstrate how the downward induction rule IntInd≤ works for refuting the inductive property (3) from our motivating example of Figure 1(a). We use literals from (5) as the premises of the IntInd≤ rule. The corresponding instance of the downward induction rule is defined by

$$\begin{aligned} b &\stackrel{\text{def}}{=} \sigma\_m; \\ t &\stackrel{\text{def}}{=} \sigma\_n; \\ L[x] &\stackrel{\text{def}}{=} 2 \cdot \text{sum}(x, \sigma\_m) = \sigma\_m \cdot (\sigma\_m + 1) - x \cdot (x - 1). \end{aligned}$$

This instance of IntInd≤ is:

$$\begin{array}{cc} 2 \cdot \mathsf{sum}(\sigma\_n, \sigma\_m) \neq \sigma\_m \cdot (\sigma\_m + 1) - \sigma\_n \cdot (\sigma\_n - 1) & \sigma\_n \leq \sigma\_m \\ \hline \end{array} \quad \begin{array}{c} \sigma\_n \leq \sigma\_m \\ \end{array} \quad \begin{array}{c} \sigma\_n \leq \sigma\_m \\ \end{array} \quad \begin{array}{c} \left(\mathsf{Int}.\mathsf{Ind}\_{\leq}\right) \\ \right. \\ \left. \left(\begin{array}{c} \sigma\_n \leq \sigma\_m \rightarrow 2 \cdot \mathsf{sum}(x, \sigma\_m) = \sigma\_m \cdot (\sigma\_m + 1) - x \cdot (x - 1) \\ \rightarrow \\ \end{array} \right. \\ \left. \left(\begin{array}{c} \sigma\_n \leq \sigma\_m \rightarrow 2 \cdot \mathsf{sum}(x, \sigma\_m) = \sigma\_m \cdot (\sigma\_m + 1) - (x - 1) \cdot ((x - 1) - 1) \\ \rightarrow \end{array} \right) \right) \\ \rightarrow \forall y. \big(y \leq \sigma\_m \rightarrow 2 \cdot \mathsf{sum}(y, \sigma\_m) = \sigma\_m \cdot (\sigma\_m + 1) - y \cdot (y - 1) \Big) \\ \end{array}$$

This single instance of the induction rule does the magic. By adding its conclusion to the search space we can obtain a contradiction in a few steps by applying a few superposition rules and using ground reasoning in linear integer arithmetic with uninterpreted functions (as evidenced by the results for the first problem subset, *x all* of *sum*, in Table 3).

We finally note that functional correctness of Figure 1(b) is proved by the interval upward induction rule IntInd[≥], in a similar way as above (and as evidenced by the results of Table 3 for *declared unint ax-fin conj-fin* in *val*).

What we find especially interesting in Example 2 is that the induction axiom used in it (and discovered by our implementation of induction in Vampire) uses the induction argument that would probably be used by a majority of humans who would try to argue why the program property holds.

#### **5 Implementation and Experiments**

#### **5.1 Implementation**

We implemented our integer induction rules IntInd≥, IntInd>, IntInd≤, IntInd< as well as IntInd[≥] and the other corresponding interval induction rules in Vampire. Further, we also implemented a more general induction rule IntInd that does not require bounds to be in the search space and uses 0 as the lower or the upper bound. Our implementation in Vampire, consisting of approximately 1,200 lines of new C++ code, is available at https://github.com/vprover/vampire. The size of this additional code is relatively small because Vampire has libraries for indexing and chaining inference rules that could be used off the shelf.

Our (interval) downward/upward induction rules described in Section 4 can be applied when either (i) the comparison literal (e.g., t ≥ b for the IntInd≥ rule) is selected and the corresponding clause ¬L[t] ∨ C was already selected as an induction candidate before, or (ii) if ¬L[t] ∨ C is selected as an induction candidate and the corresponding comparison literal was already selected before. To implement these rules efficiently, we should be able to efficiently retrieve comparison literals and literals selected for induction. To do so, we extended the indexing mechanism of Vampire to index such literals. We do not apply induction when the induction formula L[x] is a comparison having x as a top level argument, for example, x ≤ t, and allow to apply it to all other induction formulas deemed to be suitable by other user-specified options.

370 P. Hozzov´a, L. Kov´acs and A. Voronkov

```
assume e ≥ 1
fun power(x, 1) = x
   | power(x, e) = x · power(x, e − 1);
assert ∀x, y ∈ Z.(power(x · y, e) = power(x, e) · power(y, e))
```
**Fig. 2.** ML-like functional program computing integer powers for positive exponents.

Our (interval) downward/upward induction rules in Vampire are enabled by the new option --induction int. The options --int induction interval infinite and --int induction interval finite limit the enabled rules to downward/upward only, and interval downward/upward only, respectively. Further, --int induction default bound on enables the more general rule which does not require bounds to be in the search space. Our new induction rules can also be controlled by other Vampire options for well-founded/structural induction, such as --induction on complex terms on, which enables applying induction on any ground complex term. To improve Vampire's performance for integer induction, we combined our new induction rules with --induction on complex terms on and also other options not specific for induction. We extended Vampire with a new mode scheduling various option configurations for integer induction, switched on by the option --mode portfolio --schedule integer induction. Additionally, we introduced the option --schedule induction which uses either the integer induction configurations as for --schedule integer induction, or structural induction configurations, or both, depending on the data types used in the problem/property to be proved.

#### **5.2 Benchmarks**

We used two sets of examples: (i) benchmark sets LIA and UFLIA from the SMT-LIB collection [2], consisting of, respectively, 607 and 10,137 examples, and (ii) 120 new benchmarks similar to our motivating examples from Section 2.

To the best of our knowledge, the state-of-the-art systems implementing inductive reasoning have so far not yet considered inductive reasoning over integers, with two exceptions: [17], which mainly focuses on induction over inductively defined data types but mentions induction on non-negative integers and [11], which supports inductive reasoning using recursive function definitions without any special treatment for integers.

Since integer induction has not yet attracted enough attention in theorem proving, there is no significant collection of benchmarks for integer induction. To properly carry out experiments, we therefore created a set of *120 new benchmarks* based on variations of our motivating examples from Section 2 and on properties of computing integer powers. One example is the function correctness of the

**Table 1.** Description of our benchmark set of 120 new examples.

program of Figure 2, which is formalized as follows:

axioms: ∀x ∈ Z.(power(x, 1) = x)

$$\forall x, e \in \mathbb{Z}. (2 \le e \to \mathtt{power}(x, e) = x \cdot \mathtt{power}(x, e - 1))\tag{12}$$

$$\dots \quad \dots \quad \dots \quad \dots \quad (1 \le e \le \mathtt{\dots\dots\dots\dots\dots\dots\dots})\qquad \dots \quad \dots \quad (\dots \quad) \quad \dots \quad \dots \quad (\dots \quad)$$

conjecture: ∀x, y, e.(1 ≤ e → power(x · y, e) = power(x, e) · power(y, e))

Our set of 120 new benchmarks is described in Table 1 and available online at:

#### https://github.com/vprover/inductive\_benchmarks

To confirm that our new benchmarks require the use of inductive reasoning, we tested them on the SMT solver Z3 [6] that does not support induction. Z3 could not solve any of the 120 problems from our benchmark set. Names of subsets of our new benchmarks are constructed by joining variant tags described in Table 1. For example, problem (6) belongs to the category *declared unint axfin conj-fin* of the set *val*. The following benchmark:

$$\begin{aligned} \text{axiom:} & \quad \forall x \in \mathbb{Z}. (\mathbf{va1}(x) = \mathbf{va1}(x+1)) \\ \text{xconjecture:} & \quad \forall x, y \in \mathbb{Z}. (\mathbf{va1}(x) = \mathbf{va1}(y)) \end{aligned} \tag{13}$$

belongs to *declared unint ax-all conj-all* of *val* and the below example is from *defined inter ax-geq conj-geq* of *val*:

$$\begin{aligned} \text{axioms:} \quad & \forall x \in \mathbb{Z}. (x \le 0 \to \mathbf{va1}(x) = 0) \\ & \forall x \in \mathbb{Z}. (0 < x \to \mathbf{va1}(x) = \mathbf{va1}(x - 1)) \\ \text{conjecture:} \quad & \forall x \in \mathbb{Z}. (0 \le x \to \mathbf{va1}(x) = \mathbf{va1}(0)) \end{aligned} \tag{14}$$

While 9 of the benchmarks (all in *val*) use finite intervals in both the assertion and the invariant (*ax-fin conj-fin*), the remaining 111 benchmarks require inductive reasoning over infinite intervals.

**Table 2.** Comparison of solvers on SMT-LIB benchmarks.

#### **5.3 Experimental Setup**

We ran our experiments on computers with 32 cores (AMD Epyc 7502, 2.5 GHz) and 1 TB RAM. In all experiments we used the memory limit of 16 GB per problem. For the new benchmarks we used a 300 seconds time limit. For the experiments on the larger LIA and UFLIA sets we used a 10 seconds time limit.

In what follows, Vampire refers to the (default) version of Vampire, as in [10, 16]. By Vampire-I we denote our new version of Vampire, using integer induction rules (--induction int). Vampire-I\* refers to the portfolio mode of Vampire-I, scheduling various option configurations for integer induction (--mode portfolio --schedule induction).

For *experiments with the new benchmarks*, we note that Vampire without integer induction cannot solve any of the problems. In this set of experiments, we therefore compared Vampire-I to the provers Cvc4 [17] and Acl2 [11], which are, to the best of our knowledge, the only two automated solvers supporting inductive reasoning with integers in addition to reasoning with theories and quantifiers. For Cvc4, we used the *ig* configuration from [17]: --quant-ind --quant-cf --conjecture-gen --conjecture-gen-per-round=3 --full-saturate-quant. For Acl2, we used its default configuration and translated our new problem set into the functional program encoding syntax of Acl2. In the *experiments with the LIA and UFLIA benchmark sets of SMT-LIB*, we also used Z3 [6] in the default configuration.

We ran Cvc4, Z3, Vampire and Vampire-I on problems encoded in the SMT-LIB2 syntax [2]. For running Acl2 on the new benchmarks, we translated problems into the functional program encoding syntax of Acl2.

#### **5.4 Experimental Results**

*SMT-LIB Benchmarks.* First, we evaluated the improvements of integer induction in Vampire-I when compared to Vampire, Cvc4 and Z3 on the LIA and UFLIA sets of SMT-LIB [2]. We aimed to verify that Vampire-I's performance does not deteriorate due to adding integer induction, check whether Vampire-I can solve problems that could not be solved automatically before, and to identify the best values for options related to integer induction. To this end, we picked five different strategies (e.g. using different saturation algorithms and selection functions) and used different combinations of induction options. Table 2 summarizes our results, showcasing that integer induction enabled Vampire-I to

**Table 3.** Experiments with our new benchmarks from Table 1.

solve over 100 new problems that Vampire could not solve before (last but one column of Table 2). Moreover, 45 of these problems were also new compared to Cvc4 and Z3 (last column of Table 2), which most likely means that no theorem prover was able to prove them before.

In problems solved using integer induction, the integer induction rules were applied often: at least one of the interval induction rules was used in nearly 99% of problems, while one of the induction rules with one bound was used in nearly all problems. The interval induction and induction rules were used on average 4559 and 1191 times, respectively. 89% of the proofs employed interval induction (67% upward, 29% downward), while 27% of the proofs used induction with one bound (22% upward, 8% downward). Additionally, over 64% of proofs only required one application of any induction rule.

*Experiments with 120 New Benchmarks.* Comparison results for Vampire-I, Acl2 and Cvc4 on our new benchmarks are displayed in Table 3, aggregated by benchmark subsets, as described in Table 1. We do not show Vampire in the table, since without integer induction it cannot solve any of the problems.

The results show that in some cases Acl2 can perform upward and downward induction on integers, but only when using interpreted constants as a base case (that is, it cannot handle symbolic bounds). However, it can only do so if it also proves termination of the recursively defined function. It also has issues with reasoning about multiplication.

Cvc4 has limited support for integer induction: it can apply upward induction but only when the base case is an interpreted constant. Since some problems seem to require induction with symbolic bounds, Cvc4 is mostly able to either solve all problems in a subset, or none of them. The only exception is the subset *declared mixed ax-fin conj-fin*, in which Cvc4 solves one problem, which can be solved using upward induction with an interpreted constant as the base case.

Vampire-I\* does not have any conceptual problems with solving the benchmarks. However, since it uses axioms and inference rules rather than dedicated decision procedures for handling integers, it sometime has issues with solving problems with large integer values. For example, for the infinite interval subset of the *val* benchmark set, the only problems Vampire-I\* did not solve were those containing the interpreted constant 100 or -100. Similarly, in the *power* benchmark set, the unsolved problems contained large numbers. Finally, in the *declared mixed ax-fin conj-fin* subset, the two problems Vampire-I\* did not solve also required more sophisticated arithmetic reasoning. However, inability of efficiently dealing with large numbers is not an intrinsic problem of superposition theorem provers. Reasoning with quantifiers and theories is still in its infancy and major improvements are underway. For example, there are recent parallel developments in superposition and linear arithmetic [15] that should improve this kind of reasoning in Vampire.

#### **6 Related Work**

Previous works on automating induction mainly focused on inductive reasoning for inductively defined data types, for example in inductive theorem provers Acl2 [11], IsaPlanner [7], HipSpec [4], Zeno [18] and Imandra [14]; superposition theorem provers Zipperposition [5] and Vampire [16]; and the SMT solver Cvc4 [17]. While most of these solvers support reasoning with integers, only Acl2 and Cvc4 implement some form of induction over integers.

The Acl2 approach [11] generates induction schemas based on recursive function calls in the property to be proved. Hence, it can only use induction to solve problems properties of recursively defined functions. On the other hand, the SMT-based setting of Cvc4 [17] applies induction by inductive strengthening of SMT properties in combination with subgoal discovery. As noted in Section 5, Cvc4 is limited to induction with concrete base cases and upward induction.

While downward integer induction can be considered a straightforward generalization of upward integer induction and does not solve many more problems in our benchmark sets, symbolic bounds provide a very powerful generalization, as witnessed by experimental results. In automated reasoning, the power provided by more general rules comes with the price of uncontrollable blowup of the search space. To harness this power we came up with defining (interval) upward/downward induction rules with symbolic bounds in the superposition calculus in such a way that they result in most cases in the addition of very simple clauses, which can be efficiently handled within the AVATAR architecture.

We believe that variants of our induction rules defined in Section 4 can also be successfully used by SMT solvers. The idea is to apply them, like we do, only when there is a suitable bound in the current candidate model. One can also combine this with the observation made in Example 1: one can resolve added induction formulas against literals already occurring in the search space to add only ground formulas.

The benchmark suite we propose and use in this paper is new and can be used to complement existing benchmarks: the TIP library [3] and the examples of [17]. Our 120 new examples are however more focused on integer properties, whereas [3, 17] contain a variety of problems mostly requiring induction over inductively defined types. Specifically, out of more than 500 inductive problems in TIP [3], only 3 use integers and no inductive data types. The examples from [17] contain 311 inductive benchmarks translated into three encodings, (i) using only inductive data types, (ii) using integers instead of natural numbers, but also other inductive data types (such as lists or trees), and (iii) using both integers and natural numbers to express the same properties, alongside other inductive data types. Problems from (iii) are also included in SMT-LIB [2]. Note that there is a substantial difference between our benchmarks and benchmarks from (ii). The latter mostly require inductive reasoning only for inductive data types (or no induction at all): they contain integers but only a few of them require inductive reasoning over integers, while most of our benchmarks require proper integer induction. For example, Vampire can solve 131 of 306 benchmarks in (ii) without using integer induction.

## **7 Conclusions**

We introduced new inference rules for automating inductive reasoning with integers within saturation-based theorem proving. Many problems in program analysis and mathematical problems of integers previously unsolvable by any theorem prover can now be solved completely automatically. We believe our results can progress automated program analysis and automation of mathematics, where integers are universally used.

**Acknowledgments.** We thank M´arton Hajd´u and Giles Reger for fruitful discussions. This work was partially funded by the ERC CoG ARTIST 101002685, the ERC StG SYMCAR 639270, the EPSRC grant EP/P03408X/1 and the FWF grant LogiCS W1255-N23.

## **References**

Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

# Superposition with First-class Booleans and Inprocessing Clausification

Visa Nummelin1 , Alexander Bentkamp1 , Sophie Tourret2,3 , and Petar Vukmirović1

1 Vrije Universiteit Amsterdam, Amsterdam, The Netherlands<EMAIL_ADDRESS><EMAIL_ADDRESS><EMAIL_ADDRESS>2 Université de Lorraine, CNRS, Inria, LORIA, Nancy, France<EMAIL_ADDRESS>3 Max-Planck-Institut für Informatik, Saarland Informatics Campus, Saarbrücken,

Germany

Abstract. We present a complete superposition calculus for first-order logic with an interpreted Boolean type. Our motivation is to lay the foundation for refutationally complete calculi in more expressive logics with Booleans, such as higher-order logic, and to make superposition work efficiently on problems that would be obfuscated when using clausification as preprocessing. Working directly on formulas, our calculus avoids the costly axiomatic encoding of the theory of Booleans into first-order logic and offers various ways to interleave clausification with other derivation steps. We evaluate our calculus using the Zipperposition theorem prover, and observe that, with no tuning of parameters, our approach is on a par with the state-of-the-art approach.

# 1 Introduction

Superposition is a calculus for equational first-order logic that works on problems given in clausal normal form. Its immense success made preprocessing clausification a predominant mechanism in modern automatic theorem proving. However, this preprocessing is not without drawbacks. Clausification can transform simple problems, such as s → s where s is a large formula, in a way that hides its original simplicity from the superposition calculus. Ganzinger and Stuber's superposition-like calculus [13] operates on clauses that contain formulas as well as terms and replaces preprocessing clausification by inprocessing—meaning processing during the operation of the calculus itself. Inprocessing clausification allows superposition's powerful simplification engine to work on formulas. For example, unit equalities can rewrite formulas s and t in s ↔ t before clausification duplicates the occurrences into s → t and t → s. Whole formulas rather than simple literals can be removed by rules such as subsumption resolution [4].

Another issue with Boolean reasoning in the standard superposition calculus is that, in first-order logic, formulas cannot appear inside terms although this is often desirable for problems coming from software verifiers or proof assistants. Instead, authors of such tools need to resort to translations. Kotelnikov et al.

c The Author(s) 2021

A. Platzer and G. Sutcliffe (Eds.): CADE 2021, LNAI 12699, pp. https://doi.org/10.1007/978-3-030-79876-5\_22 378–395, 2021.

studied effects of these translations in detail. They showed that simple axioms such as the domain cardinality axiom for Booleans (∀(x : o). x ≈ ∨ x ≈ ⊥) can severely slow down superposition provers. To support more efficient reasoning on problems with first-class Booleans, they describe the FOOL logic, which admits functions that take arguments of Boolean type and quantification over Booleans. They further describe two approaches to reason in FOOL: The first one [17] requires an additional rule in the superposition calculus, whereas the second one [16] is completely based on preprocessing.

Our calculus combines complementary advantages of Ganzinger and Stuber's and of Kotelnikov et al.'s work. Following Kotelnikov et al., our logic (Sect. 2) is similar to FOOL and supports nesting formulas inside terms, as well as quantifying over Booleans. Following Ganzinger and Stuber, our calculus (Sect. 3) reasons with formulas and supports inprocessing clausification.

Our calculus also extends the two approaches. To reduce the number of possible inferences, we generalize Ganzinger and Stuber's Boolean selection functions, which allow us to restrict the Boolean subterms in a clause on which inferences can be performed. The term order requirements of our calculus are less restrictive than Ganzinger and Stuber's. In addition to the lexicographic path order (LPO), we also support the Knuth-Bendix order (KBO) [15], which is known to work better with superposition in practice.

Our proof of refutational completeness (Sect. 4) lays the foundation for complete calculi in more complex logics with Booleans. Indeed, Bentkamp et al. [8] devised a refutationally complete calculus for higher-order logic based on our completeness theorem. Our theorem incorporates a powerful redundancy criterion that allows for a variety of inprocessing clausification methods (Sect. 5).

We implemented our approach in the Zipperposition theorem prover (Sect. 6) and evaluated it on thousands of problems that target our logic ranging from TPTP to SMT-LIB to Sledgehammer-generated benchmarks (Sect. 7). Without fine-tuning, our new calculus performs as well as known techniques. Exploring the strategic choices that our calculus opens should lead to further performance improvements. In addition, we corroborate the claims of Ganzinger and Stuber concerning applicability of formula-based superposition reasoning: We find a set of 17 TPTP problems (out of 1000 randomly selected) that Zipperposition can solve only using the techniques described in this paper. We refer to our technical report [25] for more details on our calculus and the complete completeness proof.

#### 2 Logic

Our logic is a first-order logic with an interpreted Boolean type. It is essentially identical to the UF logic of SMT-LIB [5], including the Core theory, but without if-then-else and let expressions, which can be supported through simple translations. It also closely resembles Kotelnikov et al.'s FOOL [17], which additionally supports if-then-else and let expressions.

Our logic requires an interpreted Boolean type o and allows for an arbitrary number of uninterpreted types. The set of symbols must contain the logical

symbols , ⊥ : o; ¬ : o → o; ∧, ∨, → : (o × o) → o; and the overloaded symbols ≈, ≈ : (τ × τ ) → o for each type τ . The logical symbols are printed in bold to distinguish them from the notation used for clauses below. Throughout the paper, we write tuples (a1,...,an) as a¯n or a¯.

The set of *terms* is defined inductively as follows. Every variable is a term. If f : ¯τn → υ is a symbol and t ¯n : ¯τn is a tuple of terms, then the application f(t ¯n) (or simply f if n = 0) is a term of type υ. If x is a variable and t : o a Boolean term, then the quantified terms ∀x. t and ∃x. t are terms of Boolean type. We view quantified terms modulo α-renaming. A *formula* is a term of Boolean type.

The *root* of a term is f if the term is an application f(t ¯n); it is x if the term is a variable x; and it is ∀ or ∃ if the term is a quantified term ∀x. t or ∃x. t. A variable occurrence is *free* in a term if it is not bound by ∀ or ∃. A term is *ground* if it contains no free variables. Substitutions are defined as usual in first-order logic and they rename quantified variables to avoid capture.

A literal s ≈˙ t is an equation s ≈ t or a disequation s ≈ t. Unlike terms constructed using the function symbols ≈ and ≈, literals are unoriented. A clause L1 ∨···∨ Ln is a finite multiset of literals Lj . The empty clause is written as ⊥. Terms t of Boolean type are not literals. They must be encoded as t ≈ and t ≈ ⊥, which we call *predicate literals*. Both are considered positive literals because they are equations, not disequations.

We have considered excluding negative literals s ≈ t by encoding them as (s ≈ t) ≈ ⊥, following Ganzinger and Stuber. However, this approach requires an additional term order condition to make the conclusion of equality factoring small enough, excluding KBO. To support both KBO and LPO, we allow negative literals. Regardless, our simplification mechanism will allow us to simplify negative literals of the form t ≈ ⊥ and t ≈ into t ≈ and t ≈ ⊥, respectively, thereby eliminating redundant representations of predicate literals.

The semantics is a straightforward extension of standard first-order logic only adding the interpretation of the Boolean type as a two element domain, as in Kotelnikov et al.'s FOOL logic. Some of our calculus rules introduce Skolem symbols, which are intended to be interpreted as witnesses for existentially quantified terms. Still, our semantics treats them as uninterpreted symbols. To achieve a satisfiability-preserving calculus, we assume that these symbols do not occur in the input problem. More precisely, we inductively extend the signature of the input problem by a symbol sk∀y. ¯ ∃z.t : ¯τ → υ for each term of the form ∃z. t over the extended signature, where υ is the type of z and y¯ : ¯τ are the free variables occurring in ∃z. t, in order of first appearance.

#### 3 The Calculus

Following standard superposition, our calculus employs a term order and a literal selection function to restrict the search space. To accommodate for quantified Boolean terms, we impose additional requirements on the term order. To support flexible reasoning with Boolean subterms, in addition to the literal selection function, we introduce a Boolean subterm selection function.

Term Order The calculus is parameterized by a strict well-founded order  on ground terms that fulfills: (O1) u  ⊥  for any term u that is not or ⊥; (O2) ∀x. t  {x → u}t and ∃x. t  {x → u}t for any term u whose only Boolean subterms are and ⊥; (O3) subterm property; (O4) compatibility with contexts (not necessarily below ∀ and ∃); (O5) totality. The order is extended to literals, clauses, and nonground terms as usual [2]. The nonground order then also enjoys (O6) stability under grounding substitutions.

Ganzinger and Stuber's term order restrictions are similar but incompatible with KBO. Using an encoding of our terms into untyped first-order logic we describe how both LPO and the transfinite variant of KBO [19] can satisfy conditions (O1)–(O6).

Our encoding represents bound variables by De Bruijn indices, which become new constant symbols dbn for n ∈ N. Quantifiers are represented by two new unary function symbols, also denoted by ∀ and ∃. All other symbols are simply identified with their untyped counterpart. Regardless of symbol precedence or symbol weights, KBO and LPO enjoy properties (O3)–(O6) when applied to the encoded terms. They are even compatible with contexts below quantifiers.

 For KBO, we can use the same symbol precedence and a symbol weight function W that assigns each symbol ordinal weights (of the form ωa + b with a, b ∈ N), where W() = W(⊥) = 1, W(∀) = W(∃) = ω, and W(f) ∈ N \ {0} for any other symbol f.

Selection and Eligibility Following an idea of Ganzinger and Stuber, we parameterize our calculus with two selection functions: one selecting literals and one selecting Boolean subterms.

Definition 1 (Selection functions). The calculus is parameterized by a literal selection function *FLSel* and a Boolean subterm selection function *FBSel*. The function *FLSel* maps each clause to a subset of its literals. The selection function *FBSel* maps each clause to a subset of its Boolean subterms. The literals *FLSel*(C) and the subterms *FBSel*(C) are *selected* in C. The following restrictions apply: (S1) A literal can only be selected if it is negative or of the form s ≈ ⊥. (S2) A Boolean subterm can only be selected if it is not , ⊥, or a variable. (S3) A Boolean subterm can only be selected if its occurrence is not below a quantifier. (S4) The topmost terms on either side of a positive literal cannot be selected.

The interplay of maximality w.r.t. term order, literal and Boolean selection functions gives rise to a new notion of eligibility:

Definition 2 (Eligibility). A literal L is (*strictly*) *eligible* w.r.t. a substitution σ in C if it is selected in C or there are no selected literals and no selected Boolean subterms in C and σL is (strictly) maximal in σC. The eligible subterms of a clause C w.r.t. a substitution σ are inductively defined as follows: (E1) Any selected subterm is eligible. (E2) If a literal s ≈˙ t with σs σt is either eligible and negative or strictly eligible and positive, then s is eligible. (E3) If a subterm is eligible and its root is not ≈, 6≈, ∀, or ∃, all of its direct subterms are also eligible. (E4) If a subterm is eligible and of the form s ≈ t or s 6≈ t, then s is eligible if σs 6 σt and t is eligible if σs 6 σt. The substitution σ is left implicit if it is the identity substitution.

The Core Inference Rules The following inference rules form our calculus:

D D0 ∨ t ≈ t 0 C[u] Sup σ(D0 ∨ C[t 0 ]) C C 0 ∨ u 0 ≈ v 0 ∨ u ≈ v Factor σ(C 0 ∨ v 6≈ v 0 ∨ u ≈ v 0 ) C C 0 ∨ u 6≈ u 0 Irrefl σC0 C C 0 ∨ s ≈ t ⊥Elim σC0 C[u] BoolRw σC[t 0 ] C[∀z. v] ∀Rw C[{z 7→ sk∀y. ¯ ∃z.¬v(¯y)}v] C[∃z. v] ∃Rw C[{z 7→ sk∀y. ¯ ∃z.v(¯y)}v] C[u] BoolHoist C[⊥] ∨ u ≈ > C[s ≈ t] ≈Hoist C[⊥] ∨ s ≈ t C[s 6≈ t] 6≈Hoist C[>] ∨ s ≈ t C[∀x. t] ∀Hoist C[⊥] ∨ {x 7→ y}t ≈ > C[∃x. t] ∃Hoist C[>] ∨ {x 7→ y}t ≈ ⊥

The rules are subject to the following side conditions:

Rationale for the Rules Our calculus is a graceful generalization of superposition: if the input clauses do not contain any Boolean terms, it coincides with standard superposition. In addition to the standard superposition rules Sup, Factor, and Irrefl, our calculus contains various rules to deal with Booleans. For each logical symbol and quantifier, we must consider the case where it is true and the case where it is false. Whenever possible, we prefer rules that rewrite the Boolean subterm in place (with names ending in Rw). When this cannot be done in a satisfiability-preserving way, we resort to rules hoisting the Boolean subterm into a dedicated literal (with names ending in Hoist). For terms rooted by an uninterpreted predicate, the rule BoolHoist only deals with the case that the term is false. If it is true, we rely on Sup to rewrite it to eventually.

*Example 3.* The clause a ∧ ¬a ≈ can be refuted by the core inferences as follows. First we derive a ≈ (displayed on the left) and then we use it to derive ⊥ (displayed on the right). In this and the following example, we assume eager selection of literals whenever the selection restrictions allow it.

The derivation illustrates how BoolHoist and Sup replace uninterpreted predicates by and ⊥ to allow BoolRw to eliminate the surrounding logical symbols.

*Example 4.* The clause (∃x. ∀y. y ≈ x) ≈ can be refuted as follows:

$$\frac{\frac{(\exists x.\forall y.\,y\,\,g\,\,x)\approx\mathsf{T}}{(\forall y.\,y\,\,\mathtt{g\,\,sk\,\_{x.\forall y.\,y\,\,g}})\approx\mathsf{T}}\,\exists\mathrm{Rw}}{\begin{array}{l} \mathsf{T}\lor(y'\;\mathtt{g\,\,sk\,\_{x.\forall y.\,y\,\,g}})\approx\mathsf{T} \\ \hline \bot\approx\mathsf{T}\lor(y'\;\mathtt{g\,\,sk\,\_{x.\forall y.\,y\,\,g}})\approx\mathsf{T} \\ \hline \frac{(y'\;\mathtt{g\,\,sk\,\_{x.\forall y.\,y\,\,g}})\approx\mathsf{T}}{\bot}\,\mathit{g\,\,Rw} \\ \hline \bot\end{array}}\,\mathit{L\,\mathit{L\,I}}$$

Redundancy Criterion In standard superposition, a clause is defined as redundant if all of its ground instances follow from smaller ground instances of other clauses. We keep this definition, but use a nonstandard notion of ground instances, inspired by constraint superposition [23]. In our completeness proof, this new notion of ground instances ensures that ground instances of the conclusion of ∀Rw, ∃Rw, ∀Hoist, and ∃Hoist inferences are smaller than the corresponding instances of their premise by property (O2).

Definition 5 (Redundancy of clauses). The *ground instances* of a clause C are all ground clauses of the form γC where γ is a substitution such that for all variables x, the only Boolean subterms of γx are ⊥ and . A ground clause C is *redundant* w.r.t. a ground clause set N if there exist clauses C1,...,Ck ∈ N such that C1,...,Ck |= C and C  Ci for all 1 ≤ i ≤ k. A nonground clause C is redundant w.r.t. clauses N if C is strictly subsumed by a clause in N or every ground instance of C is redundant w.r.t. ground instances of N.

In standard superposition, an inference is defined as redundant if all its ground instances are, and a ground inference is defined as redundant if its conclusion follows from other clauses smaller than the main premise. We keep this definition as well, but we use a nonstandard notion of ground instances for some of the Boolean rules. In our report, we define a slightly stronger variant of inference redundancy via an explicit ground calculus, but the following notion is also strong enough to justify the few prover optimizations based on inference redundancy we know from the literature (e.g., simultaneous superposition [7]).

Definition 6 (Redundancy of inferences). A *ground instance* of a ∀Rw, ∃Rw, ∀Hoist, or ∃Hoist inference is an inference obtained by applying a grounding substitution to premise and conclusion, regardless of whether the result is a valid ∀Rw, ∃Rw, ∀Hoist, or ∃Hoist inference. A *ground instance* of an inference ι of other rules is an inference ι of the same rule such that premises and conclusion of ι are ground instances of the respective premises and conclusion of ι. For ι , we use selection functions that select the ground literals and Boolean subterms corresponding to the ones selected in the nonground premises. A ground inference with main premise C, side premises C1,...,Cn, and conclusion D is *redundant* w.r.t. N if there exist clauses D1,...,Dk ≺ C in N such that D1,...,Dk, C1,...,Cn |= D. A nonground inference is redundant if all its ground instances are redundant.

A clause set N is *saturated* if every inference from N is redundant w.r.t. N.

Simplification Rules The redundancy criterion is a graceful generalization of the criterion of standard superposition. Thus, the standard simplification and deletion rules, such as deletion of trivial literals and clauses, subsumption, and demodulation, can be justified. Demodulation below quantifiers is justified if the term order is compatible with contexts below quantifiers.

Some calculus rules can act as simplifications. ⊥Elim can always be a simplification. Given a clause on which both Rw and Hoist apply, where ∈ {∀, ∃}, the clause can be replaced by the conclusions of these rules. If Rw does not apply because of condition 4 or 5, Hoist alone can be a simplification. Also justified by redundancy, the rules BoolHoist and Hoist can simultaneously replace all occurrences of the eligible subterm they act on. For example, applying ≈Hoist to p(x ≈ y) ≈ ∨ q(x ≈ y) ≈ ⊥ yields p(⊥) ≈ ∨ q(⊥) ≈ ⊥ ∨ x ≈ y.

While experimenting with our implementation, we have observed that the following simplification rule from Vampire [18] can substantially shorten proofs:

$$\frac{s \not\approx t \lor C[s]}{s \not\approx t \lor C[t]} \text{LOLRw}$$

In this rule, we require s  t.

Interpreting literals of the form s ≈ as s ≈ ⊥ and s ≈ ⊥ as s ≈ we can apply the rule even to these positive literals. This especially convenient with rules such as BoolHoist. Consider the clause C = pi (⊥) ≈ ⊥ ∨ q ≈ ⊥, assume no literal is selected and the Boolean selection function always selects a subterm p(⊥). Applying BoolHoist to C we get p(⊥) ≈ ∨pi−1(⊥) ≈ ⊥∨q ≈ ⊥. This can then be simplified to a tautological clause p(⊥) ≈ ∨ p(⊥) ≈ ⊥ ∨ q ≈ ⊥ using i − 2 LocalRw steps. If we did not use LocalRw, BoolHoist would produce i − 2 intermediary clauses starting from C, none of which would be recognized as a tautology.

Many rules of our calculus replace subterms with or ⊥. After this replacement, resulting terms can be simplified using Boolean equivalences that specify the behavior of logical operations on and ⊥. To this end, we use the rule BoolSimp [33], similar to simp of Leo-III [27, Sect. 4.2.1]:

$$\frac{C[s]}{C[t]} \text{BooL} \\ \text{SIMP}$$

This rule replaces s with t whenever s ≈ t is contained in a predefined set of tautological equations. In addition to all equations that Leo-III uses for simp, we also include more complex ones, such as (¬u → u) ≈ u and (u1 → ··· → un → v1 ∨ ··· ∨ vm) ≈ where ui = vj for some i and j. The exhaustive list is given in our technical report. Using BoolSimp and ⊥Elim, the twelve steps of Example 3 can be replaced by just two simplification steps.

BoolSimp simplifies terms with logical symbol roots if one argument is either or ⊥ or if two arguments are identical. Thus, after simplification, BoolRw applies only in two remaining cases: if all arguments of a logical symbol are distinct variables and if the sides of a (dis)equation are different and unifiable. This observation can be used to streamline the implementation of BoolRw.

#### 4 Refutational Completeness

Our calculus is dynamically refutationally complete. All the rules that do not introduce Skolem symbols are also sound.

Completeness Theorem 7. *Let* S0 *be an unsatisfiable set of clauses. Let* (Si)∞ i=0 *be a fair derivation—i.e., a derivation where* ∞ i=0 ∞ j=i Sj *is saturated. Then* ⊥ ∈ Si *for some* i*.*

We outline some key parts of the proof here and refer to our technical report [25] for the details. We first define a ground version of our calculus with standardly inherited redundancy criterion and prove it complete. Devising suitable ground analogues of the rules ∀Rw and ∃Rw was difficult because the arguments of the Skolems depend on the variables occurring in the premise. Therefore, we parameterize the ground calculus by a function that provides ground Skolem terms in the ground versions of these rules. When lifting the completeness result to the nonground level, we instantiate the parameter with a specific function that allows us to lift the ∀Rw and ∃Rw inferences.

To prove the ground calculus complete, we employ the framework for reduction of counterexamples [3]. It requires us to construct an interpretation I given a saturated unsatisfiable clause set that does not contain ⊥. Then we must show that any counterexample—i.e., a clause that does not hold in I—can be reduced to a smaller (≺) counterexample by some inference.

The interpretation I is defined by a normalizing rewrite system as in the standard completeness proof of superposition. To ensure a correct interpretation of Booleans, we incrementally add Boolean rewrite rules along with the rules produced by clauses as usual. If a counterexample can be rewritten by a Boolean rule, we reduce it by a Rw or Hoist inference.

We derive the dynamic completeness of our nonground calculus using the saturation framework [35]. It gives us a nonground clause set N to work with. We then have to choose the parameters of our ground calculus such that all of its inferences from the grounding of N are redundant or liftable. We show that inferences rewriting below variables are redundant. Other inferences we show to be liftable—i.e., they are a ground instance of some inference from N.

## 5 Inprocessing Clausification Methods

Our calculus makes preprocessing clausification unnecessary: A problem specified by a formula f can be represented as a clause f ≈ . Our redundancy criterion allows us to add various sets of rules to steer the inprocessing clausification.

Without any additional rules, our core calculus rules perform all the necessary reasoning about formulas. We call this method *inner delayed clausification* because the calculus rules tend to operate on the inner Boolean subterms first.

The *outer delayed clausification* method adds the following rules to the calculus, which are guided by the outermost logical symbols. Let s and t be Boolean terms. Below, we let s+ range over literals of the form s ≈ and s ≈ ⊥, and s− over literals of the form s ≈ ⊥ and s ≈ .

$$\begin{array}{cc} s^+ \lor C \\ \hline \hline co(s, C) \\ \hline co(s, C) \end{array} + \begin{array}{c} s^- \lor C \\ \hline co(\neg s, C) \\ \hline co(\neg s, C) \end{array} - \text{OUTERCLAus} $$

$$\begin{array}{c} s \approx t \lor C \\ s \approx \bot \lor C \\ \hline s \not\approx t \lor C \\ s \approx \bot \lor t \approx \bot \lor C \\ \hline \end{array} \approx \text{OUTERCLAus} $$

The rules +OuterClaus and −OuterClaus are applicable to any term s whose root is a logical symbol, whereas the rules ≈OuterClaus and ≈OuterClaus are only applicable if neither s nor t is or ⊥. Clearly, our redundancy criterion allows us to replace the premise of all Outer-Claus-rules with their conclusions. Nonetheless, the rules ≈OuterClaus and ≈OuterClaus are not used as simplification rules since destructing equivalences disturbs the syntactic structure of the formulas, as noted by Ganzinger and Stuber [13]. The function *oc*(s, C) analyzes the shape of the formula s and distributes it over the clause C. For example, *oc*(s1 → s2, C) = {s1 ≈ ⊥ ∨ s2 ≈ ∨ C}, and *oc*(¬(s1 ∨ s2), C) = {s1 ≈ ⊥ ∨ C, s2 ≈ ⊥ ∨ C}. This function also replaces quantified terms by either a fresh free variable or a Skolem in the body of the quantified term, depending on the polarity. The full definition of *oc*(s, C) is specified in our technical report.

A third inprocessing clausification method is *immediate clausification*. It first preprocesses the input problem using a standard first-order clausification procedure such as Nonnengart and Weidenbach's [24]. Then, during the proof search, when a clause C appears on which OuterClaus rules could be applied, we apply the standard clausification procedure on the formula ∀x. C ¯ instead (where x¯ are the free variables of C), and replace C with the clausification results. With this method, the formulas are clausified in one step, making intermediate clausification results inaccessible to the simplification machinery.

Renaming Common Formulas Following Tseitin [31], clausification procedures usually rename common formulas to prevent a possible combinatorial explosion caused by naive clausification. In our two delayed clausification methods, we realize this idea using the following rule:

$$\begin{array}{cccc} & C\_1[\sigma\_1 f] & \cdots & C\_n[\sigma\_n f] \\ \hline \\ C\_1[\sigma\_1 \mathfrak{p}(\bar{x})] & \cdots & C\_n[\sigma\_n \mathfrak{p}(\bar{x})] & R\_1 & \cdots & R\_m \\ \end{array} \text{RENAME}$$

Here, the formula f has a logical root, x¯ are the distinct free variables in f, p is a fresh symbol, σi is a substitution, and the clauses R1,...,Rm are the result of simplifying a *definition clause* R = p(¯x) ≈ f as described below. The rule avoids exponential explosion by replacing n positions in which results of f's clausification will appear into a single position in R. Optimizations such as polarity-aware renaming [24, Sect. 4] also apply to Rename.

Several issues arise with Rename as an inprocessing rule. We need to ensure that in R, f  p(¯x), since otherwise demodulation might reintroduce a formula f in the simplified clauses. This can be achieved by giving the fresh symbol p a precedence smaller than that of all symbols initially present in the problem (other than and ⊥). To ensure the precedence is well founded, the precedence of p must be greater than that of symbols previously introduced by the calculus. For KBO, we additionally set the weight of p to the minimal possible weight.

For Rename to be used as a simplification rule, we need to ensure that the conclusions are smaller than the premises. This is trivially true for all clauses other than the clause R. For example, let Ci = f ≈ (σi is the identity). Clearly, R is larger than Ci. However, we can view the definition clause R as two clauses R+ = p(¯x) ≈ ⊥ ∨ f ≈ and R− = p(¯x) ≈ ∨ f ≈ ⊥. Then, we can apply a single step of the OuterClaus rules to R+ and R− (on their subformula f), which further results in clauses R1,...,Rm. Inspecting the OuterClaus rules, it is clear that m ≤ 4, which makes enforcing this simplification tolerable. Furthermore, as f is simplified in each of R1,...,Rm, they are smaller than any premise Ci.

Another potential source of a combinatorial explosion in our calculus are formulas that occur deep in the arguments of uninterpreted predicates. Consider the clause C = pi (x) ≈ ∨ qj (y) ≈ where i, j > 2. If the first and the second literal are eligible in C, any clause pi1 (x) ≈ ∨ pi2 (⊥) ≈ ∨ ··· ∨ pi*k* (⊥) ≈ ∨ qj1 (y) ≈ ∨ qj2 (⊥) ≈ ∨···∨ qj*l* (⊥) ≈ (where i1+···+ik = i and j1+ ··· + jl = j) , resulting from multiple BoolHoist applications, can be obtained in many different ways. This explosion can be avoided using the following rule:

$$\frac{s \approx t \lor C}{\mathbf{p}(\overline{x}) \approx \mathbf{T} \lor C \qquad R\_1 \quad \cdots \quad R\_4} \text{RENAEDEEP}$$

where p is a fresh symbol, x¯ are all free variables occurring in s ≈ t, the clauses R1,...,R4 result from simplifying R = p(¯x) ≈ (s ≈ t) as described above, and we impose the same precedence and weight restrictions on p as for Rename. Finally, we require that both s ≈ t and C contain deep Booleans where a Boolean subterm u|p of a term u is a *deep Boolean* if there are at least two distinct proper prefixes q of the position p such that the root of u|q is an uninterpreted predicate.

Similarly to Rename, the definition clause R can be larger than the premise. As OuterClaus-rules might not apply to s ≈ t, we need a different solution:

$$\frac{C[u]}{C[\mathfrak{L}] \lor u \approx \mathfrak{T} \quad C[\mathfrak{T}] \lor u \approx \mathfrak{L}} \\ \text{BooLHosSTIMP}$$

In this rule u is a non-variable Boolean subterm, different from and ⊥, whose indicated occurrence is not in a literal u ≈ b where b is , ⊥ or a variable. Clearly, both conclusions of BoolHoistSimp are smaller than the premise. As before, observing that R is equivalent to two clauses R+ = p(¯x) ≈ ⊥∨s ≈ t and R− = p(¯x) ≈ ∨s ≈ t, we simplify R+ and R− into clauses that are guaranteed to be smaller than the premise. This is achieved by applying BoolHoistSimp to one of the deep Boolean occurrences in both R+ and R−, which produces R1,...,R4 and reduces the size of resulting clauses enough for them to be smaller than the premise of RenameDeep. The RenameDeep rule can be applied analogously to negative literals s ≈ t.

#### 6 Implementation

Zipperposition [11] is an automatic theorem prover designed for easy prototyping of various extensions of superposition. So far, it has been extended to support induction, arithmetic, and various fragments of higher-order logic. We have implemented our calculus and its extensions described above in Zipperposition.

Zipperposition has long supported λ as the only binder. Because introducing new binders would significantly complicate the implementation, we decided to represent the terms ∀x. t and ∃x. t as ∀(λx. t) and ∃(λx. t), respectively.

We introduced a normalized presentation of predicate literals as either s ≈ or s ≈ ⊥. As Zipperposition previously encoded them as s ≈ or s ≈ , enforcing the new encoding was a source of tedious implementation effort.

Factor inferences happen even when the maximal literal is selected since the discovery of condition (3) as described in Sect. 3 came after the evaluation.

Zipperposition's existing selection functions were not designed with Boolean subterm selection in mind. For instance, a function that selects a literal L with a selectable Boolean subterm s can make s eligible, even if the Boolean selection function did not select s. To mitigate this issue, we can optionally block selection of literals that contain selectable Boolean subterms.

We implemented four Boolean selection functions: selecting the leftmost innermost, leftmost outermost, syntactically largest or syntactically smallest selectable subterm. Ties are broken by selecting the leftmost term. Additionally, we implemented a Boolean selection function that does not select any subterm.

Vukmirović and Nummelin [33, Sect. 3.4] explored inprocessing clausification as part of their pragmatic approach to higher-order Boolean reasoning. They describe in detail how the formula renaming mechanism is implemented. We reuse their mechanism, and simplify definition clauses as described in Sect. 5.

#### 7 Evaluation

The goal of our evaluation was to answer the following questions:

We filtered TPTP [29] and SMT-LIB [5] to get first-order benchmarks that actually do use the Boolean type. In TPTP THF we found 145 such problems (*TPTP Bool*) and in the UF section of SMT-LIB 5507 such problems. Martin Desharnais and Jasmin Blanchette generated 1253 Sledgehammer problems that target our logic. To measure the overhead of our calculus, we randomly chose 1000 FOF and CNF problems from the TPTP (*TPTP FO*). Even with this sample the experiment could take up to (145+5507+1253+1000) × #modes × 300 s ≈ 9 CPU months. On StarExec servers, evaluation roughly took three days under low load. Otherwise evaluating on all 13 000 FOF and CNF problems could have taken 2.5 times longer.

SMT-LIB interprets the symbol ite as the standard if-then-else function [5, Sect. 3.7.1]. Whenever a term s = ite(t1, t2, t3) of type τ occurs in a problem, we replace s with fτ (t1, t2, t3), where fτ is a fresh symbol denoting the ite function of a particular return type. To comply with SMT-LIB, we add the following axioms: ∀x y. fτ (, x, y) ≈ x and ∀x y. fτ (⊥, x, y) ≈ y. SMT-LIB allows the use of let variable bindings [5, Sect. 3.6.1]. We simply replace each variable with its definition in the body of the let bindings.

Currently, among competing superposition-based provers only E and Vampire support first-order logic with interpreted Booleans, and they do so through preprocessing. We could not evaluate Vampire in the first-order mode with FOOL preprocessing because it yielded unsound results on TPTP Bool benchmarks. We were able to run E on all benchmarks, except for the ones in SMT syntax.

We used Zipperposition's first-order portfolio, which invokes the prover sequentially with up to 13 configurations in different time slices. To compare different features, we ran different *modes* that enable a given feature in all of the portfolio configurations. All experiments were performed on the StarExec Iowa servers [28], equipped with Intel Xeon E5-2609 0 CPUs clocked at 2.40 GHz. We set the CPU time limit to 300 s. Figure 1 displays the results. An empty cell indicates that a mode is not evaluated on that benchmark set. An archive with the raw evaluation data is publicly available.4

A preprocessing transformation that removes all Boolean subterms occurring as arguments of symbols [34, Sect. 8], similar to Kotelnikov et al.'s FOOL clausification approach [16], is implemented in Zipperposition. To answer question 1, we enabled preprocessing and compared it to our new calculus parameterized with the Boolean selection function that selects the smallest selectable subterm. The mode using our new calculus performs immediate inprocessing clausification, and we call it *base*, while the mode that preprocesses Boolean subterms is denoted by *preprocess* in Figure 1.

The obtained results do not give a conclusive answer to question 1. On both TPTP Bool and Sledgehammer problems, some configuration of our new calculus manages to prove one problem more than preprocessing. On SMT-LIB benchmarks, the best configuration of our calculus matches preprocessing. This shows that our calculus already performs roughly as well as previously known techniques and suggests that it will be able to outperform preprocessing techniques after tuning of its parameters.

For context, we provide the evaluation of E on supported benchmarks. On TPTP FO benchmarks it solves 643 problems, on TPTP Bool benchmarks 144

4 https://doi.org/10.5281/zenodo.4550787

Fig. 1: Number of problems solved per benchmark set and Zipperposition mode. The x-axes start from the number of problems solved by all evaluated modes.

problems, and on Sledgehammer benchmarks 674 problems. Note that there is no straightforward way to compare these results with Zipperposition.

Our *base* mode uses immediate inprocessing clausification. To answer question 2, we compared *base* with a variant of *base* with outer delayed clausification (*base+outer* ) and with a variant with inner delayed clausification (*base+inner* ). In the delayed modes, we invoke the Rename rule on formulas that are discovered to occur more than four times in the proof state.

The results show that inner delayed clausification, which performs the laziest form of clausification, gives the worst results on most benchmark sets. Outer delayed clausification performs roughly as well as immediate clausification on problems targeting our logic.  However, outer delayed clausification solves 17 problems not solved by immediate clausification on these problems. This suggests that it opens new possibilities for first-order reasoning that need to be explored further with specialized strategies and additional rules.

We found a problem with a conjecture of the form s → s that only the delayed clausification modes can prove: the TPTP problem SWV122+1. The subformula renaming mechanism of immediate clausification obfuscates this problem, whereas delayed clausification allows BoolSimp to convert the negated conjecture to ⊥ directly, completing the proof in half a second.

To answer question 3, we compared the mode of Zipperposition in which all rules introduced by our calculus are disabled (*off* ) with *base* on purely first-order problems. Our results show that both modes perform roughly the same.

To answer question 4, we evaluated the Boolean selection functions we have implemented: syntactically smallest selectable term (used in *base*), syntactically largest selectable term (selmax), leftmost innermost selectable term (selli), leftmost outermost selectable term (sello), and no Boolean selection (sel∅). We also evaluated two modes in which the rules LocalRw and BoolHoistSimp (BHS) are enabled. None of the selection functions influences the performance greatly. Similarly, we observe no substantial difference regardless of whether the rules LocalRw and BoolHoistSimp are enabled.

# 8 Related Work and Conclusion

The research presented in this paper extends superposition in two directions: with inprocessing clausification and with first-class Booleans. The first direction has been explored before by Ganzinger and Stuber [13], and others have investigated it in the context of other superposition-related calculi [1,4,9,20,21].

The other direction has been explored before by Kotelnikov et al., who developed two approaches to cope with first-class Booleans [16,17]. For the quantified Boolean formula fragment of our logic, Seidl et al. developed a translation into effectively propositional logic [26]. More general approaches to incorporate theories into superposition include superposition for finite domains [14], hierarchic superposition [6], and superposition with (co)datatypes [10].

For SMT solvers [22], supporting first-class Booleans is a widely accepted standard [5]. In contrast, the TPTP TFX format [30], intended to promote firstclass Booleans in the rest of the automated reasoning community, has yet to gain traction. Software verification tools could clearly benefit from its popularization, as some of them identify terms and formulas in their logic, e.g., Why3 [12].

In conclusion, we devised a refutationally complete superposition calculus for first-order logic with interpreted Booleans. Its redundancy criterion allows us to flexibly add inprocessing clausification and other simplification rules. We believe our calculus is an excellent choice for the basis of new superposition provers: it offers the full power of standard superposition, while supporting rich input languages such as SMT-LIB and TPTP TFX. Even with unoptimized implementation and basic strategies, our calculus matches the performance of earlier approaches. In addition, the freedom it offers in term order, literal and Boolean subterm selection opens possibilities that are yet to be explored. Overall, our calculus appears as a solid foundation for richer logics in which the Boolean type cannot be efficiently preprocessed, such as higher-order logic [8]. In future work, we plan to tune the parameters and would find it interesting to combine our calculus with clause splitting techniques, such as AVATAR [32].

Acknowledgment Martin Desharnais and Jasmin Blanchette generated the Sledgehammer benchmarks. Simon Cruanes helped us with the implementation. The anonymous reviewers, Ahmed Bhayat, Jasmin Blanchette, and Uwe Waldmann suggested textual improvements. The maintainers of StarExec Iowa let us use their service. We thank them all. Nummelin'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). Bentkamp 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).

#### References

Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

# Superposition for Full Higher-order Logic

Alexander Bentkamp1 , Jasmin Blanchette1,2,3 , Sophie Tourret2,3 , and Petar Vukmirovic´1

1 Vrije Universiteit Amsterdam, Amsterdam, the Netherlands

<EMAIL_ADDRESS>
2 Université de Lorraine, CNRS, Inria, LORIA, Nancy, France

<EMAIL_ADDRESS>
3 Max-Planck-Institut für Informatik, Saarland Informatics Campus, Saarbrücken, Germany

Abstract. We recently designed two calculi as stepping stones towards superposition for full higher-order logic: Boolean-free λ-superposition and superposition for first-order logic with interpreted Booleans. Stepping on these stones, we finally reach a sound and refutationally complete calculus for higher-order logic with polymorphism, extensionality, Hilbert choice, and Henkin semantics. In addition to the complexity of combining the calculus's two predecessors, new challenges arise from the interplay between λ-terms and Booleans. Our implementation in Zipperposition outperforms all other higher-order theorem provers and is on a par with an earlier, pragmatic prototype of Booleans in Zipperposition.

# 1 Introduction

Superposition is a leading calculus for first-order logic with equality. We have been wondering for some years whether it would be possible to gracefully generalize it to extensional higher-order logic and use it as the basis of a strong higher-order automatic theorem prover. Towards this goal, we have, together with colleagues, designed superposition-like calculi for three intermediate logics between first-order and higherorder logic. Now we are finally ready to assemble a superposition calculus for full higher-order logic. The filiation of our new calculus from Bachmair and Ganzinger's standard first-order superposition is as follows:

Our goal was to devise an efficient calculus for higher-order logic. To achieve it, we pursued two objectives. First, the calculus should be refutationally complete. Second, the calculus should coincide as much as possible with its predecessors oSup and λSup on the respective fragments of higher-order logic (which in turn essentially coincide with Sup on first-order logic). Achieving these objectives is the main contribution of this paper. We made an effort to keep the calculus simple, but often the refutational completeness proof forced our hand to add conditions or special cases.

Like oSup, our calculus oλSup operates on clauses that can contain Boolean subterms, and it interleaves clausification with other inferences. Like λSup, oλSup eagerly βη-normalizes terms, employs full higher-order unification, and relies on a fluid subterm superposition rule (FLUIDSUP) to simulate superposition inferences below applied variables—i.e., terms of the form *y t*1 ...*tn* for *n* ≥ 1.

Because oSup contains several superposition-like inference rules for Boolean subterms, our completeness proof requires dedicated *fluid Boolean subterm hoisting rules* (FLUIDBOOLHOIST, FLUIDLOOBHOIST), which simulate Boolean inferences below applied variables, in addition to FLUIDSUP, which simulates superposition inferences.

Due to restrictions related to the term order that parameterizes superposition, it is difficult to handle variables bound by unclausified quantifiers if these variables occur applied or in arguments of applied variables. We solve the issue by replacing such quantified terms ∀*y*.*t* by equivalent terms (λ*y*. *t*) ≈ (λ*y*. ) in a preprocessing step.

We implemented our calculus in the Zipperposition prover and evaluated it on TPTP and Sledgehammer benchmarks. The new Zipperposition outperforms all other higherorder provers and is on a par with an ad hoc implementation of Booleans in the same prover by Vukmirovic and Nummelin [30]. We refer to the technical report [8] for the ´ completeness proof and a more detailed account of the calculus and its evaluation.

#### 2 Logic

Our logic is higher-order logic (simple type theory) with rank-1 polymorphism, Hilbert choice, and functional and Boolean extensionality. Its syntax mostly follows Gordon and Melham [17]. We use the notation ¯*an* or ¯*a* to stand for the tuple (*a*1,...,*an*) where *n* ≥ 0. Deviating from Gordon and Melham, type arguments are explicit, written as cτ¯*m* for a symbol c : Πα¯ *m*. υ and types ¯τ*m*. In the type signature Σty, we require the presence of a nullary Boolean type constructor o and a binary function type constructor →. In the term signature Σ, we require the presence of the logical symbols , ⊥, ¬, ∧, ∨, →, ∀, ∃, ≈, and ≈. The logical symbols are shown in bold to distinguish them from the notation used for clauses below. Moreover, we require the presence of the Hilbert choice operator ε ∈ Σ. Although ε is interpreted in our semantics, we do not consider it a logical symbol. Our calculus will enforce the semantics of ε by an axiom, whereas the semantics of the logical symbols will be enforced by inference rules. We write V for the set of (term) variables. We use Henkin semantics, in the style of Fitting [15], with respect to which we can prove our calculus refutationally complete. In summary, our logic essentially coincides with the TPTP TH1 format [20].

We generally view terms modulo αβη-equivalence. When defining operations that need to analyze the structure of terms, however, we use a custom normal form as the default representative of a βη-equivalence class: The βηQη*-normal* form *t*↓βηQη of a term *t* is obtained by bringing the term into η-short β-normal form and finally applying the rewrite rule Qτ *s* −→-Qη Qτ (λ*x*. *s x*) exhaustively whenever *s* is not a λexpression. Here and elsewhere, Q stands for either ∀ or ∃.

On top of the standard higher-order terms, we install a clausal structure that allows us to formulate calculus rules in the style of first-order superposition. A literal *s* ≈˙ *t* is an equation *s* ≈ *t* or disequation *s* ≈ *t* of terms *s* and *t*; both equations and disequations are unordered pairs. A clause *L*1 ∨···∨ *Ln* is a finite multiset of literals *Lj*. The empty clause is written as ⊥. This clausal structure does not restrict the logic, because an arbitrary term *t* of Boolean type can be written as the clause *t* ≈ .

We considered excluding negative literals by encoding them as (*s* ≈ *t*) ≈ ⊥, following ←→Sup [16]. However, this approach would make the conclusion of the equality factoring rule (EFACT) too large for our purposes. Regardless, the simplification machinery will allow us to reduce negative literals *t* ≈ ⊥ and *t* ≈ to *t* ≈ and *t* ≈ ⊥, respectively, thereby eliminating redundant representations of nonequational literals.

We let CSU(*s*,*t*) denote an arbitrary (preferably, minimal) complete set of unifiers for two terms *s* and *t* on the set of free variables of the clauses in which *s* and *t* occur. To compute such sets, Huet-style preunification [18] is not sufficient, and we must resort to a full unification procedure [19, 29]. To cope with the nontermination of such procedures, we use dovetailing as described by Vukmirovic et al. [28, Sect. 5]. ´

Some of the rules in our calculus introduce Skolem symbols, representing objects mandated by existential quantification. We assume that these symbols do not occur in the input problem. More formally, given a problem over a term signature Σ, our calculus operates on a Skolem-extended term signature Σsk that, in addition to all symbols from Σ, inductively contains symbols skΠα. ¯ ∀*x*¯. ∃*z*.*t z* : Πα. ¯ τ¯ → υ for all types υ, variables *z* : υ, and terms *t* : υ → o over Σsk, where ¯α are the free type variables occurring in *t* and ¯*x* : ¯τ are the free term variables occurring in *t*, both in order of first occurrence.

# 3 The Calculus

The oλSup calculus closely resembles λSup, augmented with rules for Boolean reasoning that are inspired by oSup. As in λSup, superposition-like inferences are restricted to certain first-order-like subterms, the *green subterms*, which we define inductively as follows: Every term *t* is a green subterm of *t*, and for all symbols f ∈ Σ \ {∀,∃}, if *t* is a green subterm of *ui* for some *i*, then *t* is a green subterm of fτ¯ *u*¯. For example, the green subterms of f(g (¬p)) (∀τ (λ*x*.q)) (*y* a) (λ*x*.h b) are the term itself, g (¬p), ¬p, p, ∀τ (λ*x*. q), *y* a, and λ*x*. h b. We write *s t* to denote a term *s* with a green subterm *t* and call the first-order-like context *s* a *green context*.

Following λSup, we call a term *t fluid* if (1) *t*↓βηQη is of the form *y u*¯*n* where *n* ≥ 1, or (2) *t*↓βηQη is a λ-expression and there exists a substitution σ such that *t*σ↓βηQη is not a λ-expression (due to η-reduction). Intuitively, fluid terms are terms whose normal form can change radically as a result of instantiation.

We define deeply occurring variables as in λSup, but exclude λ-expressions directly below quantifiers: A variable *occurs deeply* in a clause *C* if it occurs inside an argument of an applied variable or inside a λ-expression that is not directly below a quantifier.

Preprocessing. Our completeness theorem requires that quantified variables do not appear in certain higher-order contexts. We use preprocessing to eliminate problematic occurrences of quantifiers. The rewrite rules ∀≈ and ∃≈, which we collectively denote by Q≈, are defined as ∀τ −→-∀≈ λ*y*. *y* ≈ (λ*x*. ) and ∃τ −→-∃≈ λ*y*. *y* ≈ (λ*x*. ⊥) where the rewritten occurrence of Qτ is unapplied or has an argument of the form λ*x*. *v* such that *x* occurs as a nongreen subterm of *v*. If either of these rewrite rules can be applied to a given term, the term is Q≈*-reducible*; otherwise, it is Q≈*-normal*.

For example, the term λ*y*.∃ι → ι (λ*x*.g *x y*(*zy*) (f *x*)) is Q≈-normal. A term may be Q≈-reducible because a quantifier appears unapplied (e.g., g ∃ι ); a quantified variable occurs applied (e.g., ∃ι → ι (λ*x*. *x* a)); a quantified variable occurs inside a nested λexpression (e.g., ∀ι (λ*x*. f (λ*y*. *x*))); or a quantified variable occurs in the argument of a variable, either a free variable (e.g., ∀ι (λ*x*.*z x*)) or a variable bound above the quantifier (e.g., λ*y*. ∃ι (λ*x*. *y x*)).

A preprocessor Q≈-normalizes the input problem. Although inferences may produce Q≈-reducible clauses, we do not Q≈-normalize during the derivation process itself. Instead, Q≈-reducible ground instances of clauses will be considered redundant by the redundancy criterion. Thus, clauses whose ground instances are all Q≈-reducible can be deleted. However, there are Q≈-reducible clauses, such as *x* ∀ι ≈ a, that nevertheless have Q≈-normal ground instances. Such clauses must be kept because the completeness proof relies on their Q≈-normal ground instances.

In principle, we could omit the side condition of the Q≈-rewrite rules and eliminate all quantifiers. However, the calculus (especially, the redundancy criterion) performs better with quantifiers than with λ-expressions, which is why we restrict Q≈-normalization as much as the completeness proof allows. Extending the preprocessing to eliminate all Boolean terms as in Kotelnikov et al. [21] does not work for higher-order logic because Boolean terms can contain variables bound by enclosing λ-expressions.

Term Order. The calculus is parameterized by a well-founded strict total order on ground terms satisfying these four criteria: (O1) compatibility with green contexts i.e., *s s* implies *t s t s* ; (O2) green subterm property—i.e. *t s s* where is the reflexive closure of ; (O3) *u* ⊥ for all terms *u* ∈ { / ,⊥}; (O4) Qτ *t t u* for all types τ, terms *t*, and terms *u* such that Qτ *t* and *u* are Q≈-normal and the only Boolean green subterms of *u* are and ⊥. The restriction of (O4) to Q≈-normal terms ensures that term orders fulfilling the requirements exist, but it forces us to preprocess the input problem. We extend to literals and clauses via the multiset extensions in the standard way [2, Sect. 2.4].

For nonground terms, is required to be a strict partial order such that *t s* implies *t*θ *s*θ for all grounding substitutions θ. As in λSup, we also introduce a nonstrict variant for which we require that *t*θ *s*θ for all grounding substitutions θ whenever *t s*, and similarly for literals and clauses.

To construct a concrete order fulfilling these requirements, we define an encoding into untyped first-order terms, and compare these using a variant of the Knuth–Bendix order. In a first step, denoted*O*, the encoding translates fluid terms *t* as fresh variables *zt*; nonfluid λ-expressions λ*x*:τ. *u* as lam(*O*(τ),*O*(*u*)); applied quantifiers Qτ (λ*x*:τ. *u*) as Q1(*O*(τ),*O*(*u*)); and other termsfτ¯ *u*¯*k* asf*k*(*O*(τ¯),*O*(*u*¯*k*)). Bound variables are encoded as constants db*i* corresponding to De Bruijn indices. In a second step, denoted *P*, the

encoding replaces Q1 by Q 1 and variables *z* by *z* whenever they occur below lam. For example, ∀ι (λ*x*.p*y y* (λ*u*.f *y y* (∀ι (λ*v*.*u*)))) is encoded as ∀1(ι,p3(*y*, *y*,lam(o,f3(*y* , *y* , ∀ 1(ι,db1))))). The first-order terms can then be compared using a transfinite Knuth– Bendix order kb [22]. Let the weight of ∀1 and ∃1 be ω, the weight of 0 and ⊥0 be 1, and the weights of all other symbols be less than ω. Let the precedence > be total and ⊥0,0 be the symbols of lowest precedence, with ⊥0 > 0. Then let *t s* if *O*(*P*(*t*)) kb *O*(*P*(*s*)) and *t s* if *O*(*P*(*t*)) kb *O*(*P*(*s*)).

Selection Functions. The calculus is also parameterized by a literal selection function and a Boolean subterm selection function. We define an element *x* of a multiset *M* to be -*maximal* for some relation if for all *y* ∈ *M* with *y x*, we have *y* = *x*. It is *strictly* -maximal if it is -maximal and occurs only once in *M*.

The literal selection function *HLitSel* maps each clause to a subset of *selected literals*. A literal may not be selected if it is positive and neither side is ⊥. Moreover, a literal *L y* may not be selected if *y u*¯*n*, with *n* ≥ 1, is a -maximal term of the clause.

The Boolean subterm selection function *HBoolSel* maps each clause *C* to a subset of *selected subterms* in *C*. Selected subterms must be green subterms of Boolean type. Moreover, a subterm *s* must not be selected if *s* = , if *s* = ⊥, if *s* is a variable-headed term, if *s* is at the topmost position on either side of a positive literal, or if *s* contains a variable *y* as a green subterm, and *y u*¯*n*, with *n* ≥ 1, is a -maximal term of the clause.

Eligibility. A literal *L* is (*strictly*) *eligible* w.r.t. a substitution σ in *C* if it is selected in *C* or there are no selected literals and no selected Boolean subterms in *C* and *L*σ is (strictly) -maximal in *C*σ.

The eligible subterms of a clause *C* w.r.t. a substitution σ are inductively defined as follows: Any selected subterm is eligible. If a literal *L* = *s* ≈˙ *t* with *s*σ *t*σ is either eligible and negative or strictly eligible and positive, then the subterm *s* is eligible. If a subterm *t* is eligible and the head of *t* is not ≈ or ≈ , all direct green subterms of *t* are eligible. If a subterm *t* is eligible and *t* is of the form *u* ≈ *v* or *u* ≈ *v*, then *u* is eligible if *u*σ *v*σ and *v* is eligible if *u*σ *v*σ.

The Core Inference Rules. The calculus consists of the following core inference rules. The first five rules stem from λSup, with minor adaptions concerning Booleans:

$$\begin{array}{llll} \overbrace{\begin{subarray}{c} D \\ \begin{subarray}{c} D' \lor t \approx \bar{t} \end{subarray}}^{D} & C \{u\} \\ \hline (D' \lor C \{\forall'\}) \sigma & \text{Sup} & \overbrace{\begin{subarray}{c} C' \lor u \not\approx u' \\ C' \sigma \end{subarray}}^{C} \text{ERES} & \overbrace{\begin{subarray}{c} \widehat{C' \lor u' \approx \bar{\nu}' \lor u \approx \bar{\nu} \\ (C' \lor v \not\approx v' \lor u \approx \bar{\nu}') \sigma \end{subarray}}^{C} \text{EFS} \\ \end{array} & \overbrace{\begin{subarray}{c} \widehat{D' \lor t \approx \bar{t} \; \nu \; \begin{subarray}{c} \widehat{\pi} \\ (C' \lor v \not\approx v' \lor u \approx \bar{\nu}') \sigma \end{subarray}}^{C} \text{EFS} & \overbrace{\begin{subarray}{c} \widehat{C' \; \nu \; \begin{subarray}{c} \widehat{\pi} \\ \end{subarray}}^{C} \text{EFS} & \overbrace{\begin{subarray}{c} \widehat{\pi} \\ (C' \; \nu \; \begin{subarray}{c} \widehat{\pi} \\ \end{subarray}}^{C} \text{ARGB} \end{subarray}}^{C} \text{EFS} \\ \end{array} \text{EFS} \end{array}$$

SUP 1. *u* is not fluid; 2. *u* is not a variable deeply occurring in *C*; 3. if *u* is a variable *y*, there must exist a grounding substitution θ such that *t*σθ *t* σθ and *C*σθ ≺ *C*σθ, where *C* = *C*{*y* → *t* }; 4. σ ∈ CSU(*t*,*u*); 5. *t*σ *t* σ; 6. *u* is eligible in *C* w.r.t. σ; 7. *C*σ *D*σ; 8. *t* ≈ *t* is strictly eligible in *D* w.r.t. σ; 9. *t*σ is not a fully applied logical symbol; 10. if *t* σ = ⊥, the subterm *u* is at the top level of a positive literal. ERES 1. σ ∈ CSU(*u*,*u* ); 2. *u* ≈ *u* is eligible in *C* w.r.t. σ.

The following rules are concerned with Boolean reasoning and originate from oSup. They have been adapted to support polymorphism and applied variables.

FALSEELIM 1. σ ∈ CSU(*s* ≈ *s* , ⊥ ≈ ); 2. *s* ≈ *s* is strictly eligible in *C* w.r.t. σ.

2. *u* is not a variable; 3. *u* is eligible in *C* w.r.t. σ; 4. if the head of *u* is a variable, it must be applied and the affected literal must be of the form *u* ≈ , *u* ≈ ⊥, or *u* ≈ *v* where *v* is a variable-headed term; 5. for FORALLRW, the indicated occurrence of *u* is not in a literal *u* ≈ , and for EXISTSRW, the indicated occurrence of *u* is not in a literal *u* ≈ ⊥.

Like SUP, also the Boolean rules must be simulated in fluid terms. The following rules are Boolean counterparts of FLUIDSUP:

$$\frac{\mathcal{C}\langle u\rangle}{(\mathcal{C}\langle z\Delta\rangle \vee x \approx \mathsf{T})\sigma} \frac{\mathsf{F}\_{\mathsf{LU}\mathsf{UD}\mathsf{T}}}{\mathsf{Bool}\mathsf{LD}\mathsf{Hom}\mathsf{T}} \qquad \frac{\mathcal{C}\langle u\rangle}{(\mathcal{C}\langle z\mathsf{T}\rangle \vee x \approx \mathsf{\Delta})\sigma} \frac{\mathsf{F}\_{\mathsf{LU}\mathsf{UD}\mathsf{T}}}{\mathsf{Loo}\mathsf{Hom}\mathsf{Hom}\mathsf{T}}$$

FLUIDBOOLHOIST 1. *u* is fluid; 2. *z* and *x* are fresh variables; 3. σ ∈ CSU(*z x*, *u*); 4. (*z* ⊥)σ = (*z x*)σ; 5. *x*σ = and *x*σ = ⊥; 6. *u* is eligible in C w.r.t. σ.

FLUIDLOOBHOIST Like the above but with ⊥ replaced by in condition 4.