where $t'[\psi'] \doteq t[\psi]$, $\mathcal{V}ar(s, \phi) \cap \mathcal{V}ar(t', \psi') = \emptyset$, and $\sigma = \text{mgu}(s, t')$.

By definition, it is clear that $s[\phi] \ominus s'[\phi'] = \emptyset$ for any value-free constrained pattern $s'[\phi']$ such that $s'[\phi'] \doteq s[\phi]$.

**Example 4.7.** For $\Sigma_1 = \{\text{f}, \text{nil}, \text{cons}\} \cup \{\text{n} \mid n \in \mathbb{Z}\}$, we have that $f(xs, y)[\text{true}] \ominus f(\text{nil}, y_1)[y_1 \le 0] = \{f(\text{nil}, y_a)[\neg(y_a \le 0)], f(\text{cons}(x', xs'), y')[\text{true}]\}$. In addition to $\Sigma_1$, let us consider a defined symbol $\mathfrak{g} : \text{list} \times \text{list} \to \text{list}$. A complement of the term $\mathfrak{g}(x, x)[\text{true}]$ is, e.g., $\{\mathfrak{g}(t_1, t_2) \mid t_1 : \text{list}, t_2 : \text{list} \in T(C'_1), t_1 \ne t_2\}$, and there is no finite complement of $\mathfrak{g}(x, x)[\text{true}]$ (cf. [27, Proposition 4.5]).

The following theorem shows correctness of $\ominus$ over constrained patterns.

**Theorem 4.8 (correctness of $s[\phi] \ominus t[\psi]$).** For a value-free constrained pattern $s[\phi] : \iota$ and a value-free constrained linear pattern $t[\psi]$, $s[\phi] \ominus t[\psi]$ is a finite set of value-free constrained patterns with sort $\iota$ such that

1. $\mathcal{G}_C(u[\varphi]) \cap \mathcal{G}_C(u'[\varphi]) = \emptyset$ for any different constrained patterns $u[\varphi], u'[\varphi'] \in (s[\phi] \ominus t[\psi])$,

2. if $s[\phi]$ is linear, then $s[\phi] \ominus t[\psi]$ is a set of constrained linear patterns,

3. $s < u$ for any constrained term $u[\varphi] \in (s[\phi] \ominus t[\psi])$,

4. $\max\{\text{height}(s), \text{height}(t)\} \ge \text{height}(u)$ for any term $u[\varphi] \in (s[\phi] \ominus t[\psi])$, and

5. $\mathcal{G}_C(s[\phi] \ominus t[\psi]) = \mathcal{G}_C(s[\phi]) \setminus \mathcal{G}_C(t[\psi])$.

*Proof (Sketch).* This can be proved as a straightforward extension of the correctness proof for unconstrained patterns to constrained ones by means of the following properties: $\{s\rho \mid \rho \in \bar{\sigma}, s\rho \ne s\sigma\}$ is a set of value-free patterns; $\sigma|_{\mathcal{V}_{ar}(\phi, \psi')} = \rho|_{\mathcal{V}_{ar}(\phi, \psi')}$ for any $\rho \in \bar{\sigma}$; $\mathcal{G}_C(s\sigma[\phi\sigma]) = \mathcal{G}_C(s\sigma[\phi\sigma \wedge \psi'\sigma]) \cup \mathcal{G}_C(s\sigma[\phi\sigma \wedge \neg\psi'\sigma])$ for an arbitrary constraint $\psi'$. A complete proof can be seen in [31]. $\square$

# 5 Complements of Constrained Patterns

In this section, we first extend the complement algorithm for unconstrained linear patterns in [15, 27, 28] to constrained patterns. Then, using the extended complement algorithm, we show that quasi-reducibility is decidable for left-linear LCTRSs over a signature $\Sigma$ with decidable built-in theories such that $\Sigma_{terms}$ is finite and there is no constructor $c : \iota_1 \times \dots \times \iota \in C_R$ with $\iota \in S_{theory}$.

Complements of constrained patterns are defined as a straightforward extension of complements of unconstrained patterns.

**Definition 5.1 (complement of constrained patterns).** A set $P$ of constrained patterns is called a complement of a set $P'$ of constrained patterns w.r.t. an $n$-ary defined symbol $f \in \mathcal{D}$ if $\mathcal{G}_C(P) = \mathcal{G}_C(\{f(x_1, \dots, x_n)\}) \setminus \mathcal{G}_C(P')$, where $x_1, \dots, x_n$ are pairwise distinct variables. A set $P$ of constrained patterns is called a complement of a constrained pattern $f(s_1, \dots, s_n)[\phi]$ if $P$ is a complement of $\{f(s_1, \dots, s_n)[\phi]\}$ w.r.t. $f$. A set $P$ of constrained patterns is called a complement of a set $P'$ of constrained patterns if $\mathcal{G}_C(P) = \mathcal{G}_C(\{f(x_1, \dots, x_n) \mid f \in \mathcal{D}\}) \setminus \mathcal{G}_C(P')$, where $x_1, \dots, x_n$ are pairwise distinct variables.
Note that as for unconstrained patterns, complements of constrained patterns are not unique.

*Example 5.2.* Let us consider the $S_1$-sorted signature $\Sigma_1$ in Example 1.1 again. The set $\{(\text{a}) f(\text{nil}, y_a) [\neg(y_a \le 0)], (\text{b}) f(\text{cons}(x_b, \text{nil}), y_b) [\text{true}]\}$ is a complement of $(\text{1}) f(\text{nil}, y_1) [y \le 0]$.

## 5.1 Difference Operator over Sets of Constrained Patterns

The complement algorithm in [15,27,28] is defined by the repetition of applying the difference operator $\ominus$ over patterns. Thus, as in [15,27,28], we extend $\ominus$ to finite sets of constrained patterns in order to have the results in Example 1.2.

In computing $P \ominus Q$, if there exist constrained patterns $s[\phi] \in P$ and $t[\psi] \in Q$ such that $s[\phi] \ominus t[\psi] \ne \{s[\phi]\}$, then we recursively compute $((P \setminus \{s[\phi]\}) \cup (s[\phi] \ominus t[\psi])) \ominus ((Q \setminus \{t[\psi]\}) \cup (t[\psi] \ominus s[\phi]))$. In Sect. 4.2, we required divisors of $\ominus$ to be linear, and thus $t[\psi]$ has to be linear. It is difficult to know which constrained terms are selected as a divisor for $\ominus$ over constrained patterns. For this reason, to ensure the linear of divisors for the application of $\ominus$ to constrained patterns, we assume that all constrained terms in $Q$ are linear, while not all of them may be necessarily linear. Then, for the recursive call of $\ominus$ for sets of constrained patterns, we would like to ensure that all constrained patterns in $(Q \setminus \{t[\psi]\}) \cup (t[\psi] \ominus s[\phi])$ are linear. Since $Q$ is assumed to be linear in advance, we need to ensure that all constrained patterns in $t[\psi] \ominus s[\phi]$ are linear. Therefore, for the extension of $\ominus$ to sets of constrained patterns, we assume that all constrained patterns in $P$ are linear, as well as $Q$.

**Definition 5.3 ($\ominus$ over sets of value-free constrained linear patterns).**

We extend $\ominus$ for finite sets of value-free constrained linear patterns as follows: For finite sets $P, Q$ of value-free constrained linear patterns,

$$ P \ominus Q = \begin{cases} (P' \cup (s[\phi] \ominus t[\psi])) \ominus (Q' \cup (t[\psi] \ominus s[\phi])) & \text{if } P = P' \ominus \{s[\phi]\}, Q = Q' \ominus \{t[\psi]\}, \text{ and } s[\phi] \ominus t[\psi] \ne \{s[\phi]\} \\ P & \text{otherwise} \end{cases} $$

Since $\ominus$ over sets of value-free constrained linear patterns is non-deterministic, there may be two or more sets that can be results of $P \ominus Q$, while all the results are correct. In addition, a result of $P \ominus Q$ is not always minimal. Note that using $\bar{\sigma}$, $s[\phi] \ominus t[\psi]$ and $t[\psi] \ominus s[\phi]$ can be computed simultaneously.
**Example 5.4.** For $\Sigma_1 = \{\text{f}, \text{nil}, \text{cons}\} \cup \{\text{n} \mid n \in \mathbb{Z}\}$, we have that

$$ \begin{aligned} \{\text{f}(xs, y) [\text{true}]\} &\ominus \left\{ \begin{array}{ll} (1) & \text{f}(\text{nil}, y_1) [y_1 \le 0], \\ (2) & \text{f}(\text{cons}(x_2, xs_2), y_2) [x_2 \le 0 \land y_2 > 0], \\ (3) & \text{f}(\text{cons}(x_3, \text{cons}(z_3, zs_3)), y_3) [x_3 > 0 \land y_3 > 1] \end{array} \right\} \\ &= \left\{ \begin{array}{ll} (a) & \text{f}(\text{nil}, y_a) [\neg(y_a \le 0)], \\ (1') & \text{f}(\text{cons}(x', xs'), y') [\text{true}] \end{array} \right\} \ominus \{(2), (3)\} \\ &= \left\{ \begin{array}{ll} (a) & \text{f}(\text{nil}, y_a) [\neg(y_a \le 0)], \\ (2') & \text{f}(\text{cons}(x', xs'), y') [\neg(x' \le 0 \land y' > 0)] \end{array} \right\} \ominus \{(3)\} \\ &= \left\{ \begin{array}{ll} (a) & \text{f}(\text{nil}, y_a) [\neg(y_a \le 0)], \\ (b) & \text{f}(\text{cons}(x_b, \text{nil}), y_b) [\text{true}], \\ (c) & \text{f}(\text{cons}(x_c, \text{cons}(z_c, zs_c)), y_c) [\neg(x_c \le 0 \land y_c > 0) \land \neg(x_c > 0 \land y_c > 1)] \end{array} \right\} \ominus \emptyset \\ &= \{(a), (b), (c)\} \end{aligned} $$

A key for correctness of $\ominus$ over sets of (constrained) linear patterns is non-overlappingness between (constrained) patterns in dividends sets of $\ominus$. We define a notion of non-overlappingness of constrained patterns and their sets.

**Definition 5.5 (C-non-overlappingness of constrained terms).** Two constrained terms $s[\phi]$, $t[\psi]$ are called non-overlapping w.r.t. $\mathcal{C}$ (C-non-overlapping, for short) if $\mathcal{G}_C(s[\phi]) \cap \mathcal{G}_C(t[\psi]) = \emptyset$. Two sets $P, Q$ of constrained terms are said to be C-non-overlapping if $\mathcal{G}_C(P) \cap \mathcal{G}_C(Q) = \emptyset$. A set $P$ of constrained terms is said to be pairwise C-non-overlapping if any two different constrained terms $s[\phi]$, $t[\psi] \in P$ are C-non-overlapping.

**Example 5.6.** The constrained terms $\text{f}(\text{nil}, y_1)$ $[y_1 \le 0]$ and $\text{f}(\text{nil}, y_a)$ $[\neg(y_a \le 0)]$ are $C_1$-non-overlapping, but $\text{f}(\text{nil}, y_1)$ $[y_1 \le 0]$ and $\text{f}(xs, y)$ [true] are not $C_1$-non-overlapping because, e.g., $\text{f}(\text{nil}, 0) \in \mathcal{G}_{C_1}(\text{f}(\text{nil}, y_1))$ $[y_1 \le 0] \cap \mathcal{G}_{C_1}(\text{f}(xs, y))$ [true].

Note that non-overlappingness and unifiability of constrained patterns are dual properties: $s[\phi]$, $t[\psi]$ are C-non-overlapping if and only if $s[\phi]$ and $t'[\psi']$ are not unifiable, where $t'[\psi'] \doteq t[\psi]$ and $\text{Var}(s, \phi) \cap \text{Var}(t', \psi') = \emptyset$.

For correctness of $P \ominus Q$, we assume that $P$ is pairwise C-non-overlappingness.

**Example 5.7.** For $\Sigma_1 = \{\text{f}, \text{nil}, \text{cons}\} \cup \{\text{n} \mid n \in \mathbb{Z}\}$, we have that a result of $\{\text{f}(\text{nil}, y) [\text{true}], \text{f}(xs, y) [\text{true}]\} \ominus \{\text{f}(xs', y') [\text{true}]\}$ is $\{\text{f}(\text{nil}, y) [\text{true}]\}$, which is not an expected one. Since $\text{f}(xs, y) \lesssim \text{f}(\text{nil}, y)$, the set $\{\text{f}(\text{nil}, y) [\text{true}], \text{f}(xs, y) [\text{true}]\}$ is redundant from the viewpoint of ground instances.

The following proposition shows the correctness of $\ominus$ over sets of value-free constrained linear patterns.

**Theorem 5.8 (correctness of $P \ominus Q$).** Let $P, Q$ be finite sets of value-free constrained linear patterns. If $P$ is pairwise C-non-overlapping, then $P \ominus Q$ is a pairwise C-non-overlapping finite set of value-free constrained linear patterns such that $\mathcal{G}_C(P \ominus Q) = \mathcal{G}_C(P) \setminus \mathcal{G}_C(Q)$.
**Proof (Sketch).** To prove this claim, we show that for finite sets $P, Q$ of value-free constrained linear patterns, all of the following hold: (i) if $P$ is pairwise $C$-non-overlapping, $P = P' \uplus \{s[\phi]\}, Q = Q' \uplus \{t[\psi]\}$, and $s[\phi] \ominus t[\psi] \neq \{s[\phi]\}$, then $P'$ and $\{s[\phi] \ominus t[\psi]\}$ are $C$-non-overlapping, and (ii) if $P$ is pairwise $C$-non-overlapping, then $\mathcal{G}_C(P \ominus Q) = \mathcal{G}_C(P) \setminus \mathcal{G}_C(Q)$.

The first statement (i) is a straightforward extension of the corresponding statement for unconstrained linear patterns to constrained ones. The difficulty of the second statement (ii) is the well-founded order for induction. Let $h$ be the maximum height of terms in $P, Q$. Then, in computing $P \ominus Q$, the heights of all terms considered during the computation are less than or equal to $h$, and thus such terms are finitely many. We denote by $T(\Sigma, \mathcal{V})_{\le h}$ the set of terms whose heights are less than or equal to $h$. Then, We define a quasi-order $\tilde{\le}_{\le h}$ over terms in $T(\Sigma, \mathcal{V})_{\le h}$ as follows: $s \tilde{\le}_{\le h} t$ if and only if $s \lesssim t$, $\text{height}(s) \le h$, and $\text{height}(t) \le h$. The strict part $\succ_{< h}$ of $\tilde{\le}_{\le h}$ is defined as $\succ_{\le h} = (\tilde{\le}_{\le h} \setminus \tilde{\le}_{\ge h})$. Note that $s \succ_{\le h} t$ if and only if $s < t$, $\text{height}(s) \le h$, and $\text{height}(t) \le h$. In computing $s[\phi] \ominus t[\psi]$, the resulting set may contain $s\sigma[\phi\sigma \wedge \neg\psi'\sigma]$ and we may have that $s = s\sigma$ (and thus $(\phi\sigma \wedge \neg\psi'\sigma) = (\phi \wedge \neg\psi')$. On the other hand, since $\phi \wedge \psi'$ and $\neg\psi'$ are satisfiable, we have that $\{\theta | \llbracket \phi\theta \rrbracket = \top\} \supset \{\theta | \llbracket (\phi \wedge \neg\psi')\theta \rrbracket = \top\}$. However, the sets may be infinite, and thus the relation $\supset$ for the sets is not well-founded in general. To overcome the problem, we consider the number of constrained terms $t[\psi]$ such that $s[\phi] \ominus t[\psi] \neq \{s[\phi]\}$. Let $\tilde{\le}_{h,N}$ be the order of lexicographic products of terms and natural numbers compared by $\tilde{\le}_{\le h}$ and $\ge_N$. Let $\succ_{\le h,N} = (\tilde{\le}_{h,N} \setminus \tilde{\le}_{\ge h,N})$. Then, it is clear that $\succ_{\le h,N}$ is well-founded. We define the weight $w$ for pairs of sets of constrained linear patterns as follows: $w(P, Q) = \{(s, n) \mid s[\phi] \in P, n = \{|t[\psi] \in Q \mid s[\phi] \ominus t[\phi] \neq \{s[\phi]\}\} \mid w(P, Q) = \{(s, n) \mid s[\phi] \in P, n = \{|t[\psi] \in Q \mid s[\phi] \ominus t[\psi] \neq \{s[\phi]\}\} \mid w(P, Q) \ge h, N\}$ with the weight $w$. A complete proof can be seen in [31]. $\square$

Note that for $P \ominus Q$, if there are no constrained terms $s[\phi] \in P$ and $t[\psi] \in Q$ such that $s[\phi] \in P$ and $t[\psi] \in Q$ are not unifiable, then neither $P$ nor $Q$ must be a set of constrained linear patterns and $P$ must not be pairwise $C$-non-overlapping.

## 5.2 Complement Algorithm for Constrained Linear Patterns

In this section, we first show a complement algorithm for sets of value-free constrained linear patterns, and then show that quasi-reducibility is decidable for some class of left-linear LCTRSs with decidable built-in theories.

**Definition 5.9.** Let $f$ be an $n$-ary defined symbol in $\mathcal{D}$, and $Q$ be a finite set of value-free constrained linear patterns. Then, we define a finite set $(\overline{Q})_f$ of constrained patterns as follows: $(\overline{Q})_f = \{f(x_1, \dots, x_n) [\text{true}]\} \ominus Q$, where $x_1, \dots, x_n$ are pairwise distinct variables. We extend $(\cdot)_f$ for $\mathcal{D}$ as follows: $\overline{Q} = \bigcup_{f \in \mathcal{D}} (\overline{Q})_f$. \\

**Example 5.10.** For $\Sigma_1 = \{\text{f}, \text{nil}, \text{cons}\} \cup \{\text{n} \mid n \in \mathbb{Z}\}$ in Example 1.1, we have that $\{(1), (2), (3)\} = (\{(1), (2), (3)\})_f = \{(\text{a}), (\text{b}), (\text{c})\}$.
As a direct consequence of Theorem 5.8, the following claim holds for $\overline{(\cdot)}_f$.

**Theorem 5.11.** Let $Q$ be a pairwise $C$-non-overlapping finite set of value-free constrained linear patterns, and $f$ an $n$-ary defined symbol in $D$. Then, $G_C(\overline{(Q)}_f) = G_C(f(x_1, \dots, x_n) [\text{true}]) \setminus G_C(\{t[\psi] \in Q \mid \text{root}(t) = f\})$ and $\overline{(Q)}_f$ is a complement of $Q$ w.r.t. $f$, where $x_1, \dots, x_n$ are pairwise distinct variables.

*Proof (Sketch).* By definition, during the computation of $\overline{(Q)}_f$, all constrained patterns in the left-hand sides of $\ominus$ are rooted by $f$. Thus, no constrained term $t[\psi]$ in $Q$ such that $\text{root}(t) \neq f$ is not unifiable with any constrained pattern in the left-hand sides of $\ominus$, and hence $\{f(x_1, \dots, x_n) [\text{true}]\} \ominus Q = \{f(x_1, \dots, x_n) [\text{true}]\} \ominus \{t[\psi] \in Q \mid \text{root}(t) = f\}$. Then, by Theorem 5.8, $\overline{(Q)}_f$ is a complement of $Q$ w.r.t. $f$. A complete proof can be seen in [31]. □

The following corollary is a direct consequence of Theorem 5.11.

**Corollary 5.12.** For a pairwise $C$-non-overlapping finite set $Q$ of value-free constrained linear patterns, $G_C(\overline{Q}) = G_C(\{f(x_1, \dots, x_n) \mid f \in D\}) \setminus G_C(Q)$, where $x_1, \dots, x_n$ are pairwise distinct variables.

Corollary 5.12 immediately implies decidability of quasi-reducibility for left-linear LCTRSs with decidable built-in theories.

**Theorem 5.13.** Let $\mathcal{R}$ be a finite left-linear LCTRS such that $\Sigma_{\text{terms}}$ is finite and there is no constructor $c : \iota_1 \times \dots \times \iota \to \mathcal{C}_{\mathcal{R}}$ with $\iota \in \mathcal{S}_{\text{theory}}$. Then, $\mathcal{R}$ is quasi-reducible if and only if $\{\tilde{\ell}[\tilde{\phi}] \mid \ell \to r [\phi] \in \mathcal{R}, \ell \text{ is a pattern}\} = \emptyset$. Thus, quasi-reducibility is decidable for such LCTRSs with decidable built-in theories.<fnref n="4" />

*Proof (Sketch).* Since the built-in theory is decidable, by the well-founded order in the proof of Theorem 5.8, the set $\{\tilde{\ell}[\tilde{\phi}] \mid \ell \to r [\phi] \in \mathcal{R}, \ell \text{ is a pattern}\}$ is computable, and thus its emptiness is decidable. Therefore, quasi-reducibility of $\mathcal{R}$ is decidable. A complete proof can be seen in [31]. □

*Example 5.14.* The LCTRS $\mathcal{R}_1$ in Example 1.1 is not quasi-reducible because $\{f(xs, y) [\text{true}]\} \ominus \{(1), (2), (3)\} = \{(\text{a}), (\text{b}), (\text{c})\}$. On the other hand, the LCTRS $\mathcal{R}'_1$ is quasi-reducible because $\{f(xs, y) [\text{true}]\} \ominus \{(1), (2), (3), (\text{a}), (\text{b}), (\text{c})\} = \emptyset$.

# 6 Related Work

As mentioned before, to the best of our knowledge, there is no work for difference operators and complement algorithms for constrained patterns, and decidability of quasi-reducibility in the LCTRS setting, while some sufficient conditions have been investigated [24,37].

<footnote n="4">⁴ It is sufficient that all constraints of constrained rewrite rules in $\mathcal{R}$ are in a class of a decidable theory. For example, the integer theory is not decidable, but the constraints of $\mathcal{R}_1$ and $\mathcal{R}'_1$ are formulas of Presburger arithmetic.</footnote>
There are several works on quasi-reducibility and sufficient completeness of TRSs and constrained rewrite systems. Decidability of quasi-reducibility has been shown in [18] without yielding a practical algorithm. Then, complement algorithms have been proposed [15, 27, 28], which are used as decision procedures for quasi-reducibility of left-linear TRSs. *Negation elimination* from equational formulas [12,39] is a well-investigated application of complement algorithms. *Tree automata techniques* [11] can be used to obtain complements, and thus they also yield decision procedures for quasi-reducibility of left-linear TRSs. Recently, a well-designed decision procedure for quasi-reducibility of TRSs has been proposed [40]. However, to the best of our knowledge, the above procedures have not yet been extended to constrained rewrite systems, and the extension is not so trivial.

Sufficient completeness is equivalent to quasi-reducibility for terminating systems. A sufficient condition for sufficient completeness of constrained and conditional rewrite systems based on constrained tree automata techniques has been shown in [6]. In addition, as mentioned in Sect. 1, an SMT-based sufficient condition for left-patternless constrained rewrite systems [23,37] and a procedural sufficient condition for quasi-reducibility of LCTRSs [24] have been shown.

For programming languages, there are some works on the exhaustiveness checking. In [29], a method for examining pattern-matching anomalies of ML programming languages has been proposed. This method checks two points: there are no useless patterns, and it considers all patterns. This method is implemented on OCaml but is also useful for Haskell. However, guards are not considered: Standard ML of New Jersey does not allow us to write guards for pattern matching; a recent version of the GHC implementation of Haskell does not implement any form of exhaustiveness checking even without guards, while there is a check for redundancy of patterns, which does not work for guards. When compiling programs, OCaml compilers warn users about guard constraints attached to patterns so that they can take care of the exhaustiveness of constrained patterns, which is not checked by the compilers. As mentioned before, due to the SMT solving for supported built-in theories, the exhaustiveness checking for guarded patterns is not realistic.

Unification of constrained terms in Definition 4.4 is a bit different from unification modulo built-ins [9, Definition 11]. Unlike ours, the unification is defined for terms, and unifiers are pairs of substitutions and constraints.

Another related work on unification of constrained terms is unification with abstraction and theory instantiation for SMT solving [35]. The algorithm for such unification is very similar to the syntactic unification procedure [3, Section 4.6], while it considers underlying theories and disequalities as constraints. Unlike the algorithm, our unification of constrained terms $s[\phi], t[\psi]$ first uses syntactic unification to obtain an mgu $\sigma$ of $s$ and $t$, and then check satisfiability of $\phi\sigma \wedge \psi\sigma$.

*Matching logic* [7, 8, 36] (ML, for short) is a first-order logic variant to reason about structures by allowing formulas to represent terms, and is expressive enough and very powerful. For example, $s \ominus t$ with $Var(s) \cap Var(t) = \emptyset$ can be
represented by the formula $s \wedge \neg t$. However, decidability of ML formulas is not clear due to its generality.

# 7 Conclusion

In this paper, we extended the difference operator and the complement algorithm in the unconstrained setting to constrained linear patterns, proposing a difference operator and a complement algorithm for constrained linear patterns used in LCTRSs that have finitely many user-defined function symbols and have no user-defined constructor term with a theory sort for built-in value-constants. Then, we showed that quasi-reducibility is decidable for such LCTRSs. Many LCTRSs obtained from practical programs by existing transformations belong to the class. We will implement the algorithm in our LCTRS tool as future work.

For brevity, we had some restrictions, e.g., non-existence of user-defined constructor terms with theory sorts. A future work is to drop such restrictions, proposing a difference operator and a complement algorithm for more general classes of LCTRSs.

The complexity of the complement algorithm for constrained linear patterns relies on that of SMT solving used in the computation. We are interested in complexity of the algorithm without the complexity of SMT solving. Analysis of such complexity is another future work.

# References

1. Aoto, T., Nishida, N., Schöpf, J.: Equational theories and validity for logically constrained term rewriting. In: Rehof, J. (ed.) Proceedings of the 9th International Conference on Formal Structures for Computation and Deduction. Leibniz International Proceedings in Informatics, vol. 299, pp. 31:1–31:21. Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024). https://doi.org/10.4230/LIPICS.FSCD.2024.31

2. Aoto, T., Toyama, Y., Kimura, Y.: Improving rewriting induction approach for proving ground confluence. In: Miller, D. (ed.) Proceedings of the 2nd International Conference on Formal Structures for Computation and Deduction. LIPIcs, vol. 84, pp. 7:1–7:18. Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017). https://doi.org/10.4230/LIPICS.FSCD.2017.7

3. Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press (1998). https://doi.org/10.1145/505863.505888

4. Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB) (2016). https://www.SMT-LIB.org

5. Barrett, C.W., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 336, pp. 1267–1329, 2nd edn. IOS Press (2021). https://doi.org/10.3233/FAIA201017

6. Bouhoula, A., Jacquemard, F.: Sufficient completeness verification for conditional and constrained TRS. J. Appl. Log. 10(1), 127–143 (2012). https://doi.org/10.1016/J.JAL.2011.09.001
7. Chen, X., Roșu, G.: Matching µ-logic. In: Proceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science, pp. 1–13. IEEE (2019). https://doi.org/10.1109/LICS.2019.8785675

8. Chen, X., Roșu, G.: Matching mu-logic: foundation of K framework (invited paper). In: Roggenbach, M., Sokolova, A. (eds.) Proceedings of the 8th Conference on Algebra and Coalgebra in Computer Science. LIPIcs, vol. 139, pp. 1:1–1:4. Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019). https://doi.org/10.4230/LIPICS.CALCO.2019.1

9. Ciobăcă, Ș, Arusoaie, A., Lucanu, D.: Unification modulo builtins. In: Moss, L.S., de Queiroz, R., Martinez, M. (eds.) WoLLIC 2018. LNCS, vol. 10944, pp. 179–195. Springer, Heidelberg (2018). https://doi.org/10.1007/978-3-662-57669-4_10

10. Ciobăcă, Ș, Lucanu, D.: A coinductive approach to proving reachability properties in logically constrained term rewriting systems. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds.) IJCAR 2018. LNCS (LNAI), vol. 10900, pp. 295–311. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-94205-6_20

11. Comon, H., et al.: Tree automata techniques and applications (2007). http://www.grappa.univ-lille3.fr/tata

12. Fernández, M.: Negation elimination in empty or permutative theories. J. Symb. Comput. 26(1), 97–133 (1998). https://doi.org/10.1006/JSCO.1998.0203

13. Fuhs, C., Guo, L., Kop, C.: An innermost DP framework for constrained higher-order rewriting. In: Fernández, M. (ed.) Proceedings of the 10th International Conference on Formal Structures for Computation and Deduction. LIPIcs, vol. 337, pp. 20:1–20:24. Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025). https://doi.org/10.4230/LIPICS.FSCD.2025.20

14. Fuhs, C., Kop, C., Nishida, N.: Verifying procedural programs via constrained rewriting induction. ACM Trans. Comput. Logic 18(2), 14:1–14:50 (2017). https://doi.org/10.1145/3060143

15. Higashiwada, N., Aoto, T.: Automatically proving sufficient completeness of conditional term rewriting systems. In: Manuscript for the presentation at the 124th Workshop of IPSJ Special Interest Group on Programming, pp. 1–6 (2019). (in Japanese)

16. Kanazawa, Y., Nishida, N.: On transforming functions accessing global variables into logically constrained term rewriting systems. In: Niehren, J., Sabel, D. (eds.) Proceedings of the 5th International Workshop on Rewriting Techniques for Program Transformations and Evaluation. Electronic Proceedings in Theoretical Computer Science, vol. 289, pp. 34–52. Open Publishing Association (2019)

17. Kanazawa, Y., Nishida, N., Sakai, M.: On representation of structures and unions in logically constrained rewriting. In: IEICE Technical Report SS2018-38, the Institute of Electronics, Information and Communication Engineers, vol. 118, no. 385, pp. 67–72 (2019). (in Japanese)

18. Kapur, D., Narendran, P., Zhang, H.: On sufficient-completeness and related properties of term rewriting systems. Acta Informatica 24(4), 395–415 (1987). https://doi.org/10.1007/BF00292110

19. Kojima, M., Nishida, N.: From starvation freedom to all-path reachability problems in constrained rewriting. In: Hanus, M., Inclezan, D. (eds.) PADL 2023. LNCS, vol. 13880, pp. 161–179. Springer, Cham (2023). https://doi.org/10.1007/978-3-031-24841-2_11

20. Kojima, M., Nishida, N.: Reducing non-occurrence of specified runtime errors to all-path reachability problems of constrained rewriting. J. Logical Algebraic Methods Program. 135, 1–19 (2023). https://doi.org/10.1016/j.jlamp.2023.100903
21. Kojima, M., Nishida, N.: A sufficient condition of logically constrained term rewrite systems for decidability of all-path reachability problems with constant destinations. J. Inf. Process. 32, 417–435 (2024)

22. Kojima, M., Nishida, N., Matsubara, Y.: Transforming concurrent programs with semaphores into logically constrained term rewrite systems. In: Riesco, A., Nigam, V. (eds.) Informal Proceedings of the 7th International Workshop on Rewriting Techniques for Program Transformations and Evaluation, pp. 1–12 (2020)

23. Kojima, M., Nishida, N., Matsubara, Y.: Transforming concurrent programs with semaphores into logically constrained term rewrite systems. J. Logical Algebraic Methods Program. 143, 1–23 (2025). https://doi.org/10.1016/j.jlamp.2024.101033

24. Kop, C.: Quasi-reductivity of logically constrained term rewriting systems. CoRR abs/1702.02397 (2017). http://arxiv.org/abs/1702.02397

25. Kop, C., Nishida, N.: Term rewriting with logical constraints. In: Fontaine, P., Ringeissen, C., Schmidt, R.A. (eds.) FroCoS 2013. LNCS (LNAI), vol. 8152, pp. 343–358. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-40885-4_24

26. Kop, C., Nishida, N.: Constrained term rewriting tool. In: Davis, M., Fehnker, A., McIver, A., Voronkov, A. (eds.) LPAR 2015. LNCS, vol. 9450, pp. 549–557. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-48899-7_38

27. Lassez, J.-L., Marriott, K.: Explicit representation of terms defined by counter examples. In: Nori, K.V. (ed.) FSTTCS 1986. LNCS, vol. 241, pp. 96–107. Springer, Heidelberg (1986). https://doi.org/10.1007/3-540-17179-7_6

28. Lazrek, A., Lescanne, P., Thiel, J.J.: Tools for proving inductive equalities, relative completeness, and $\omega$-completeness. Inf. Comput. 84(1), 47–70 (1990). https://doi.org/10.1016/0890-5401(90)90033-E

29. Maranget, L.: Warnings for pattern matching. J. Funct. Program. 17(3), 387–421 (2007). https://doi.org/10.1017/s0956796807006223

30. Nishida, N., Kojima, M., Matsumi, A.: A nesting-preserving transformation of SIMP programs into logically constrained term rewrite systems. J. Logical Algebraic Methods Program. 144, 1–15 (2025). https://doi.org/10.1016/j.jlamp.2025.101045

31. Nishida, N., Kojima, M., Nakamura, Y.: Difference of constrained patterns in logically constrained term rewrite systems (full version). CoRR abs/2505.04080 (2025). https://doi.org/10.48550/arXiv.2507.04080

32. Nishida, N., Winkler, S.: Loop detection by logically constrained term rewriting. In: Piskac, R., Rümmer, P. (eds.) VSTTE 2018. LNCS, vol. 11294, pp. 309–321. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-03592-1_18

33. Ohlebusch, E.: Advanced Topics in Term Rewriting. Springer, Cham (2002). https://doi.org/10.1007/978-1-4757-3661-8

34. Reddy, U.S.: Term rewriting induction. In: Stickel, M.E. (ed.) CADE 1990. LNCS, vol. 449, pp. 162–177. Springer, Heidelberg (1990). https://doi.org/10.1007/3-540-52885-7_86

35. Reger, G., Suda, M., Voronkov, A.: Unification with abstraction and theory instatiation in saturation-based reasoning. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10805, pp. 3–22. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-89960-2_1

36. Rosu, G.: Matching logic. Logical Methods Comput. Sci. 13(4) (2017). https://doi.org/10.23638/LMCS-13(4:28)2017

37. Sakata, T., Nishida, N., Sakabe, T., Sakai, M., Kusakari, K.: Rewriting induction for constrained term rewriting systems. IPSJ Trans. Program. 2(2), 80–96
(2009). (in Japanese) (a translated summary is available from https://www.trs.css.i.nagoya-u.ac.jp/crisys/)

38. Schöpf, J., Mitterwallner, F., Middeldorp, A.: Confluence of logically constrained rewrite systems revisited. In: Benzmüller, C., Heule, M.J.H., Schmidt, R.A. (eds.) Automated Reasoning. LNCS, vol. 14740, pp. 298–316. Springer, Cham (2024). https://doi.org/10.1007/978-3-031-63501-4_16

39. Tajine, M.: The negation elimination from syntactic equational formula is decidable. In: Kirchner, C. (ed.) RTA 1993. LNCS, vol. 690, pp. 316–327. Springer, Heidelberg (1993). https://doi.org/10.1007/978-3-662-21551-7_24

40. Thiemann, R., Yamada, A.: A verified algorithm for deciding pattern completeness. In: Rehof, J. (ed.) Proceedings of the 9th International Conference on Formal Structures for Computation and Deduction. LIPIcs, vol. 299, pp. 27:1–27:17. Schloss Dagstuhl–Leibniz-Zentrum für Informatik (2024). https://doi.org/10.4230/LIPICS.FSCD.2024.27

41. Winkler, S., Middeldorp, A.: Completion for logically constrained rewriting. In: Kirchner, H. (ed.) Proceedings of the 3rd International Conference on Formal Structures for Computation and Deduction. Leibniz International Proceedings in Informatics, vol. 108, pp. 30:1–30:18. Schloss Dagstuhl–Leibniz-Zentrum für Informatik (2018). https://doi.org/10.4230/LIPIcs.FSCD.2018.30

**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.
Theorem Proving
Iterative Monomorphisation

Tanguy Bozec¹,²(✉) and Jasmin Blanchette²(✉)

¹ ENS Paris-Saclay, Université Paris-Saclay, Gif-sur-Yvette, France

² Ludwig-Maximilians-Universität München, Munich, Germany

tanguy.bozec@ens-paris-saclay.fr

**Abstract.** Monomorphisation can be used to extend monomorphic provers to support polymorphic logics. We describe a pragmatic iterative approach. We implemented it in the Zipperposition prover, where it is used to translate away polymorphism before invoking the monomorphic prover E as a backend. Our evaluation shows that this approach increases Zipperposition's success rate. Moreover, we find that iterative monomorphisation outperforms some native implementations of polymorphism.

**Keywords:** Polymorphism · monomorphism · automated reasoning

# 1 Introduction

Automatic theorem provers provide automation for proof assistant users. Many proof assistants, such as HOL4 [16], HOL Light [9] and Isabelle/HOL [13], support rank 1 polymorphism, where type quantification is allowed at the top level of formulae. By contrast, many automatic provers only work with monomorphic logics. One way to close this gap is to extend automatic provers to natively support polymorphism, as has been done in Vampire [1]. However, this entails a lot of work that must be redone for every prover. The alternative is to translate polymorphic problems to monomorphic problems.

To achieve this, one approach [2] is to encode a complete polymorphic type system, but this increases the size of the input problem substantially and slows down provers [2]. Another approach to encode polymorphism is based on iterative monomorphisation, as described by Böhme [5, Section 2.2.1]. Iterative monomorphisation heuristically instantiates the formulae's type variables with concrete types. However, any translation relying on a finite number of instantiations is inevitably incomplete. By a typed version of the compactness theorem, for any first order polymorphic formula $\varphi$, there exists an equisatisfiable finite set of monomorphic instances of $\varphi$, but it cannot be computed in general [4, Theorem 1].

Böhme's approach is implemented as part of Isabelle/HOL's SMT (satisfiability modulo theories) integration [5, Chapter 2]. This implementation is also used by Sledgehammer [6, 14] to interface with superposition based automatic theorem provers. However, it is documented only superficially [5, Section 2.2.1]. An iterative monomorphisation approach is also described in the context of SMT-LIB [7]. Moreover, a similar algorithm appears to be implemented in the MESON tactic [8] of HOL Light, but it is undocumented.
In this paper, we present an algorithm based on our understanding of Böhme’s description and implementation (Sect. 3). We also provide a more detailed description to help future implementers. In addition, we present some optimisations to curb the combinatorial explosions (Sect. 4).

The algorithm works as follows. The input problem is a set of formulae. All the problem’s symbols are collected, and the polymorphic symbol instances are matched against the monomorphic ones. This yields new symbol instances, both polymorphic and monomorphic. The process is then iterated, making use of the newly generated instances. Consider the unary type constructor list. If a formula contains `list(α)`, where α is a type variable, the types `list(int)`, `list(list(int))`, etc., can be generated. However, because new types emerge through matching, `list(list(int))` can be obtained only once the `list(int)` instance has been generated.

To keep the number of generated formulae finite, we limit the number of iterations. After the iterations are completed, the new monomorphic symbol instances are used to instantiate the polymorphic symbols in the problem’s formulae, generating new monomorphic formulae. Finally, because monomorphic provers support only nullary type constructors, types must be ‘mangled’; for example, the compound type `list(int)` might be mangled to `list_int`.

We implemented iterative monomorphisation in Zipperposition [18], a higher order prover written in OCaml. Although Zipperposition is polymorphic, it uses the monomorphic prover E [15] as a backend. Thanks to our work, E can now be used with polymorphic problems. Moreover, our implementation can be used as a preprocessor for other stand-alone provers. Our source code is available online. Our evaluation on the TPTP [17] tries to answer three questions (Sect. 6):

1. Is the new Zipperposition with the E backend more successful on polymorphic problems than Zipperposition without backend?

2. How competitive are monomorphic provers on monomorphised problems?

3. Is iterative monomorphisation more effective than the native polymorphism implemented in polymorphic provers?

## 2 Preliminaries

Our algorithm works independently of the structure of the problem’s formulae. It relies exclusively on the formulae’s monomorphic and polymorphic symbol instances. Type variables are assumed to be implicitly universally quantified at a formula’s top level. The precise form of formulae is left unspecified. Due to this generality, iterative monomorphisation can be used with any standard variant of rank 1 polymorphic logic. In particular, it can work with the polymorphic first and higher order logics embodied by TPTP’s TF1 and TH1 syntaxes [3,11].

Our abstract framework relies on the following basic definitions.

**Definition 1.** A (*polymorphic*) type $\tau$ is a type variable (e.g. $\alpha$) or the application of an $n$-ary type constructor to $n$ types (e.g. `list(α)`, `map(int, string)`). If $n = 0$, we omit the parentheses (e.g. `int`). A type is *monomorphic* if it contains no type variables.
**Definition 2.** A (function or predicate) symbol $f$ has a *type arity* that specifies the number of type arguments it takes. A *symbol instance* is a symbol applied to type arguments listed between angle brackets: $f\langle\tau_1, \dots, \tau_n\rangle$, where each $\tau_i$ is a type. If $n = 0$, we omit the angle brackets (e.g. $f$).

**Definition 3.** A (*type*) *substitution* is a partial function mapping a finite number of type variables to corresponding types. Substitutions are written as $\sigma = \{\alpha_1 \mapsto \tau_1, \dots, \alpha_n \mapsto \tau_n\}$. They are assumed to be lifted to formulae; thus, $\sigma(\varphi)$ yields the variant of $\varphi$ in which each $\alpha_i$ is replaced by $\tau_i$. Given two substitutions $\tau, v$, the successive application of $\tau$ and $v$ is denoted by $v \circ \tau$.

**Definition 4.** Two substitutions $\{\alpha_1 \mapsto \tau_1, \dots, \alpha_m \mapsto \tau_m\}$ and $\{\beta_1 \mapsto v_1, \dots, \beta_n \mapsto v_n\}$ are said to be *compatible* if $\alpha_i = \beta_j$ implies $\tau_i = v_j$ for all $i, j$.

**Definition 5.** Given two types $\tau, v$, *matching* $v$ against $\tau$ either fails or yields a substitution $\sigma$ such that $\sigma(v) = \tau$.

### 3 High Level Algorithm

The iterative monomorphisation algorithm takes a polymorphic problem as input and returns a monomorphic problem. It applies a bounded number of iterations, each taking a polymorphic problem as argument and returning a problem with new partially instantiated formulae. Once the iterations are completed, a final step discards all non-monomorphic formulae.

The initial phase of each iteration computes two maps, $M$ and $N$, from the input problem $\Phi$.

- Given a symbol $f$ occurring in $\Phi$, the set $M(f)$ consists of all monomorphic type argument tuples to which $f$ is applied in $\Phi$. For example, if $\text{foldl}\langle\text{nat}, \text{int}\rangle$ occurs in $\Phi$, then $(\text{nat}, \text{int}) \in M(\text{foldl})$.

- Given a formula $\varphi \in \Phi$ and a symbol $f$ occurring in $\varphi$, the set $N(\varphi)(f)$ consists of all type argument tuples to which $f$ is applied in $\varphi$ and which contain a type variable. For example, if $\text{foldl}\langle\text{nat}, \text{list}(\alpha)\rangle$ occurs in $\varphi$, then $(\text{nat}, \text{list}(\alpha)) \in N(\varphi)(\text{foldl})$.

$N$ is parametrised with $\varphi$ because type variables are implicitly quantified at the formula level. The formula indicates the scope of type variables. This is not necessary for $M$ since all the types it contains are monomorphic. To avoid copying the monomorphic types for each formula, $M$ and $N$ are kept separate.

Once the maps $M$ and $N$ are initialised, each iteration performs the following steps to create new instances of formulae:

1. Create an empty set of formulae $\Phi'$.

2. For each formula $\varphi \in \Phi$ and for each symbol $f$ occurring in $\varphi$:

2.1. For each $(\tau_1, \dots, \tau_n) \in M(f)$ and $(v_1, \dots, v_n) \in N(\varphi)(f)$ and for each $i$, match $v_i$ against $\tau_i$, yielding the substitution $\sigma_i$ in case of success.

2.2. If all $n$ matchings are successful and the substitutions $\sigma_i$ are pairwise compatible, add the formula $(\sigma_1 \circ \dots \circ \sigma_n)(\varphi)$ to $\Phi'$.

3. Return $\Phi \cup \Phi'$.
The algorithm is trivially sound because the newly generated formulae are instances of the initial problem's formulae. However, it is not complete.

**Example 6.** Consider the following problem:

$$ \langle 1 \rangle \quad \mathbf{p}\langle \mathbf{int} \rangle(0) $$

$$ \langle 2 \rangle \quad \forall a : \alpha, as : \mathbf{list}(\alpha). \mathbf{p}\langle\alpha\rangle(a) \to \mathbf{p}\langle\mathbf{list}(\alpha)\rangle(as) $$

The first iteration matches $\alpha$ against $\mathbf{int}$ for $\mathbf{p}$, generating the formula

$$ \langle 3 \rangle \quad \forall a : \mathbf{int}, as : \mathbf{list}(\mathbf{int}). \mathbf{p}\langle\mathbf{int}\rangle(a) \to \mathbf{p}\langle\mathbf{list}(\mathbf{int})\rangle(as) $$

The second iteration matches $\alpha$ against $\mathbf{list}(\mathbf{int})$, leading to the formula

$$ \langle 4 \rangle \quad \forall a : \mathbf{list}(\mathbf{int}), as : \mathbf{list}(\mathbf{list}(\mathbf{int})). \mathbf{p}\langle\mathbf{list}(\mathbf{int})\rangle(a) \to \mathbf{p}\langle\mathbf{list}(\mathbf{list}(\mathbf{list}(\mathbf{int})))\rangle(as) $$

Similarly the third iteration adds

$$ \langle 5 \rangle \quad \begin{gathered} \forall a:\mathbf{list}(\mathbf{list}(\mathbf{int})), as:\mathbf{list}(\mathbf{list}(\mathbf{list}(\mathbf{int}))). \\ \mathbf{p}\langle\mathbf{list}(\mathbf{list}(\mathbf{list}(\mathbf{int})))\rangle(a) \to \mathbf{p}\langle\mathbf{list}(\mathbf{list}(\mathbf{list}(\mathbf{list}(\mathbf{int}))))\rangle(as) \end{gathered} $$

This example illustrates how an infinite number of new formulae can be generated from a simple initial problem. Any reasonable implementation must limit the number of new type arguments, substitutions and formulae.

# 4 Low Level Algorithm

The algorithm presented above is too naïve in practice. In this section, we present a lower level algorithm with the following features. First, numeric bounds are introduced to stop combinatorially explosive enumerations. Second, type argument tuples are separated into an old set and a new set to avoid re-computing some of the same matchings in successive iterations. Third, substitutions are directly applied to the type arguments instead of the formulae. This avoids having to re-extract the type arguments from the formulae at each iteration. New formulae are generated only once all iterations are completed, in a separate, final step.

The data structures used in the algorithm are based on the ones used in the high level description. Instead of a map $M$ from symbols to monomorphic type argument tuples, we now have $M_{old}$ and $M_{new}$, which play the same role whilst also distinguishing between those type argument tuples that have already been matched against and those that have not. Similarly, $N_{old}$ and $N_{new}$ replace the map $N$ from formulae to symbols to non-monomorphic type argument tuples. Finally, we maintain a map $S$ from formulae to the substitutions generated by the matchings. It is used to generate new formulae in the final phase.

All sets referenced in the algorithm are finite. Moreover, the algorithm relies on primitives whose implementation depends on the specifics of the grammar and logic used. Functions computing the following are assumed to be available:

- *initialisation*($\Phi$), where $\Phi$ is a set of (polymorphic) formulae, extracts the initial type argument maps $M$ and $N$ from $\Phi$.
**Function** `iterative_monomorphisation(Φ)`
**Data:** set Φ of polymorphic formulae
**Result:** set of monomorphic formulae
(M<sub>old</sub>, N<sub>old</sub>) ← (∅, ∅)
(M<sub>new</sub>, N<sub>new</sub>) ← `initialisation(Φ)`
S ← ∅
**for** i = 1 **to** num_loops **do**
(M<sub>next</sub>, N<sub>next</sub>) ← (∅, ∅)
**foreach** ϕ ∈ Φ **do**
(M<sub>Δ</sub>, N<sub>Δ</sub>, S<sub>Δ</sub>) ←
formula_monomStep(ϕ, M<sub>old</sub>, M<sub>new</sub>, N<sub>old</sub>(ϕ), N<sub>new</sub>(ϕ))
S(ϕ) ← S&#773;(ϕ) ∪ S&#773;<sub>Δ</sub>
M<sub>next</sub> ← M<sub>next</sub> ∪ M<sub>Δ</sub>
N<sub>next</sub>(ϕ) ← N<sub>next</sub>(ϕ) ∪ N<sub>Δ</sub>
(M<sub>old</sub>, M<sub>new</sub>) ← (M<sub>old</sub> ∪ M<sub>new</sub>, M<sub>next</sub>)
(N<sub>old</sub>, N<sub>new</sub>) ← (N<sub>old</sub> ∪ N<sub>new</sub>, N<sub>next</sub>)
**return** mangle(generate_monomFormulae(Φ, S))

<caption>**Fig. 1.** Algorithm for iterative monomorphisation.</caption>

- `type_vars(τ₁, ..., τₙ)`, where τ₁, ..., τₙ are types, gathers all the type variables from each type τ₁, ..., τₙ into a set. This function is overloaded to accept a formula ϕ as input, in which case it returns the set of all type variables which occur in the formula.

- `match(v, τ)`, where v and τ are types, matches v against τ and either fails or returns `Some(σ)`, where σ results from the matching. The algorithm matches only non-monomorphic types against monomorphic types.

- `domain(σ)` returns the set of type variables α such that $\sigma(\alpha) \neq \alpha$.

- `compatible(σ₁, σ₂)` tests the compatibility between σ₁ and σ₂.

- `mangle(Φ)`, where Φ is a set of monomorphic formulae, returns the same set of formulae where all types have been mangled.

The iterative monomorphisation algorithm is given in Fig. 1. It has three phases. The first phase applies a *monomorphisation step* to each formula in Φ until the user-set limit, `num_loops`, is reached. This limit is the only bound necessary for the algorithm to terminate. We use the colour blue to identify bounds and code related to bounds. At the end of each of these iterations, the old and new type argument maps are updated with newly generated types. No new formulae are generated at this stage, only new type arguments and substitutions. Once these iterations are completed, the first phase is complete and the substitutions used to create new type argument tuples are passed to `generate_monomFormulae` for the second phase. This is when the new formulae are generated. The third phase mangles the composite types of the newly monomorphised formulae. This allows targeting a simply typed logic with no support for *n*-ary type constructors.
**Function** `formula_monochrome`($\varphi, M_{old}, M_{new}, N_{old}(\varphi), N_{new}(\varphi)$)

**Data:** polymorphic formula $\varphi$

old and new monomorphic type argument maps $M_{old}, M_{new}$

old and new non-monomorphic type argument maps $N_{old}(\varphi), N_{new}(\varphi)$

**Result:** monomorphic type argument map

non-monomorphic type argument map

set of substitutions

`max_monochrome_args` ←

$min(max(\text{mono\_floor}, |M_{old} \cup M_{new}| \cdot \text{mono\_mult}), \text{mono\_cap})$

`max_nonmon_args` ←

$min(max(\text{nonm\_floor}, |N_{old}(\varphi) \cup N_{new}(\varphi)| \cdot \text{nonm\_mult}), \text{nonm\_cap})$

$S \leftarrow \emptyset$

$S' \leftarrow \text{matches}(M_{new}, N_{new}(\varphi)) \cup \text{matches}(M_{new}, N_{old}(\varphi)) \cup$

$\text{matches}(M_{old}, N_{new}(\varphi))$

$(M_{next}, N_{next}(\varphi)) \leftarrow (\emptyset, \emptyset)$

`foreach $\sigma \in S'$ do`

`foreach ($f \mapsto (v_1, \dots, v_n) \in N_{old}(\varphi) \cup N_{new}(\varphi)$) do`

`if type_vars(v_1, \dots, v_n) \subseteq \text{subst\_dom}(\sigma) then`

`if $|M_{next}| < \max_{\text{mono\_args}}$ then`

$M_{next}(f) \leftarrow \bar{M}_{next}(f) \cup \{(\sigma(v_1), \dots, \sigma(v_n))\}$

$S \leftarrow S \cup \{\sigma\}$

`else if $|N_{next}(\varphi)| \ge \max_{\text{nonm\_args}}$ then`

$M_{next} \leftarrow M_{next} \setminus (M_{old} \cup M_{new})$

$N_{next}(\varphi) \leftarrow N_{next}(\varphi) \setminus (N_{old}(\varphi) \cup N_{new}(\varphi))$

`return $(M_{next}, N_{next}(\varphi), S)$`

`else`

`if $|N_{next}(\varphi)| < \max_{\text{nonm\_args}}$ then`

$N_{next}(\varphi)(f) \leftarrow \bar{N}_{next}(\varphi)(f) \cup \{(\sigma(v_1), \dots, \sigma(v_n))\}$

$S \leftarrow S \cup \{\sigma\}$

`return $(M_{next} \setminus (M_{old} \cup M_{new}), N_{next}(\varphi) \setminus (N_{old}(\varphi) \cup N_{new}(\varphi)), S)$`

<caption>**Fig. 2.** Algorithm for formula monomorphisation step</caption>

The formula monomorphisation algorithm is given in Fig. 2. It forms the core of the process. Essentially, it computes new type argument tuples for a single formula. Type argument tuples are matched against each other to obtain a set of substitutions which is iterated over in the outermost loop. The separation of type argument tuples into old and new maps is used to ensure that only combinations involving at least one new map are considered. This avoids re-computing some matchings processed in previous iterations. New tuples are obtained by applying each substitution to each non-monomorphic type argument tuple such that at least one tuple component is instantiated by the substitution.

The total number of type argument tuples can increase cubically in the number of type argument tuples at each iteration and can therefore grow doubly exponentially in the number of iterations. We give a sketch of how such growth can occur for a single formula. If we assume that after $k$ iterations, there are $N_k$
type argument tuples in total divided evenly between monomorphic and non-
monomorphic type argument tuples, then there can be up to $(\frac{N_k}{2})^2$ successful
matches, yielding as many substitutions. Each substitution is then applied to
each non-monomorphic type argument for a total of $(\frac{N_k}{2})^3$ possible new type
argument tuples. If half of these new type argument tuples are monomorphic
and the other half are non-monomorphic, then the next iteration will begin with
$N_{k+1} = N_k^3 \cdot 2^{-3}$ evenly split type argument tuples. Therefore, the total number
of type argument tuples on the $k$th iteration can reach $N_k = N_0^{3k} \cdot 2^{-\frac{3k^2+3}{2}}$.

Depending on the shape and size of the input problem and the number
of iterations performed, the doubly exponential growth may be problematic.
Introducing bounds addresses this potential issue. The limit on the number of
newly generated monomorphic type argument tuples is min(max(mono_mult ·
m, monoFloor), mono_cap), where *m* is the total number of monomorphic type
argument tuples. The components of this limit are

1. `mono_cap`, a limit on the total number of new type argument tuples;

2. `mono_mult`, which is used to allow the total number of (monomorphic) type argument tuples to grow by a certain proportion of the current number *m* of monomorphic type argument tuples;

3. `monoFloor`, which balances out `mono_mult`, preventing `mono_mult` from inhibiting new type argument tuple generation if *m* is too low.

Similar bounds are used for the non-monomorphic type argument tuples:
The limit on the number of new non-monomorphic type argument tuples is
min(max(nonmult·n, nonmFloor), nonmCap), where *n* is the number of non-
monomorphic type argument tuples associated with the current formula. An
important difference with the monomorphic case is that *n* depends on the current
formula being processed whilst *m* does not. Both in the monomorphic and in the
non-monomorphic case, the maximum number of newly generated type argument
tuples is fixed per formula and per iteration.

The *matches* function, which computes the substitutions used for generat-
ing new type arguments, is given in Fig. 3. Each symbol instance from *N*(*φ*) is
matched against all corresponding symbol instances from *M*. For two such sym-
bol instances, the types from the non-monomorphic type argument tuple are
matched component-wise against the types from the monomorphic type argu-
ment tuple. The resulting substitutions are composed if they are compatible.
In the algorithm, compatibility is checked by making sure the **foreach** loop has
successfully iterated over all elements of the type argument tuple. If any substitu-
tions are incompatible, the matchings are discarded. Since the composition of two
compatible substitutions is commutative, the order of composition is irrelevant.
The total number of substitutions generated is limited by **substitution_cap**.

The various bounds presented here overlap to some extent. For instance, hav-
ing at most `substitution_cap` substitutions generated by *matches* may be suffi-
cient to curb the number of new type argument tuples, making the `mono_cap`,
`mono_mult`, `monoFloor` triplet superfluous. Nonetheless every bound has uses.
**Function** `matches(M, N(φ))`

**Data:** monomorphic type argument map *M*
non-monomorphic type argument map *N(φ)*

**Result:** set of substitutions

$S \leftarrow \emptyset$

**foreach** $f \mapsto (v_1, \dots, v_n) \in N(\varphi)$ **do**

**foreach** $(\tau_1, \dots, \tau_n) \in M(f)$ **do**

if $|S| > \text{substitution\_cap}$ then
return *S*

if for all $0 \le i \le n$, match($v_i$, $\tau_i$) = *Some*($\sigma_i$) **then**

if $\sigma_1, \dots, \sigma_n$ are compatible **then**

$\sigma \leftarrow \sigma_1 \circ \dots \circ \sigma_n$

$S \leftarrow S \cup \{\sigma\}$

return *S*

<caption>**Fig. 3.** Algorithm for match generation.</caption>

**Function** `generate_mono_formulae(Φ, S)`

**Data:** set $\Phi$ of polymorphic formulae
substitution map *S*

**Result:** set of monomorphic formulae

$\Psi \leftarrow \emptyset$

**foreach** $\varphi \in \Phi$ **s.t.** $\varphi$ is non-monomorphic **do**

**foreach** $\sigma \in \text{mono\_substs}(S(\varphi), \text{type\_vars}(\varphi), \emptyset, \{\})$ **do**

if $|\Psi| < \text{max\_new\_formulae}$ then
$\Psi \leftarrow \Psi \cup \{\sigma(\varphi)\}$

else
return $\Psi$

return $\Psi$

<caption>**Fig. 4.** Algorithm for monomorphic formula generation.</caption>

For example, problems that lead to few successful matches but many type argu-
ment tuples may benefit from a limit on the number of new type argument tuples
whilst problems for which substitution generation is more combinatorially explo-
sive may benefit from a limit on the number of generated substitutions.

Once all monomorphisation iterations have been completed, we are left with a
set of the substitutions that have been used to generate new type arguments. The
last phase uses this set to instantiate the type variables in the input problem's
non-monomorphic formulae. In the presence of bounds, the order in which the
elements of *S* are traversed affects the formulae resulting from the last phase.

The `generate_mono_formulae` function is given in Fig. 4. It generates monomorphising substitutions and applies them to the polymorphic formulae of the input problem that they instantiate. A substitution $\sigma$ is monomorphising for a formula $\varphi$ if $\sigma(\varphi)$ is monomorphic. Since the substitutions are monomorphising relative to the formula they are applied to, the resulting formulae will
<figure><img src="image_50.png" /><figcaption>**Fig. 5.** Algorithm for monomorphising substitution generation.</figcaption></figure>

be monomorphic. The `max_new_formulae` bound is used to control the total number of new formulae. It overlaps with `max_substs` but can be useful to set an absolute limit on the size of the final problem.

To monomorphise a polymorphic formula, we first compute its monomorphis-
ing substitutions using the `mono_substs` function given in Fig. 5. Such substitu-
tions are computed using a recursive function. Given a set $V$ of type variables
and a set $S(\varphi)$ of substitutions, it selects a substitution $\sigma_\Delta$ from $S(\varphi)$ that
instantiates at least one of the type variables in $V$. It is important that $\sigma_\Delta$ be
compatible with $\sigma$ so that they can be composed and the function recursively
called to instantiate the remaining type variables.

The Zipperposition implementation of the `mono_substs` function uses a map
from type variables to substitutions instead of a set to filter the relevant substi-
tutions from `S` efficiently. The `max_substs` bound exists for two main reasons:

1. The iterative monomorphisation algorithm can generate up to `max_substs` new monomorphic formulae per initial polymorphic formula. Generating an excessive number of new formulae can overwhelm the prover. The final number of output formulae is limited to at most $|\Phi| \cdot \max_substs$.

2. The `mono_substs` function is the algorithm's most combinatorially explosive part. For a formula $\varphi$, if $S(\varphi)$ contains $n$ substitutions that each instantiate exactly one of $v$ type variables, up to $n^v$ monomorphising substitutions may be generated. Recall that the total number of type argument tuples used to generate $S(\varphi)$ can be doubly exponential in the number of loop iterations. The starting $n$ may therefore already be very large.
# 5 Detailed Example

To illustrate the low level version of the iterative algorithm, we consider the following (admittedly contrived) initial problem:

$$ \langle 1 \rangle \quad \mathbf{p}(\text{int, nat})(-1, 3) \wedge \mathbf{p}(\text{int, int})(-1, -2) $$

$$ \langle 2 \rangle \quad \forall x : \alpha, y : \text{list}(\alpha), z : \beta. \mathbf{p}(\text{list}(\alpha), \alpha)(y, x) \wedge \mathbf{p}(\alpha, \alpha)(x, x) \wedge \mathbf{p}(\alpha, \beta)(x, z) $$

$M_{\text{new}}$ is initialised with $\{\mathbf{p} \mapsto \{(\text{int, nat}), (\text{int, int})\}\}$ and $N_{\text{new}}$ with $\{\langle 2 \rangle \mapsto \{\mathbf{p} \mapsto \{(\text{list}(\alpha), \alpha), (\alpha, \alpha), (\alpha, \beta)\}\}\}$. Then we enter the main loop (assuming `num_loops` is at least 1). We iterate over each formula and call `formulaMonoStep` for each of them. Nothing happens for formula $\langle 1 \rangle$ because it contains no type variables. For formula $\langle 2 \rangle$, $M_{\text{new}}$ and $N_{\text{new}}(\langle 2 \rangle)$ are passed as arguments to `matches`.

The three non-monomorphic type argument tuples are matched against their monomorphic counterparts in $M_{\text{new}}$:

- $(\text{list}(\alpha), \alpha)$ fails in both cases because $\text{list}(\alpha)$ fails to match against `int`.

- $(\alpha, \alpha)$ fails to match against $(\text{int, nat})$ because the substitutions resulting from the match of the first and second element of the tuple are incompatible. The second match is successful and yields the substitution $\sigma_1 = \{\alpha \mapsto \text{int}\}$

- $(\alpha, \beta)$ succeeds in both cases and generates the substitutions $\sigma_2 = \{\alpha \mapsto \text{int}, \beta \mapsto \text{int}\}$ and $\sigma_3 = \{\alpha \mapsto \text{int}, \beta \mapsto \text{nat}\}$.

Then `matches` returns, and the substitutions are used to generate new type argument tuples. Each substitution is applied to the type arguments of the function symbols of formula $\langle 2 \rangle$ because they are the only function symbols with non-monomorphic type arguments. The table below summarises the situation:

<table><thead><tr><th></th><th>σ<sub>1</sub></th><th>σ<sub>2</sub></th><th>σ<sub>3</sub></th></tr></thead><tbody><tr><td>(list(α), α)</td><td>(list(int), int)</td><td>(list(int), int)</td><td>(list(int), int)</td></tr><tr><td>(α, α)</td><td>(int, int)</td><td>(int, int)</td><td>(int, int)</td></tr><tr><td>(α, β)</td><td>(int, β)</td><td>(int, int)</td><td>(int, nat)</td></tr></tbody></table>

With a simple two-formula initial problem, there are already up to nine new type arguments tuples generated at this step in the first iteration alone, although only four are unique. Once the new type argument tuples are added to their respective maps, a new iteration is begun. We only consider one iteration and continue to the next phase of the algorithm.

The next function to be called is `generate formulas`. It iterates over all non-monomorphic formulae of the initial problem; in our case, this will only be $\langle 2 \rangle$. The set of type variable tuples of $\langle 2 \rangle$ is passed to `mono_substs` along with the set of all previously generated substitutions.

First, we instantiate $\alpha$, the first type variable of $\langle 2 \rangle$. If $\sigma_1$ is selected to instantiate $\alpha$, both $\sigma_2$ and $\sigma_3$ will in turn be selected to instantiate $\beta$. This will generate two monomorphising substitutions, $\sigma_1 \circ \sigma_2 = \sigma_2$ and $\sigma_1 \circ \sigma_3 = \sigma_3$, which are added to the set of monomorphising substitutions $S_{\text{res}}$. Now $\sigma_2$ is
selected. It simultaneously instantiates $\alpha$ and $\beta$. Here, $\sigma_2$ is already in $S_{\text{res}}$ and is therefore ignored, and $\sigma_3$ is treated similarly. No more than **substitution_cap** monomorphising substitutions can be generated in this way.

Now, the monomorphising substitutions have been generated. We only need to apply them to the formula they monomorphise. This is repeated for all non-monomorphic formulae or until **max_new formulae** is reached. The order of formulae will impact the output problem in the latter case. For some larger input problems, *mono_substs* could be sufficiently explosive to only allow a handful of different formulae to be monomorphised. The ability to set **substitution_cap** independently can help avoid this issue.

Finally, if the target language supports only nullary type constructors, the types of all monomorphic formulae, both new and old, are mangled. Assuming that mangling is not necessary, the algorithm outputs

$$ \langle 1 \rangle \ p(\text{int}, \text{nat})(-1, 3) \wedge p(\text{int}, \text{int})(-1, -2) $$

$$ \langle 3 \rangle \ \forall x : \text{int}, y : \text{list}(\text{int}), z : \text{int}. \ p(\text{list}(\text{int}), \text{int})(y, x) \wedge p(\text{int}, \text{int})(x, x) \wedge \\ \qquad \qquad \qquad p(\text{int}, \text{int})(x, z) $$

$$ \langle 4 \rangle \ \forall x : \text{int}, y : \text{list}(\text{int}), z : \text{nat}. \ p(\text{list}(\text{int}), \text{int})(y, x) \wedge p(\text{int}, \text{int})(x, x) \wedge \\ \qquad \qquad \qquad p(\text{int}, \text{nat})(x, z) $$

In this example, two new monomorphic formulae are generated.

# 6 Evaluation

The monomorphisation algorithm is parametrised by many bounds. The first part of the evaluation process seeks appropriate values for these bounds. The second part compares the performance of Zipperposition without E and with the new monomorphising E backend on polymorphic problems. The third part compares the performance of different provers on polymorphic problems and their monomorphised counterparts.

The benchmarks are taken from version 8.2.0 of the TPTP library [17]. The library contains 1765 problems in TF1 and TH1, corresponding respectively to first and higher order logic with rank 1 polymorphism. Because Zipperposition does not support reasoning with real numbers, we removed all problems that include them. In total, our benchmark suite contains 1534 polymorphic problems. We chose as a measure of success for a given prover (or prover configuration) the number of problems that could be solved by the prover in at most 30 s per problem with a single thread. Our raw evaluation data is available online.<fnref n="1" />

## Parameter Optimisation

Each bound of the monomorphisation process represents a tradeoff: a higher bound allows for a more exhaustive instantiation of type variables but takes more time. Since we cannot test all possible combinations of values for all bounds to find the best compromise between completeness and speed, we group closely

<footnote n="1">¹ https://zenodo.org/records/14881532.</footnote>
related bounds together and test combinations of values for the bounds in these groups. Once we find the best performing set of values for a group, we assign these values to the corresponding bounds as we begin the search for the next group. If several groups result in the same number of proved problems, we select the most constraining values. Winning entries are shown in bold in Tables 1 to 6.

To guard against overfitting took place, we carried out the part of the evaluation related to parameter optimisation and all preliminary evaluations on 500 randomly chosen problems out of the 1534 selected problems. We carried out the rest of the evaluations on the remaining 1034 problems.

Before finding values to assign to the bounds of the monomorphisation algorithm, we must choose which base options to run Zipperposition with. Because the space of possible base configurations is too large to evaluate exhaustively, we evaluated, in a preliminary experiment, all pre-existing portfolio configurations that called E against our benchmark suite of 500 problems. Since E could not treat these non-monomorphic problems, it was disabled. The preliminary evaluation found that the 40_b.comb configuration performed best by proving 131 problems. This configuration became the base configuration, which we used as a basis to evaluate the monomorphisation options.

We conducted additional informal evaluations on the 500 problems to find appropriate default values and test ranges for the monomorphisation bounds. We started the option evaluation process with the base configuration and the following default values for monomorphisation bounds and parameters for E:

- `nonm_cap`: $\infty$

- `nonm_mult`: 1

- `nonmFloor`: 50

- substitution order: separation

- `substitution_cap`: $\infty$

- `max_substs`: 10

- `max_new formulae`: 2000

- new formulae limit multiplier: 0

- monomorphisation timeout: 20

- `num_loops`: 4

- E timeout: 30

- E call point: 0

The initial values for the `mono_cap`, `mono_mult` and `monoFloor` options are irrelevant because the options' values are set when computing Table 1.

Table 1 groups bounds that control the maximum number of newly generated monomorphic type arguments per formula and per iteration. The limit on newly generated type arguments is determined by three components that form a natural group of bounds.

The table shows that generating no new monomorphic type arguments seems to be the best approach. This result may seem counterintuitive, but it is possible to monomorphise formulae without generating monomorphic type arguments. This is because non-monomorphic type argument generation can produce substitutions that instantiate one or more type variables, and it is these substitutions that are used to monomorphise formulae.

Table 2 is similar to Table 1 except that it evaluates the bounds limiting the number of new non-monomorphic type arguments. The bound values are lower because we found non-monomorphic type arguments to be combinatorially explosive in preliminary evaluations. The table confirms that non-monomorphic
<table><caption>**Table 1.** Evaluation of bounds for monomorphic type argument generation</caption><thead><tr><th rowspan="3">mult</th><th colspan="10">cap</th></tr><tr><th colspan="5">500</th><th colspan="5">1000</th><th colspan="5">∞</th></tr><tr><th colspan="10">floor</th></tr><tr><th>0</th><th>50</th><th>100</th><th>200</th><th>0</th><th>50</th><th>100</th><th>200</th><th>0</th><th>50</th><th>100</th><th>200</th></tr></thead><tbody><tr><td>0</td><td><b>178</b></td><td>161</td><td>161</td><td>156</td><td>178</td><td>160</td><td>160</td><td>156</td><td>178</td><td>161</td><td>160</td><td>156</td></tr><tr><td>1</td><td>155</td><td>155</td><td>155</td><td>158</td><td>153</td><td>154</td><td>154</td><td>156</td><td>154</td><td>154</td><td>155</td><td>155</td></tr><tr><td>2</td><td>154</td><td>154</td><td>153</td><td>154</td><td>153</td><td>153</td><td>154</td><td>152</td><td>154</td><td>153</td><td>154</td><td>154</td></tr><tr><td>∞</td><td>153</td><td>154</td><td>153</td><td>155</td><td>155</td><td>153</td><td>154</td><td>156</td><td>159</td><td>160</td><td>161</td><td>161</td></tr></tbody></table>

<table><caption>**Table 2.** Evaluation of bounds for non-monomorphic type argument generation</caption><thead><tr><th rowspan="3">mult</th><th colspan="10">cap</th></tr><tr><th colspan="5">500</th><th colspan="5">1000</th><th colspan="5">∞</th></tr><tr><th colspan="10">floor</th></tr><tr><th>0</th><th>10</th><th>50</th><th>100</th><th>0</th><th>10</th><th>50</th><th>100</th><th>0</th><th>10</th><th>50</th><th>100</th></tr></thead><tbody><tr><td>0</td><td>125</td><td><b>184</b></td><td>182</td><td>177</td><td>125</td><td>184</td><td>182</td><td>177</td><td>125</td><td>184</td><td>182</td><td>177</td></tr><tr><td>0.5</td><td>176</td><td>184</td><td>182</td><td>177</td><td>176</td><td>184</td><td>182</td><td>177</td><td>176</td><td>184</td><td>182</td><td>177</td></tr><tr><td>1</td><td>182</td><td>181</td><td>178</td><td>177</td><td>182</td><td>181</td><td>178</td><td>177</td><td>182</td><td>181</td><td>178</td><td>177</td></tr><tr><td>∞</td><td>173</td><td>174</td><td>174</td><td>174</td><td>174</td><td>174</td><td>173</td><td>173</td><td>125</td><td>125</td><td>125</td><td>125</td></tr></tbody></table>

type argument generation drives the creation of useful non-monomorphic formulae. This is indicated by the very low number of problems solved when no new non-monomorphic type arguments are allowed. Performance of the monomorphisation algorithm seems to plateau for some ranges of values and drops off beyond.

The substitution generation phase occurs once all type arguments have been generated. The bound limiting the number of monomorphising substitutions per formula is directly related to the order which dictates how such monomorphising substitutions are generated. The heuristic greatly affects monomorphising substitution generation. The ‘age’ order of substitution orders substitutions generated in earlier iterations first. The ‘random’ order randomly shuffles substitutions. Finally, the ‘separation’ order separates the substitutions into groups of substitutions generated in the same iteration and generates monomorphising substitutions from each of these groups independently. Table 3 shows that the values of bounds limiting the number of monomorphising substitutions seem to affect performance only when the ‘separation’ heuristic is used.

Table 4 groups the bounds related to the size of the output problem to be passed to the E prover. The absolute limit is the maximum number of formulae passed to E. The multiplier limits the total number of newly generated formulae based on the problem’s initial number of formulae. We find that the E prover tends to perform better when given a limited number of formulae.
<table><caption>**Table 3.** Evaluation of bounds for substitution generation</caption><thead><tr><th rowspan="2">mono subst</th><th colspan="3">substitution order</th></tr><tr><th>age</th><th>random</th><th>separation</th></tr></thead><tbody><tr><td>2</td><td>161</td><td>178</td><td>175</td></tr><tr><td>5</td><td>161</td><td>178</td><td>180</td></tr><tr><td>7</td><td>161</td><td>178</td><td>182</td></tr><tr><td>10</td><td>161</td><td>178</td><td><strong>184</strong></td></tr></tbody></table>

<table><caption>**Table 4.** Evaluation of bounds directly related to the size of the output problem</caption><thead><tr><th rowspan="2">formula cap</th><th colspan="4">formula multiplier</th></tr><tr><th>1</th><th>2</th><th>3</th><th>&infin;</th></tr></thead><tbody><tr><td>500</td><td><strong>184</strong></td><td>184</td><td>184</td><td>183</td></tr><tr><td>2000</td><td>184</td><td>184</td><td>184</td><td>184</td></tr><tr><td>&infin;</td><td>168</td><td>178</td><td>183</td><td>125</td></tr></tbody></table>

<table><caption>**Table 5.** Evaluation of parameters related to the depth of monomorphisation</caption><thead><tr><th rowspan="2">num. loops</th><th colspan="4">mono time</th></tr><tr><th>5</th><th>10</th><th>20</th><th>30</th></tr></thead><tbody><tr><td>1</td><td>183</td><td>184</td><td>183</td><td>183</td></tr><tr><td>2</td><td><strong>186</strong></td><td>186</td><td>186</td><td>185</td></tr><tr><td>3</td><td>186</td><td>186</td><td>186</td><td>185</td></tr><tr><td>4</td><td>186</td><td>186</td><td>186</td><td>185</td></tr><tr><td>5</td><td>185</td><td>185</td><td>185</td><td>184</td></tr></tbody></table>

For larger problems, the monomorphisation algorithm may time out despite the bounds. In these cases, neither Zipperposition nor E will have had a chance to try to solve the problem. To avoid this, a timer can interrupt the monomorphisation algorithm, after which Zipperposition resumes normal operation. Table 5 tests the amount of time that is allocated to monomorphisation against the number of iterations of the monomorphisation algorithm. Neither parameter seems to substantially affect the algorithm's performance.

Table 6 shows the impact of the options with which we call the E prover. The point at which Zipperposition interrupts its normal operation and begins the monomorphisation process is determined by the 'E call point' parameter. It is expressed as a fraction of the total time allotted to Zipperposition. The E timeout (in seconds) limits how long E is run before being interrupted, at which point Zipperposition resumes normal operation. The longer Zipperposition runs before E is invoked, the more formulae are generated, and the more combina-
<table><caption>**Table 6.** Evaluation of parameters related to the E prover</caption><thead><tr><th rowspan="2">E timeout</th><th colspan="4">E call point</th></tr><tr><th>0</th><th>0.1</th><th>0.2</th><th>0.3</th></tr></thead><tbody><tr><td>2</td><td>180</td><td>143</td><td>132</td><td>124</td></tr><tr><td>5</td><td><b>185</b></td><td>142</td><td>134</td><td>125</td></tr><tr><td>10</td><td>184</td><td>143</td><td>132</td><td>125</td></tr><tr><td>20</td><td>184</td><td>137</td><td>133</td><td>125</td></tr><tr><td>30</td><td>182</td><td>133</td><td>134</td><td>125</td></tr></tbody></table>

<table><caption>**Table 7.** Evaluation of Zipperposition without E vs. with E</caption><thead><tr><th></th><th>without E</th><th>with E</th><th>union</th></tr></thead><tbody><tr><td>500 problem suite</td><td>160</td><td>198</td><td>207</td></tr><tr><td>1034 problem suite</td><td>337</td><td>410</td><td>434</td></tr></tbody></table>

torially explosive iterative monomorphisation is. This likely explains the poor performance for greater values of the E call point.

## E as a Zipperposition backend

We compare the performance of two instances of Zipperposition. By default, Zipperposition may call E as a backend when given a monomorphic problem [18]. The first instance is run in the portfolio mode `portfolio.sequential.py`, which attempts to prove the problem with various configurations tried in succession. Since all given problems are non-monomorphic, these configurations can never invoke E as a backend, this instance is therefore labeled ‘without E’. The second instance is a modification of the `portfolio.sequential.py` file where each configuration is modified analogously to `40_b.comb` with the options obtained in the previous evaluation phase. This instance can successfully call E as a backend because it is able to provide E with a monomorphised problem. Each of the two instances is evaluated on the set of the 500 previously used problems, and the set of the remaining 1034 problems is evaluated separately. The proportion of problems successfully solved on the 500 and 1034 problem suites are similar, suggesting that no overfitting took place during the option optimisation phase.

Table 7 shows that the use of E as a backend markedly improves the performance of Zipperposition. It is not a strict improvement, since some problems are solved without E and not with E.

## Monomorphisation as a Preprocessor

To evaluate the usefulness of iterative monomorphisation as an alternative to native polymorphism, two competitive higher order polymorphic provers were run on the 1034 problem suite. We chose Leo-III and Zipperposition. Unfortunately we needed to exclude Vampire because of parsing issues. The fix for these issues was unavailable for Vampire's higher order branch at the time of the evaluation.
<table><caption>**Table 8.** Evaluation of native polymorphism vs. monomorphisation</caption><thead><tr><th></th><th>Native</th><th>Mono</th><th>Union</th></tr></thead><tbody><tr><td>E</td><td>-</td><td>340</td><td>340</td></tr><tr><td>Leo-III with E</td><td>157</td><td>231</td><td>274</td></tr><tr><td>Zipperposition</td><td>339</td><td>351</td><td>404</td></tr></tbody></table>

Table 8 shows the results. The monomorphisation approach is evaluated in two steps. First, each problem is monomorphised using the options obtained from the first evaluation phase except for the monomorphisation timeout option, which is increased to 30 s. For 149 problems, monomorphisation times out. Second, each prover is run on the remaining monomorphised problems, and the results are tallied in the ‘Mono’ column. In addition to the polymorphic provers used in the ‘Native’ tests, the monomorphic prover E is run on the monomorphised problems to provide an additional point of comparison. Instead of running each prover for 30 s on the monomorphised problems, the monomorphisation time (rounded up to the nearest second) is subtracted to compare fairly against the ‘Native’ column, which does not have a similar preprocessing phase.

Despite the monomorphisation timeouts, monomorphisation is more effective than Leo-III’s and Zipperposition’s native polymorphism on the benchmarks.

# 7 Conclusion

We described a translation algorithm that iteratively instantiates polymorphic types to produce monomorphic problems. Our primary motivation was to improve the success rate of Zipperposition and its monomorphic E backend, and indeed our evaluation shows a clear improvement. We also saw that even with automatic provers that support polymorphism, iterative monomorphisation is a better alternative in practice.

We see the following avenues for future work. First, iterative monomorphisation blindly enumerates candidate instantiations, without exploiting any knowledge about the logical structure of the formulae in which symbols occur. For example, a lemma $p\langle\alpha\rangle$ cannot be used to prove the conjecture $\neg p\langle nat\rangle$ because of the incompatible polarities, but our algorithm instantiates $\alpha$ with nat regardless. Second, some automatic provers as well as tools such as Sledgehammer include relevance filters that heuristically select a subset of the available axioms; filters such as MePo [12] and SInE [10] are iterative and could be interleaved with monomorphisation. Third, although one would expect native implementations of polymorphism to outperform any preprocessor, currently this is not the case, suggesting that there is considerable room for improvement on the native front.

**Acknowledgements.** We thank Sascha Böhme for fruitful discussions. We thank Janis Limperg, Mark Summerfield, and the peer reviewers for suggesting textual improvements. This research is co-funded by the European Union (ERC, Nekoka, 101083038).
Views and opinions expressed are however those of the authors only and do not neces-
sarily reflect those of the European Union or the European Research Council. Neither
the European Union nor the granting authority can be held responsible for them.

References

1. Bhayat, A., Reger, G.: A polymorphic Vampire. In: Peltier, N., Sofronie-Stokkermans, V. (eds.) IJCAR 2020. LNCS (LNAI), vol. 12167, pp. 361–368. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-51054-1_21

2. Blanchette, J.C., Böhme, S., Popescu, A., Smallbone, N.: Encoding monomorphic and polymorphic types. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 493–507. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-36742-7_34

3. Blanchette, J.C., Paskevich, A.: TFF1: the TPTP typed first-order form with rank-1 polymorphism. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 414–420. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-38574-2_29

4. Bobot, F., Paskevich, A.: Expressing polymorphic types in a many-sorted language. In: Tinelli, C., Sofronie-Stokkermans, V. (eds.) FroCoS 2011. LNCS (LNAI), vol. 6989, pp. 87–102. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-24364-6_7

5. Böhme, S.: Proving Theorems of Higher-Order Logic with SMT Solvers. PhD thesis, Technische Universität München (2012)

6. Böhme, S., Nipkow, T.: Sledgehammer: Judgement Day. In: Giesl, J., Hähnle, R. (eds.) IJCAR 2010. LNCS (LNAI), vol. 6173, pp. 107–121. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-14203-1_9

7. Bonichon, R., Déharbe, D., Tavares, C.: Extending SMT-LIB v2 with λ-terms and polymorphism. In: Rümmer, P., Wintersteiger, C.M. (eds.) SMT 2014. CEUR Workshop Proceedings, vol. 1163, pp. 53–62. CEUR-WS.org (2014)

8. Harrison, J.: Optimizing proof search in model elimination. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS, vol. 1104, pp. 313–327. Springer, Heidelberg (1996). https://doi.org/10.1007/3-540-61511-3_97

9. Harrison, J.: HOL Light: an overview. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 60–66. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-03359-9_4

10. Hoder, K., Voronkov, A.: Sine qua non for large theory reasoning. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS (LNAI), vol. 6803, pp. 299–314. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22438-6_23

11. Kaliszyk, C., Sutcliffe, G., Rabe, F.: TH1: The TPTP typed higher-order form with rank-1 polymorphism. In: Fontaine, P., Schulz, S., Urban, J. (eds.) PAAR 2016. CEUR Workshop Proceedings, vol. 1635, pp. 41–55. CEUR-WS.org (2016)

12. Meng, J., Paulson, L.C.: Lightweight relevance filtering for machine-generated resolution problems. J. Appl. Log. **7**(1), 41–57 (2009)

13. Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45949-9

14. Paulson, L.C., Blanchette, J.C.: Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers. In: Sutcliffe, G., Schulz, S., Ternovska, E. (eds.) IWIL-2010. EPiC, vol. 2, pp. 1–11. EasyChair (2012)
15. Schulz, S.: E – a brainiac theorem prover. *AI Commun.* **15**(2–3), 111–126 (2002)

16. Slind, K., Norrish, M.: A brief overview of HOL4. In: Mohamed, O.A., Muñoz, C., Tahar, S. (eds.) *TPHOLs 2008. LNCS, vol. 5170, pp. 28–32*. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-71067-7_6

17. Sutcliffe, G.: The TPTP problem library and associated infrastructure – from CNF to TH0, TPTP v8.2.0. *J. Autom. Reason.* **59**(4), 483–502 (2017)

18. Vukmirović, P., Bentkamp, A., Blanchette, J., Cruanes, S., Nummelin, V., Tourret, S.: Making higher-order superposition work. In: Platzer, A., Sutcliffe, G. (eds.) CADE 2021. LNCS (LNAI), vol. 12699, pp. 415–432. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-79876-5_24

**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.
# The Dependently Typed Higher-Order Form for the TPTP World

Daniel Ranalter¹(✉) ID, Cezary Kaliszyk¹,² ID, Florian Rabe³ ID, and Geoff Sutcliffe⁴ ID

¹ Computational Logic, University of Innsbruck, Innsbruck, Austria
d.ranalter@gmail.com

² School of Computing, University of Melbourne, Melbourne, Australia
ckaliszyk@unimelb.edu.au

³ Computer Science, University of Erlangen-Nuremberg, Erlangen, Germany
florian.rabe@fau.de

⁴ Department of Computer Science, University of Miami, Coral Gables, USA
geoff@cs.miami.edu

**Abstract.** Much of the current research and development in the field of automated reasoning builds on the infrastructure provided by the TPTP World. The TPTP language for logical formulae is central to the far-reaching adoption of the TPTP World. This paper introduces the Dependently Typed higher-order Form (DHF) of the TPTP language. It takes advantage of already established binders in the syntax, and is thus a minimally intrusive extension to the Typed Higher-order Form (THF). A starting set of over 100 problems is provided to exhibit the usefulness and incite interest in DHF. Some tools that are already able to reason about problems in the DHF language are discussed.

**Keywords:** Automated Theorem Proving · Dependent Types · Higher-Order Logic

## 1 Introduction

The TPTP World [31] is a well-established infrastructure that supports research, development, and deployment of Automated Theorem Proving (ATP) systems. The TPTP language [27] is one of the keys to the success of the TPTP World. It has variants that support uniform expression of logical formulae across a wide range of logics. The TPTP language is used for writing both problems and solutions, which enables convenient communication between ATP systems and tools. The majority of modern ATP systems accept input in TPTP syntax. The TPTP language variants that form the basis for this work are the monomorphic and polymorphic typed higher-order forms (TH0 and TH1) [8,32] (see Sect. 2.1 for the background and further variants).

All the existing typed TPTP language variants are *simply* typed. However, there is a steady increase of interest in *dependently* typed systems, such as
Agda [3], Rocq [1,37], and Lean [9]. This interest extends to the SMT community, where the proposed version 3.0 of SMT-LIB is to include dependent types<fnref n="1" />. Dependent types allow for the elegant formulation of complex data structures, possibly even a direct encoding of correctness properties. This paper introduces the Dependently Typed higher-order Form (DHF) of the TPTP language.

While dependent types are frequently used in interactive theorem proving, Automated Theorem Proving (ATP) has yet to embrace dependent types. Rothgang et al. made first steps towards bringing ATP and dependent types together, by introducing dependently typed higher-order logic (DHOL) [17,18]. With only two minor extensions to the familiar syntax of Church-style HOL [6], DHOL makes dependent types easily accessible: HOL base types are extended into dependent base types that can take term arguments, and the function type $A \to B$ is changed into a dependent function type $\Pi x : A.B$. Originally DHOL did not allow quantifying over types or stating the equality of types, but a polymorphic version is in development.

As in FOL and HOL, DHOL allows arbitrary axioms that may constrain equality of terms in undecidable ways, and consequently DHOL's type checking is undecidable (see Sect. 3.2). To manage this complication Rothgang et al. provide an algorithm that reduces the well-formedness of a statement to a set of proof obligations. Thus theorem proving is needed to check the well-formedness of a problem's formulae, not just to prove the conjecture. Happily, typically that does not make it harder to prove the conjecture. To increase ATP support for DHOL, Rothgang et al. define a translation from well-typed DHOL to HOL that preserves provability in both directions, thereby making DHOL available for regular HOL ATP systems, albeit without leveraging DHOL's dependent types for more efficient proving. Furthermore, the translation introduces additional axioms capturing the constraints of the dependent types, thereby potentially complicating proof search. Several interactive theorem provers had previously employed the same idea, sacrificing decidable typing to gain the expressivity of dependent types, while keeping the general feel of the language simple. Most importantly, PVS [12] essentially contains DHOL as a fragment, but extends it beyond the capabilities of current automated provers. Mizar [38], using soft typing on top of first-order set theory, can also capture DHOL-like features.

A detail missing from the original formulation of DHOL was the choice operator. Ranalter et al. investigated the effects of losing the non-emptiness constraint in DHOL on Hilbert's choice in [16]. To this end, they extended the – to the authors knowledge – first native implementation of DHOL into the ATP system Lash, by Niederhauser et al. [11]. Their experiments strongly suggest that native reasoning in DHOL significantly outperforms reasoning on translated problems.

This work describes how DHOL is being integrated into the TPTP World, in a new TPTP language variant "Dependently Typed higher-order Form" (DHF), with monomorphic and polymorphic subvariants (DT0 and DT1). DHF requires only very minor changes to the familiar TPTP language syntax, mostly using existing notions for binders and application operators, thereby providing the

<footnote n="1">¹ smt-lib.org/version3.</footnote>
ATP community with the necessary foundations on which research into depen-
dently typed automated reasoning can thrive. A set of over 100 problems in DHF,
taken from several different sources, has been curated as an initial contribution
to the TPTP problem library. The problems provide a spread of interesting for-
mulations focusing on a variety of difficulty levels in proving the conjecture as
well as in type checking.

Section 2 reviews the TPTP World and establishes the necessary back-
ground for DHOL, slightly generalizing the original DHOL definition to make it
more suitable for TPTP. Section 3 introduces the new DHF form. Section 4 gives
a short overview of the starting set of problems, and Sect. 5 introduces tools that
already support the new form. Finally, Sect. 6 concludes and gives an outlook
over future work.

2 Preliminaries

2.1 The TPTP World and Infrastructure

The TPTP World infrastructure includes the TPTP language [28], the TPTP
problem library [25], the TSTP solution library [26], the SZS ontologies [24],
the Specialist Problem Classes (SPCs) and problem difficulty ratings [29], Sys-
temOnTPTP [23] and StarExec [22], and the CADE ATP System Competition
(CASC) [30]. The problem library is a large collection of Thousands of Problems
for Theorem Proving – hence the name. The problem library release v9.1.0 con-
tains over 26000 problems from over 50 different domains, written in the TPTP
language. The problems are categorized into Specialist Problem Classes accord-
ing to their syntactic and logical status. The TSTP solution library is the result
of running numerous ATP systems on the problems in that library and collecting
their output. The TPTP and TSTP libraries provide the basis for assigning a
difficulty rating to each problem, according to which ATP systems are able to
solve the problem.

The most salient feature of the TPTP World for this work is the TPTP lan-
guage. Originally the TPTP language supported only first-order clause normal
form (CNF) [35]. Over time, more complex logics were added, starting with first-
order form (FOF) in TPTP release v2.0.0 [25]. Releases v3.0.0 and v4.0.0 added
monomorphic typed higher-order (TH0) [32] and monomorphic typed first-order
(TF0) [34] forms to the mix respectively. These got extended to their polymor-
phic variants TF1 and TH1 in releases v5.0.0 [2] and v6.0.0 [8]. Release v7.0.0
of the TPTP started to include extended typed first-order form (TXF) [33]
which extends the typed first-order form with conditionals, let expressions, and
boolean terms. All the listed extensions to the TPTP are classical in nature.
This changed with the addition of non-classical typed first-order form (NTF) in
release v9.0.0 [21]. A general principle of the TPTP language is: “We provide the
syntax, you provide the semantics”. As such, there is no a priori commitment to
any semantics for each of the language forms, although in almost all cases the
intended logic and semantics are well known.

Problems and solutions are built from *annotated formulae* of the form
language(name, role, formula, source, useful_info)

The *languages* supported are `cnf` (clause normal form), `fof` (first-order form), `tff` (typed first-order form), and `thf` (typed higher-order form). The *role*, e.g., *axiom*, *lemma*, *conjecture*, defines the use of the formula. In a *formula*, terms and atoms follow Prolog conventions – functions and predicates start with a lowercase letter or are 'single quoted', and variables start with an uppercase letter. The language also supports interpreted symbols that either start with a `$`, e.g., the truth constants `$true` and `$false`, or are composed of non-alphabetic characters, e.g., integer/rational/real numbers such as 27, 43/92, -99.66. The logical connectives in the TPTP language are `!>`, `?*`, `@+`, `@-`, `!`, `?`, `~`, `|`, `&`, `=>`, `<=`, `<=>`, and `<~>`, for the mathematical connectives $Π$, $Σ$, choice (indefinite description), definite description, $∀$, $∃$, $¬$, $V$, $∧$, $⇒$, $⇔$, and $⊕$ respectively. Equality and inequality are expressed as the infix operators `=` and `!=`. The *source* and *useful_info* are optional.

## 2.2 Dependently Typed Higher-Order Logic

Dependently typed higher-order logic (DHOL) is an extension of Church's higher-order logic (HOL) [6] introduced by Rothgang et al. [17]. It takes the widely supported HOL and equips it with dependent types, i.e., types that take term arguments. As such, it is a classical and extensional type theory, as opposed to the theory used in Rocq [1,37], Lean [9], or others [3,13] that rely on an intensional type theory. Notable exceptions to this trend are PVS [19], NuPRL [7], and F* [36].

The extensionality of DHOL comes at the cost of making type checking undecidable because it must consider term equality, which may be subject to arbitrary axioms. Essentially, typing becomes undecidable if a type depends on a type for which equality is undecidable. This is because type checking *t* against type *a n* must be done by inferring the type of *t*, say *a m*, and then checking *a m = a n*, and thus *m = n*. If all dependent type symbols depend only on types for which equality is decidable (e.g., the examples below where we only use natural numbers with Presburger arithmetic), type checking is decidable. Otherwise, e.g., when using types depending on natural numbers with Peano arithmetic, type checking is undecidable.

The gain of having judgmental and provable equality coincide is significant: It positions DHOL much closer to how mathematics is usually done in the context of ATP. The availability of dependent types allows the elegant definition of data structures such as lists of fixed-length, intervals of numbers, or vector spaces over some field. It also allows encoding constraints in the types, which can remove the need for lengthy and error-prone guards in programming and track invariants useful for theorem proving. The cost – which might seem steep at first glance – is mitigated by the ever-increasing performance of ATP systems, and the fact that in many cases the proof obligations resulting from type checking are much simpler than the original proving problem.

The changes to the TPTP syntax to accommodate DHF are small: the definition of the simple base type is changed to a type that can accept term arguments,
and the simple function type $A \to B$ is changed to $\Pi x : A.B$. This makes it possible to let the result type of the function depend on the specific term of the argument.

Figure 1 gives the grammar of DHOL. A dependent base type $a$ with arity $n$ is written $a : \Pi x_1 : A_1, \dots, x_n : A_n$. type, and it is a simple base type if $n = 0$. Declarations of this form are part of the theory against which the type checking procedure is performed. In addition to base type declarations, theories may declare constant symbols $c$ and axioms $\triangleright F$. A context specifies typed variables and assumptions. Contexts are superficially similar to theories, but denote local declarations, and as such, do not contain type declarations. ◦ and • denote the empty theory and context respectively. The order in a theory or context matters because the well-typedness of declarations might depend on preceding axioms. Types, as they appear in statements and typing judgements, are either fully applied base types, (dependent) function types, or classical booleans $o$. Terms are built from variables/constants, lambda abstraction, application, and the usual connectives and quantifiers. Regular HOL can be recovered by omitting the highlighted elements – this is exactly the case when the arity of all base types is 0.

<figure><img src="image_51.png" /><figcaption>Fig. 1. The grammar of DHOL</figcaption></figure>

The following example encodes the familiar notion of fixed-length lists. As prerequisites, we give the usual notion of natural numbers in a simple type nat and a simple type char of characters for the elements of the lists:

<figure><img src="image_52.png" /></figure>

Then $\text{vec } n$ encodes the type of fixed-length lists of characters of length $n$:

<figure><img src="image_53.png" /></figure>

*Dependent Connectives*. In DHOL it is desirable to make the binary connectives conjunction, implication, and disjunction dependent in the sense that the well-formedness of the second argument may assume the truth (for conjunction and
implication) or the falsity (for disjunction) of the first argument. Consider the statement $a =_A b \Rightarrow f a =_{B(a)} f b$. The well-formedness of the right-hand side requires the left-hand side as a premise. More precisely, $\Gamma \vdash F : o$ resp. $\Gamma \vdash F$ expresses that $F$ is a well-formed resp. provable formula in context $\Gamma$. The definition of well-formed formulae is:

$$ 
\begin{array}{l@{\quad}l@{\quad}l}
\Gamma \vdash F \Rightarrow G & \text{if} & \Gamma \vdash F \text{ and } \Gamma, \triangleright F \vdash G \\
\Gamma \vdash F \wedge G & \text{if} & \Gamma \vdash F \text{ and } \Gamma, \triangleright F \vdash G \\
\Gamma \vdash F \vee G & \text{if} & \Gamma \vdash F \text{ and } \Gamma, \triangleright \neg F \vdash G
\end{array}
$$

where the **marked** parts make the connectives dependent. The usual natural deduction proof rules of implication and conjunction are the same as for the non-dependent versions. The proof rules for disjunction are adjusted as follows:

$$ \frac{\Gamma \vdash F \quad \Gamma, \triangleright \neg F \vdash G : o}{\Gamma \vdash F \vee G} \qquad \frac{\Gamma, \triangleright \neg F \vdash G}{\Gamma \vdash F \vee G} \qquad \frac{\Gamma, \triangleright F \vdash C \quad \Gamma, \triangleright \neg F, \triangleright G \vdash C}{\Gamma, \triangleright F \vee G \vdash C} $$

As usual, it is possible to choose some connectives as primitives, from which the others are defined. Rothgang et al. choose equality and implication. Contrary to HOL, they included implication because they could not define the dependent binary connectives solely from equality. For the TPTP World, it is better not to choose primitive connectives – that choice should be left to the ATP system developers. Therefore DHF extends the work by Rothgang et al. to make all connectives primitive. ATP systems can choose which connectives to treat as abbreviations, but in doing so must take the dependent nature of the connectives into account. Note that dependent connectives break the commutativity of conjunction and disjunction. While seemingly disruptive, sacrificing commutativity in this way is common practice, e.g., for short-circuit evaluation of Boolean terms in programming languages. To clarify the impact on theorem proving, Table 1 summarizes typical proof rules for FOL and their status in DHOL. Roughly speaking, all rules that do not affect the order of subformulae remain sound, while the rest of the rules require the additional check to ensure the result remains well-formed. In particular, all rules needed to perform CNF or clause normal form transformations remain available.

Developing advanced calculi for DHOL is beyond the scope of this paper. However, for example, one way to generalize resolution is to store clauses as lists $[L_1, \dots, L_n]$ where the well-formedness of each $L_i$ may depend on $\neg L_j$ for $j < i$. Resolving $[A, \vec{L}]$ and $[\neg A, \vec{M}]$ to $[\vec{L}, \vec{M}]$ is sound if the resolvent is well-formed, i.e., if the well-formedness of the $L_i$ resp. $M_i$ does not depend on $\neg A$ resp. $A$.

**Polymorphic DHOL.** DHOL as presented in the previous section and [17] is monomorphic. ATP for polymorphic DHOL, as well as proofs of properties for such an extension of the calculus, is ongoing parallel work. Polymorphic logics are already available in the TPTP language, so it is natural to offer polymorphic DHF. All the polymorphic example problems considered so far use only
<table><caption>**Table 1.** Typical proof rules for FOL and their status in DHOL</caption><thead><tr><th>Rule</th><th>Holds in DHOL</th></tr></thead><tbody><tr><td colspan="2">For disjunction and conjunction</td></tr><tr><td>associativity</td><td>✓</td></tr><tr><td>commutativity</td><td>Only if both sides are well-formed</td></tr><tr><td>idempotence, e.g., A ∧ X ∧ A ⇔ A ∧ X</td><td>✓ (Drop the <i>second</i> occurrence)</td></tr><tr><td>de Morgan laws</td><td>✓</td></tr><tr><td>distributivity of one over the other</td><td>✓</td></tr><tr><td>absorption, e.g., A ∧ (A ∨ B) ⇔ A</td><td>✓</td></tr><tr><td colspan="2">For implication</td></tr><tr><td>A ⇒ B ⇔ ¬A ∨ B</td><td>✓</td></tr><tr><td>¬(A ⇒ B) ⇔ A ∧ ¬B</td><td>✓</td></tr><tr><td>¬(A ⇒ B) ⇔ ¬B ⇒ ¬A</td><td>Only if both sides are well-formed</td></tr><tr><td colspan="2">For quantifiers and equality</td></tr><tr><td>all rules</td><td>✓</td></tr><tr><td colspan="2">Common calculus rules</td></tr><tr><td>classical reasoning</td><td>✓</td></tr><tr><td>weakening</td><td>✓</td></tr><tr><td>contraction</td><td>✓ (Drop the <i>second</i> occurrence)</td></tr><tr><td>exchange</td><td>Only if still well-formed</td></tr><tr><td>cut</td><td>✓</td></tr><tr><td>resolution</td><td>Only if the clauses remain well-formed</td></tr></tbody></table>

shallow/rank-1 polymorphism in line with the existing polymorphic first- and higher-order forms for TPTP.

**Choice.** Hilbert's choice operator has been part of HOL since its inception by Church [6]. As such, it is natural to include it in DHOL. This introduces some complications: Due to the usual non-emptiness constraint on types, the semantics of choice are clear in HOL. However, DHOL no longer abides by this constraint, requiring a design decision that affects well-typedness and provability. Experiments done in [16] suggest that the variant of choice dubbed “strong choice” results in more efficient automated reasoning. The eponymous characteristic of strong choice is the requirement that ∃x : A.t needs to be true for (εx : A.t) : A to be well-typed. Such a requirement for typing fits well with DHOL in general, and as ATP is the main concern this is the variant of choice, as it were. The problem set described in Sect. 4 includes some examples supporting this variant.

**Translation.** In order to take advantage of the ATP systems available for regular HOL, Rothgang et al. define a dependency-erasure [17], and thereby a translation from DHOL into regular HOL. They also prove that this translation is
sound and complete for well-typed DHOL problems. Due to this result, and the implementation of the translation into the preprocessor of the Leo-III theorem prover [20], there existed reasoning support for DHOL even before native DHOL reasoning was implemented in the Lash ATP system by Niederhauser et al. [11]. Information lost due to the erasure of term dependencies is captured in Partial Equivalence Relations (PERs) – symmetric and transitive relations on pairs of terms – with the idea that the relation is reflexive exactly for those terms that were previously of the same dependent type. The translation is shown in Fig. 2. The translation $\bar{t}$ of a term $t$ is defined inductively on the structure of the terms. The erasure of one type declaration results in three erased declarations: the erased type, the PER constant and an axioms stating its properties. The definition of the erasure on $\forall$- and $\exists$-quantified terms is notable as it uses a PER as guard on the argument. To see why, note that, e.g., $\forall x : A.t$ can be defined in terms of equality as $\lambda x : A.t =_{A \to o} \lambda x : A.\top$. The erasure creates a PER from

<figure><img src="image_54.png" /></figure>

<figure><img src="image_55.png" /></figure>

PER for each type

$$ 
\begin{align*}
o^* t u &= t =_o u \\
(a \ t_1 \ \dots \ t_n)^* u v &= a^* \bar{t}_1 \ \dots \ \bar{t}_n \ u \ v \\
(\Pi x : A.B)^* t u &= \forall x, y : \bar{A}. A^* x y \Rightarrow B^*(t x)(u y)
\end{align*}
$$

<caption>Fig. 2. The translation from DHOL to HOL.</caption>
this typed equality with the guarded input in the premise, and the erased term in the consequence of the implication as seen in the erasure of $\forall$.

As an example of erasure, consider the list of `chars` [a, b], represented by a term `cons 1 a (cons 0 b nil)` of type `vec 2`, where `0`, `suc 0`, `suc (suc 0)`, ... is abbreviated as `0, 1, 2, ...`. Applying the erasure gives `cons a (cons b nil)` of type `vec`. A predicate would be generated, establishing that this particular list is in the PER of vectors of length 2: `vec* 2 t t` where t stands for `cons a (cons b nil)`. While one might think that unary predicates would be sufficient as a type guard, PERs becomes necessary to express the typing and equality of higher-order functions: functions are well-typed if they map well-typed inputs to well-typed outputs, and they are equal if they agree on well-typed inputs.

# 3 DHF

After establishing the theoretic background, this section presents the realization of DHOL in the TPTP language. Syntax and semantics are given, as well as an exposition to the problem of type checking.

## 3.1 Syntax

The syntax of DHF requires almost no change to the existing TPTP syntax. The TPTP language already defines the `!>` binder for types. In the typed TPTP language variants it is currently used for only polymorphism, e.g.,

`cons : !>[A: $tType]: (A > (list @ A) > (list @ A))`

is a type declaration for a polymorphic `cons`. The TPTP syntax does not forbid listing terms in the types of such variable lists. This fact is used to unobtrusively extend TPTP by dependent types. A dependent type symbol declaration is written with $m$ terms of $n$ types as

`a : !>[x₁: A₁, ..., xₘ: Aₙ]: $tType`

or alternatively

`a : A₁ > ... > Aₙ > $tType.`

Such types use the application operator `@`, to instantiate the terms to the dependent type:

`a @ t₁ @ ... @ tₘ.`

In polymorphic problems, the variable list is prepended with the type variables, which may appear in the same binder. An example of a problem in DHF is shown in Fig. 3.
```h
thf(elem_type,type,      elem: $tType ).
thf(nat_type,type,      nat: $tType ).
thf(zero_type,type,      zero: nat ).
thf(suc_type,type,      suc: nat > nat ).
thf(plus_type,type,      plus: nat > nat > nat ).
thf(list_type,type,      list: nat > $tType ).
thf nil_type,type,      nil: list @ zero ).
thf(cons_type,type,      cons:
!>[N: nat] : (elem > (list @ N) > (list @ (suc @ N))) ).
thf(app_type,type,      app:
!>[N: nat,M: nat] : ((list @ N) > (list @ M) >
                   (list @ (plus @ N @ M))) ).

thf(ax1,axiom,
! [N: nat] : ((plus @ zero @ N) = N) ).

thf(ax2,axiom,
! [N: nat,X: list @ N] : ((app @ zero @ N @ nil @ X) = X) ).

thf(plusnell,axiom,
! [M1: nat,M2: nat,M3: nat] :
  ( (plus @ M1 @ (plus @ M2 @ M3))
   = (plus @ ( plus @ M1 @ M2) @ M3) ) ).

thf(list_app_nel_base,conjecture,
! [M2: nat,L2: list @ M2,M3: nat,L3: list @ M3] :
  ( (app @ zero @ (plus @ M2 @ M3) @ nil @
     (app @ M2 @ M3 @ L2 @ L3))
   = (app @ (plus @ zero @ M2) @ M3 @
     (app @ zero @ M2 @ nil @ L2) @ L3)) ).
```

<caption>Fig. 3. The base case of associativity of append on fixed-length lists.</caption>

## 3.2 Type Checking

Due to equality reflection, type checking for DHOL is, in general, undecidable. Nevertheless, problems need to be well-typed, otherwise the translation outlined in Sect. 2.2 might not be sound. Type checking in DHF thus takes on a larger role than in other logics in the TPTP World.

While performing the usual type checking procedure in DHOL, obligations of the form $a t_1 \cdots t_n \equiv a u_1 \cdots u_n$, are generated. These establish equality of the dependent base types applied to arguments $t_1 \cdots t_n, u_1 \cdots u_n$ of appropriate types. The type equality holds if all pairs $t_i, u_i$ are equal, which depends on the available axioms. This can create interesting situations where a problem must include axioms that are not necessary for proving the conjecture itself, but are necessary for type checking it. The common example of fixed-length lists is one such example: the statement of the associativity of append is well-typed only if addition on nat is associative, and thus requires including the defining equations
of addition. To prove the problem only the defining equations of appending lists are needed.

The undecidability of type checking can lead to compromises. One such com-
promise is “shallow type checking”. When a problem file is shallowly checked, only
the simply typed skeleton of the problem is considered, i.e., term arguments to
types as well as dependent functions are ignored. This collapses to type checking
as is done on non-dependently typed problems, and is decidable. This form of
type checking is sufficient to catch many careless mistakes in the formulation
of problems, and provides a basic check of issues often found in human-written
DHOL problems. Examples are: mismatches in the number of arguments of a
base type or function, and egregious type mismatches. Shallow type checking
provides a valuable sanity check for users, especially considering the complexity
that problems in DHOL forms can reach.

3.3 Semantics

As for HOL, there are two kinds of semantics for DHOL: standard models are
intuitive and are the ones that are usually used; non-standard (Henkin) models
are a generalization that is needed for completeness. A full account is given in
the forthcoming [15], which is summarized below. The rules of DHOL, as given
by Rothgang et al., already define which formulae are theorems.

*Standard Models.* Given a theory *T*, a standard model *M* ∈ [[*T*]] is a tuple providing an interpretation for every declaration in *T*. Similarly, given a context Γ, an assignment α ∈ [[Γ]]<sup>M</sup> for Γ is a tuple providing an interpretation for every declaration in Γ. These induce the interpretation function [[−]]<sub>α</sub><sup>M</sup> (with α omitted if the context is empty), which is defined inductively for all the syntax. In particular, the possible components of a model are defined by induction on declarations:

- For a type symbol with arguments Γ = x₁ : A₁, ..., xₙ : Aₙ, a function
  [[Γ]]<sup>M</sup> → SEΓ

- For a term symbol *c* : A, a value from [[A]]<sup>*M*</sup>

- For an axiom ▷ *F*, a unique choice ✓ if [[*M*]]<sub>α</sub><sup>*F*</sup> = 1, and no choice otherwise

For the components of an assignment:

- For a term variable *x* : A, a value from [[A]]<sub>α</sub><sup>*M*</sup>

- For an assumption ▷ F, a unique choice ✓ if [[M]]<sub>α</sub><sup>F</sup> = 1, and no choice otherwise

For types and terms, the model is defined by induction in the usual way, in
particular

- [[o]]<sub>α</sub><sup>M</sup> = {0, 1}

- [[Πx : A.B]]<sub>α</sub><sup>M</sup> is the set of functions f mapping every u ∈ [[A]]<sub>α</sub><sup>M</sup> to some
  f(u) ∈ [[B]]<sub>α<sup>u</sup></sub><sup>M</sup> where α<sup>u</sup> extends α with the value u for x
*General Models.* The definition of general models generalizes the Henkin models from HOL by applying methods from categorical models of type theory. First, akin to assignments for $\Gamma$, substitutions $\gamma : \Gamma \to \Delta$ as lists of terms or $\check{\text{}}$ by induction on $\Gamma$ are defined:

- For a term variable $x : A$, a term of type $\Delta \vdash A[\gamma]$

- For an assumption $\vdash F$, the unique choice $\check{\text{}}$ if $\Delta \vdash F[\gamma]$, and no choice otherwise

Equality of contexts and substitutions is defined by applying the existing equality judgments for types and terms component-wise. For every theory $T$, this yields the syntactic category $\llbracket T \rrbracket$ of $T$-contexts and substitutions. A general model is then defined as any pushout-preserving contravariant functor $\Phi : \llbracket T \rrbracket \to SET$. From such a $\Phi$, an interpretation function is extracted using $\Phi(x : A)$ as the interpretation of the type $A$ and $\Phi(t)$ as the interpretation of the term $t : A$ (seen as a substitution $x : A \to \bullet$). These general models must further satisfy $\Phi(o) = \{0, 1\}$, and $\Phi \models F$ is defined as $\Phi(F) = 1$. Here the pushout-preservation essentially corresponds to the preservation of substitution, i.e., interpretation and substitution commute. The lack of any preservation of exponentials allows for a *non-compositional* interpretation of function types. This approach can be seen as a generalization of Henkin models, which also preserve substitution but do not need to interpret function types compositionally. Contrary to Henkin models, the interpretation of $\lambda$ and application terms can also be non-compositional in these general models as long as substitution is preserved.

*Models for Polymorphic DHOL.* As mentioned above, a rank-1 polymorphic variant of DHOL is being developed in parallel work. It is straightforward to extend standard models to polymorphic DHOL. The syntax of binding a type variable corresponds to abstracting over an arbitrary set on the semantic side. In particular, the interpretation of a polymorphic term/type symbol with $n$ type variables takes $n$ sets as arguments. Polymorphic axioms correspond to universal quantification over sets. The definition of syntactic category and general models is expected to carry over to polymorphic DHOL as well. This has not been investigated in detail.

# 4 Problem Dataset

Over 100 problems in DHF format have been collected for addition to the TPTP problem library. Their classification is presented in Table 2 and discussed here (with 36 problems just for testing DHOL prover features omitted). The number of problems in each class is given in the last column. The problems concern several domains that can benefit from dependent types. While [17] shows DHOL to be sound and complete, the strength of the existing automation for this foundation (discussed in Sect. 5) still needs to be improved. For this reason, some of the harder problems were broken down into simpler subproblems that
can be proven independently. Some list properties that require both induction and reasoning with dependent types are an instance of this. For example, the fact that list append is associative, `ListAppAssoc`, is split into three subproblems, showing the particular induction scheme, the proof of the base case, and the step case. These three subproblems are easier to prove than their combined version, which is also included. Some problems benefit from intermediate lemmas, e.g. the instantiation of the inductive step case. These are found in the "Lemmas" categories of Table 2.

One of the simplest classes of examples are lists that depend on their length (also called vectors, for example in the Rocq library). As the list libraries of most interactive theorem provers are substantial, it is relatively easy to experiment with many properties of dependently typed lists. Such properties include the aforementioned associativity of `append`, corollaries of this statement, or involution statements about the `reverse` function. Some of these list examples are extended to their polymorphic generalizations, which are in the "Polymorphic" categories.

The idea of expressing well-known but sometimes challenging properties extends to several other algebraic data types, such as matrices that have fixed dimensions, and lists of lists. Red-black trees are a well-known data structure for balanced trees where the invariant can be expressed using dependent types, and again several problems concerning this type are included. The `Fin` type present in several proof libraries has been manually recreated, and some problems about these are in the ROCQ category of Table 2. The collection includes the five examples from category theory that were originally presented in [17], slightly reformatted to match the TPTP syntax. To make use of the choice operator [16], several problems about dependent higher-order Skolemization are included. Choice is also used in a function definition with no fixed point, and conjectures establishing this are presented in the "no FP" category. Finally, several simple tests to evaluate the ability of provers to perform native DHOL inferences are provided.

Some of the dependent HOL problems are more interesting from a proof perspective – the deep type checking is there only to make sure the problem is well-formed. For example, for all the dependent list problems, the type checking obligations are there mostly to make sure no incorrect calls are being made, but they are relatively straightforward to discharge. It is the proof that requires more logical reasoning. Other problems, while relatively straightforward in terms of proving, are harder to type check. This is because it is possible to use dependent types to encode important properties and invariants in the type system.

# 5 Tools

This section discusses the tools capable of processing problems in DHF format.
<table><caption>**Table 2.** The categories of the DHF problems.</caption><thead><tr><th>Problem Type</th><th>Problem Category</th><th>Problem Count</th></tr></thead><tbody><tr><td rowspan="10">Monomorphic Complete</td><td>Category theory</td><td>5</td></tr><tr><td>Choice basic</td><td>11</td></tr><tr><td>Choice list</td><td>3</td></tr><tr><td>Choice no fixed point</td><td>10</td></tr><tr><td>List app assoc</td><td>3</td></tr><tr><td>List app assoc corollary</td><td>1</td></tr><tr><td>List app nil</td><td>4</td></tr><tr><td>List of lists</td><td>1</td></tr><tr><td>List reversal involution</td><td>1</td></tr><tr><td>List reversal inv lemma</td><td>3</td></tr><tr><td>Matrices</td><td>5</td></tr><tr><td>ROCQ</td><td>3</td></tr><tr><td rowspan="5">Monomorphic Lemmas</td><td>Choice no fixed point</td><td>10</td></tr><tr><td>List app assoc</td><td>5</td></tr><tr><td>List app assoc corollary</td><td>5</td></tr><tr><td>List reversal involution</td><td>5</td></tr><tr><td>List reversal inv lemma</td><td>11</td></tr><tr><td rowspan="4">Polymorphic Complete</td><td>List app assoc poly</td><td>3</td></tr><tr><td>List app nil poly</td><td>4</td></tr><tr><td>List reversal involution poly</td><td>1</td></tr><tr><td>Red-black tree</td><td>3</td></tr><tr><td rowspan="3">Polymorphic Lemmas</td><td>List app assoc poly</td><td>14</td></tr><tr><td>List reversal involution poly</td><td>13</td></tr><tr><td>Red-black tree</td><td>9</td></tr></tbody></table>

## 5.1 The Logic Embedding Tool

The Leo-III [20] prover includes the *Logic Embedding Tool*, which has been extended to support polymorphic DHF. The tool implements the erasure presented in Sect. 2.2, and incorporates the polymorphic extension. The tool can generate both the type checking obligations and the translated problem separately. This makes it possible to translate DHF problems into THF problems (that do not have dependent types). The embedding tool is available as NTFLET in SystemB4TPTP<fnref n="2" />. The embedding tool enables the use of existing higher-order ATP systems for solving DHF problems, by pipelining the output from NTFLET to a THF ATP system of the user's choosing. This has been implemented as the DT2H2X ATP systems, available in SystemOnTPTP<fnref n="3" />.

<footnote n="2">² tptp.org/cgi-bin/SystemB4TPTP.</footnote>

<footnote n="3">³ tptp.org/cgi-bin/SystemOnTPTP.</footnote>
## 5.2 DLash

The Lash prover [5] is a partial reimplementation of the tableaux calculus of Satallax [4], using a central term representation with perfect sharing. This design facilitated the implementation of the DLash extension of Lash, which handles DHF [11]. In addition to the erasure implementation, DLash can process monomorphic dependently typed higher-order logic with choice. As with the Logic Embedding Tool, type checking and proving can be requested separately. DLash, like Satallax, includes a strategy language used to build so-called modes. The current version includes 36 dedicated modes for dependent types, tailored to specific problem types. DLash is available in SystemOnTPTP<fnref n="4" />.

## 5.3 MMT

MMT [14] is a logical framework designed to formalize and manage large collections of interconnected formal systems and their libraries, using modular theory graphs. A particular application of MMT is rapid prototyping [10], and it was the tool originally used to develop and prototype DHOL. The MMT/DHOL implementation offers reconstruction of omitted types and implicit arguments as well as parsing against user-defined notations. It can be used to interactively author and type check DHOL problems and export them in TPTP format. It uses the PER translation, and calls the Leo-III prover to discharge the resulting proof obligations. MMT is mostly useful for developing formalizations, rather than proving TPTP conjectures. Therefore, it does not provide a TPTP import at this point, but provides additional evidence of the well-typedness DHF problems.

## 5.4 TPTP Systems

As discussed in Sect. 2.1, TPTP includes several generic tools capable of processing problems and solutions. For DHF problems:

- TPTP4X pretty-prints DHF problems and solutions, and offers various transformations/augmentations of problems.

- BNFParser produces the abstract syntax tree from parsing a DHF problem.

- Leo-III-STC validates the syntax and types of DHF problems.

- ProblemStats outputs various syntactic measures for problems.

All these tools are available in SystemB4TPTP<fnref n="5" />. For DHF proofs:

- ProofStats outputs various syntactic measures for DAG-structured proofs.

- IDV provides interactive viewing of proofs from DHF problems.

All these tools are available in SystemOnTSTP<fnref n="6" />.

<footnote n="4">⁴ tptp.org/cgi-bin/SystemOnTPTP.</footnote>

<footnote n="5">⁵ tptp.org/cgi-bin/SystemB4TPTP.</footnote>

<footnote n="6">⁶ tptp.org/cgi-bin/SystemOnTSTP.</footnote>
# 6 Conclusion

This paper has described DHF, the dependently typed higher-order form of the TPTP language. It responds to the growing interest in dependently typed automated reasoning as exemplified by the number of TPTP problems and tools that have cropped up in the short time since DHOL was first described. It can be seen as pushing the boundary of automated theorem proving towards language features that have previously been found only in interactive provers.

DHOL problems sometimes used differing standards, which defeated the uniformity advantage that the TPTP language provides. This work unifies them, and provides over a 100 problems from different domains, benefiting from the use of dependent types. We hope that the availability of dependent types in the TPTP will stimulate research into dependently typed automated theorem proving, by making it easier to exchange and compare results. Extending existing systems with support for DHF, and improving the performance of the systems that already exist, will be important next steps. In particular, the extension of superposition-based theorem proving to dependent types is a tantalizing goal.

**Acknowledgements.** The authors thank Johannes Niederhauser and Colin Rothgang for granting access to their DHOL problems that are in the problem dataset. This work was supported by the ERC PoC grant no. 101156734 “FormalWeb3”.

# References

1. Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development: Coq'Art: The Calculus of Inductive Constructions. Springer, Cham (2004)

2. Blanchette, J.C., Paskevich, A.: TFF1: the TPTP typed first-order form with rank-1 polymorphism. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 414–420. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-38574-2_29

3. Bove, A., Dybjer, P., Norell, U.: A brief overview of Agda – a functional language with dependent types. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 73–78. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-03359-9_6

4. Brown, C.E.: Satallax: an automatic higher-order prover. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS (LNAI), vol. 7364, pp. 111–117. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-31365-3_11

5. Brown, C.E., Kaliszyk, C.: Lash 1.0 (system description). In: Blanchette, J., Kovács, L., Pattinson, D. (eds.) Automated Reasoning. LNAI, vol. 13385, pp. 350–358. Springer, Cham (2022). https://doi.org/10.1007/978-3-031-10769-6_21

6. Church, A.: A formulation of the simple theory of types. J. Symb. Log. 5(2), 56–68 (1940). https://doi.org/10.2307/2266170

7. Constable, R., et al.: Implementing Mathematics with the Nuprl Development System. Prentice-Hall (1986)

8. Kaliszyk, C., Sutcliffe, G., Rabe, F.: TH1: the TPTP typed higher-order form with rank-1 polymorphism. In: Fontaine, P., Schulz, S., Urban, J. (eds.) Proceedings 5th Workshop on Practical Aspects of Automated Reasoning. CEUR Workshop
Proceedings, vol. 1635, pp. 41–55. CEUR-WS.org (2016). https://ceur-ws.org/Vol-1635/paper-05.pdf

9. de Moura, L., Ullrich, S.: The lean 4 theorem prover and programming language. In: Platzer, A., Sutcliffe, G. (eds.) CADE 2021. LNCS (LNAI), vol. 12699, pp. 625–635. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-79876-5_37

10. Müller, D., Rabe, F.: Rapid prototyping formal systems in MMT: case studies. In: Miller, D., Scagnetto, I. (eds.) Logical Frameworks and Meta-languages: Theory and Practice, pp. 40–54 (2019)

11. Niederhauser, J., Brown, C.E., Kaliszyk, C.: Tableaux for automated reasoning in dependently-typed higher-order logic. In: Benzmüller, C., Heule, M.J.H., Schmidt, R.A. (eds.) Automated Reasoning. LNAI, pp. 86–104. Springer, Cham (2024). https://doi.org/10.1007/978-3-031-63498-7_6

12. Owre, S., Shankar, N.: The formal semantics of PVS. Technical report. SRI-CSL-97-2, SRI International (1997)

13. Pfenning, F., Schürmann, C.: System description: Twelf — a meta-logical framework for deductive systems. In: CADE 1999. LNCS (LNAI), vol. 1632, pp. 202–206. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-48660-7_14

14. Rabe, F.: A modular type reconstruction algorithm. ACM Trans. Comput. Log. 19(4), 1–43 (2018)

15. Rabe, F.: Model theory for dependently-typed higher-order logic (2024). Under review, see https://kwarc.info/people/frabe/Research/rabe_dholmodels_24.pdf

16. Ranalter, D., Brown, C.E., Kaliszyk, C.: Experiments with choice in dependently-typed higher-order logic. In: Bjørner, N.S., Heule, M., Voronkov, A. (eds.) Proceedings 25th International Conference on Logic for Programming, Artificial Intelligence and Reasoning. EPiC Series in Computing, vol. 100, pp. 311–320. EasyChair (2024). https://doi.org/10.29007/2V8H

17. Rothgang, C., Rabe, F., Benzmüller, C.: Theorem proving in dependently-typed higher-order logic. In: Pientka, B., Tinelli, C. (eds.) Automated Deduction. LNAI, vol. 14132, pp. 438–455. Springer, Cham (2023). https://doi.org/10.1007/978-3-031-38499-8_25

18. Rothgang, C., Rabe, F., Benzmüller, C.: Dependently-typed higher-order logic – extended preprint (2025). https://doi.org/10.48550/arXiv.2305.15382, under review

19. Rushby, J., Owre, S., Shankar, N.: Subtypes for specifications: predicate subtyping in PVS. IEEE Trans. Softw. Eng. 24(9), 709–720 (1998). https://doi.org/10.1109/32.713327

20. Steen, A., Benzmüller, C.: Extensional higher-order paramodulation in Leo-III. J. Autom. Reason. 65(6), 775–807 (2021). https://doi.org/10.1007/s10817-021-09588-x

21. Steen, A., Fuenmayor, D., Gleißner, T., Sutcliffe, G., Benzmüller, C.: Automated reasoning in non-classical logics in the TPTP world. In: Konev, B., Schon, C., Steen, A. (eds.) Proceedings of the 8th Workshop on Practical Aspects of Automated Reasoning. CEUR Workshop Proceedings, vol. 3201. CEUR-WS.org (2022). https://ceur-ws.org/Vol-3201/paper11.pdf

22. Stump, A., Sutcliffe, G., Tinelli, C.: StarExec: a cross-community infrastructure for logic solving. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS (LNAI), vol. 8562, pp. 367–373. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08587-6_28

23. Sutcliffe, G.: System description: SystemOnTPTP. In: McAllester, D. (ed.) CADE 2000. LNCS (LNAI), vol. 1831, pp. 406–410. Springer, Heidelberg (2000). https://doi.org/10.1007/10721959_31
24. Sutcliffe, G.: The SZS ontologies for automated reasoning software. In: Sutcliffe, G., Rudnicki, P., Schmidt, R., Konev, B., Schulz, S. (eds.) Proceedings of the LPAR Workshops: Knowledge Exchange: Automated Provers and Proof Assistants, and the 7th International Workshop on the Implementation of Logics, no. 418, pp. 38–49. CEUR Workshop Proceedings (2008)

25. Sutcliffe, G.: The TPTP problem library and associated infrastructure. The FOF and CNF parts, v3.5.0. J. Autom. Reason. **43**(4), 337–362 (2009)

26. Sutcliffe, G.: The TPTP world – infrastructure for automated reasoning. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 1–12. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-17511-4_1

27. Sutcliffe, G.: The logic languages of the TPTP world. Logic J. IGPL **31**(6), 1153–1169 (2023)

28. Sutcliffe, G., Schulz, S., Claessen, K., Van Gelder, A.: Using the TPTP language for writing derivations and finite interpretations. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 67–81. Springer, Heidelberg (2006). https://doi.org/10.1007/11814771_7

29. Sutcliffe, G., Suttner, C.: Evaluating general purpose automated theorem proving systems. Artif. Intell. **131**(1–2), 39–54 (2001). https://doi.org/10.1016/S0004-3702(01)00113-8

30. Sutcliffe, G.: The CADE ATP system competition - CASC. AI Mag. **37**(2), 99–101 (2016). https://doi.org/10.1609/AIMAG.V37I2.2620

31. Sutcliffe, G.: Stepping stones in the TPTP world. In: Benzmüller, C., Heule, M.J., Schmidt, R.A. (eds.) IJCAR 2024. LNCS, vol. 14739, pp. 30–50. Springer, Cham (2024). https://doi.org/10.1007/978-3-031-63498-7_3

32. Sutcliffe, G., Benzmüller, C.: Automated reasoning in higher-order logic using the TPTP THF infrastructure. J. Autom. Reason. **3**(1), 1–27 (2010). https://doi.org/10.6092/ISSN.1972-5787/1710

33. Sutcliffe, G., Kotelnikov, E.: TFX: the TPTP extended typed first-order form. In: Konev, B., Urban, J., Rümmer, P. (eds.) Proceedings of the 6th Workshop on Practical Aspects of Automated Reasoning. CEUR Workshop Proceedings, vol. 2162, pp. 72–87. CEUR-WS.org (2018). https://ceur-ws.org/Vol-2162/paper-07.pdf

34. Sutcliffe, G., Schulz, S., Claessen, K., Baumgartner, P.: The TPTP typed first-order form with arithmetic. In: Bjørner, N., Voronkov, A. (eds.) LPAR 2012. LNCS, vol. 7180, pp. 406–419. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-28717-6_32

35. Sutcliffe, G., Suttner, C.B.: The TPTP problem library - CNF release v1.2.1. J. Autom. Reason. **21**(2), 177–203 (1998). https://doi.org/10.1023/A:1005806324129

36. Swamy, N., et al.: Dependent types and multi-monadic effects in F*. In: Bodik, R., Majumdar, R. (eds.) Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 256–270 (2016). https://doi.org/10.1145/2837614.2837655

37. The Rocq Development Team: The Rocq reference manual – release 9.0.0 (2024). https://coq.inria.fr/doc/V9.0.0/refman

38. Trybulec, A., Blair, H.: Computer assisted reasoning with MIZAR. In: Joshi, A. (ed.) Proceedings of the 9th International Joint Conference on Artificial Intelligence, pp. 26–28. Morgan Kaufmann (1985)
**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.

<figure><img src="image_56.png" /></figure>
Context-Aware Clause Selection Using
Symbol Name Meanings in Theorem
Proving

Claudia Schon(✉) ID

Trier University of Applied Sciences, Trier, Germany

c.schon@hochschule-trier.de

**Abstract.** When humans evaluate the validity of a logical conclusion, they naturally consider its meaning and its context, allowing them to focus on relevant information and to avoid unnecessary inferences. For example, when asked to prove that all *hammocks* are also *beds*, they will certainly not draw conclusions about *vehicles* or *weapons*. In contrast, automated theorem provers typically do not account for the contextual meaning of a conclusion when selecting inference steps. Existing heuristics for selecting the clause for the next inference step usually ignore the meaning of symbol names, overlooking valuable contextual information. As a result, in the example above, clauses with symbol names such as *weapon* or *vehicle* could well be found in the processed clauses. However, since these clauses are not required for the actual proof, they are not helpful to the prover and tend to distract from the actual proof task. In this paper, we present an approach that uses natural language processing techniques to align the selection of the clause for the next inference step with the meaning of the proof goal. Our implementation and experimental results show that this method not only increases the number of successful proofs but also reduces the number of clauses processed during proof search.

**Keywords:** Commonsense Reasoning · Commonsense Knowledge · Clause Selection

# 1 Introduction

When humans evaluate the validity of a logical conclusion, they naturally consider the context and meaning of the conclusion and avoid irrelevant inferences. This intuitive approach is in line with Daniel Kahneman's model of human cognition based on two systems [13], where system 1 represents fast, instinctive and contextual thinking, while system 2 involves slower, more deliberate and logical reasoning. In the field of automated theorem proving (ATP), current systems such as E [28] and Vampire [23] predominantly use logic-based approaches similar to system 2, usually not using the contextual insights corresponding to system 1.
For example, a human being asked to prove that all *hammocks* are also *beds* will intuitively avoid considering unrelated concepts such as *vehicles* or *weapons*. Conversely, automated theorem provers typically do not consider the contextual relevance of symbol names when selecting inference steps. Existing heuristics focus on syntactic properties without exploiting the semantic content embedded in symbol names, which can lead to the inclusion of irrelevant clauses and an inefficient proof process.

It is a key strength of human reasoning that we are able to combine both intuitive (system 1) and analytical (system 2) processes. It is therefore plausible that automated theorem proving could similarly benefit from integrating these two approaches, using the contextual understanding of system 1 alongside the logical strictness of system 2. Currently, however, the meaning of symbol names, and thus the contextual content of formulae, is not taken into account during proof search in automated reasoning.

To address this gap, we integrate statistical methods from natural language processing into the reasoning process to improve the selection of the clause for the next inference step of a theorem prover. We do this by mapping symbol names to natural language words and representing them as vectors. This allows us to measure the semantic similarity between symbols and the goal of the proof. These similarities are used to derive symbol weights, which guide the selection of the clause for the next inference step in a goal-directed way.

Our approach has been implemented and evaluated using the E theorem prover [28]. Experimental results demonstrate that taking the meaning of symbol names into account enables the prover to find more proofs. In addition, the experiments also show a reduction in the number of clauses processed during proof search, indicating a more focused and efficient proof process. This work highlights the potential of combining logic-based and statistical methods to improve automated reasoning, in line with Kahneman's theory.

The main contributions of this paper are:

- The introduction of a heuristic for determining symbol weights based on similarity to the proof goal. These weights can be used to guide the selection of the clause for the next inference step in automated theorem proving.

- An evaluation of the approach, demonstrating that taking the meaning of symbols names into account enables the prover to find more proofs and to reduce the number of clauses processed during proof search for commonsense reasoning tasks.

The paper is structured as follows: after discussing related work (Sect. 2) and preliminaries (Sect. 3), we describe how to determine symbol weights based on the similarity of the symbol names to the proof goal in Sect. 4. In Sect. 5 we present experimental results of our approach. Finally, we summarize and discuss ideas for future work in Sect. 6. This paper is a revised and extended version of our previous workshop paper [27].
## 2 Related Work

The selection of the clause for the next inference step has a very large influence on the performance of theorem provers. A perfect selection can make a search unnecessary, and a proof can be found directly. Most heuristics for selecting the clause for the next inference step are based on simple counting of symbols and the like [29]. In this way, weights are specified for symbols and then used to determine weights for clauses, which are used to select the clause for the next inference step.

The theorem prover E [28] allows assigning custom weights to individual symbols, enabling fine-grained control over symbol-based heuristics. This can be done by specifying a weight function with $FunWeight^1$. Although this option allows you to set symbol weights, it does not describe how to determine them.

In [5], the selection of symbol weights is investigated. The proposed approach employs a graph neural network to predict symbol weights based on the structure of the clause normal form of the input problem. The system is trained using prior proof successes, and a novel scheme is introduced to balance positive clauses (derived from a proof) and negative clauses (not derived from a proof) during training.

Another approach is to use machine learning to derive new clause selection strategies from successful proofs [6].

The ENIGMA [10–12,32] method represents a key advancement in internal guidance within ATPs by integrating machine learning models directly into the theorem proving process to influence decisions such as clause selection. Utilizing techniques like gradient-boosted trees and recursive neural networks, ENIGMA has significantly enhanced the performance of saturation-based provers like E, particularly in large-theory settings like the Mizar Mathematical Library [4].

To the best of our knowledge, none of the currently used approaches to determining symbol weights take into account the meaning of symbol names.

The problem of premise selection, where relevant formulae for a given proof task have to be selected from a knowledge base, is related to the problem considered in this paper. Especially in the area of large mathematical libraries, there are many approaches to premise selection that rely on machine learning methods [1]. The ATP BOOST method improves premise selection by framing it as a binary classification task and using the XGBoost algorithm. DeepMath [9] uses neural networks for premise selection. It is worth noting that DeepMath does not use manually created features. Another notable technique uses recurrent neural networks to capture dependencies between premises [21]. In addition, the work in [22] applies the transformer architecture to premise selection, achieving superior performance compared to earlier recurrent neural network-based methods. Similarly, the transformer-based Magnushammer [16] shows significant improvements in detection success rates through effective retrieval and ranking of relevant premises.

<footnote n="1">¹ See the manual of E for details: https://wwwlehre.dhbw-stuttgart.de/~sschulz/WORK/E_DOWNLOAD/V_2.4/eprover.pdf.</footnote>
The Semantic Web [24] is one domain where the significance of symbol names has been assessed, revealing that the semantics embedded in the names of IRIs (Internationalized Resource Identifiers) reflect a type of social semantics that aligns with the formal meaning of the referenced resource.

Regarding premise selection in commonsense knowledge bases, there are a few approaches that consider the meaning of symbol names. One such approach is Similarity SInE [8], an extension of SInE selection that uses word embeddings to account for symbol similarity. Similarity SInE ensures that all the formulae selected by SInE are included, and additionally selects formulae for symbols that are similar to those appearing in the goal. Furthermore, [26] introduces a vector-based technique for premise selection which uses a word embedding to vectorize the formulae of a knowledge base and to use vector similarity for selection purposes. The ScVEn [19] selection takes the idea of vectorizing a knowledge base one step further by using a large language model for the vectorization step. These three methods take into account the meaning of the symbol names, but they are not used to select the clause for the next inference step.

We are not aware of any approaches that use the meaning of symbols to select the clause to be used in the next reasoning step.

# 3 Preliminaries

We consider the following first-order logic reasoning task in this paper: given a set of formulae called the knowledge base (KB) and a goal $G$, the task is to show that the KB implies $G$. This can be reduced to showing that the conjunction of KB and $
eg G$ is unsatisfiable. To show the unsatisfiability, usually the conjunction of the KB and the negated goal are transformed into an equisatisfiable clause normal form and a contradiction is inferred from the clause set.

To achieve this contradiction, saturation-based provers organise the execution of their inferences using a given-clause algorithm as shown in Algorithm 1. This algorithm maintains two sets of clauses: The set of processed clauses and the set of unprocessed clauses. Initially, all clauses are added to the set of unprocessed clauses, and the set of processed clauses is empty. In each step, the algorithm selects a so-called given clause from the set of unprocessed clauses, adds it to the set of processed clauses, and then performs all the inferences possible with the given clause and the set of processed clauses. The resulting new clauses are added to the set of unprocessed clauses. This is repeated until either the empty clause is inferred, or the set of unprocessed clauses is empty (or a resource or time limit is reached).

The choice of the given clause (line 10 in Algorithm 1) strongly influences whether and how fast a proof is found. An unskilful choice of given clause can quickly lead to a large number of irrelevant clauses in the set of unprocessed clauses, making it difficult to find a proof. On the other hand, a skilful choice of the given clause can lead to only those inferences being made that are relevant to the proof task, so that a proof can be found directly.

To select the given clause, heuristics are usually used that assign a weight to each clause. The clause with the lowest weight is then selected as the given
**Algorithm 1.** Given Clause Algorithm

Require: Initial set of clauses initial\_clauses

1: processed\_set ← {}

2: unprocessed\_set ← initial\_clauses

3: **while** True **do**

4: if empty\_clause ∈ processed\_set **then**

5: return "Proof Found"

6: **end if**

7: if unprocessed\_set is empty **then**

8: return "No Proof Found"

9: **end if**

10: given\_clause ← select\_clause(unprocessed\_set)

11: remove given\_clause from unprocessed\_set

12: add given\_clause to processed\_set

13: new\_clauses ← generate\_new\_clauses(given\_clause, processed\_set)

14: simplified\_clauses ← simplify\_clauses(new\_clauses)

15: **for** each clause in simplified\_clauses **do**

16: if clause ∉ unprocessed\_set **then**

17: add clause to unprocessed\_set

18: **end if**

19: **end for**

20: **end while**

clause. Common heuristics use the age of the clause (older clauses are favoured and receive a lower weight) or are based on a weighted symbol count. These heuristics are often used in combination. The ratio of clauses selected by age to clauses selected by symbol count is called the pick-given ratio. A well-known ratio is the pick-given ratio of 5, which means that the heuristic selects the clause with the lowest weighted symbol count five times and the oldest clause once and this process is repeated continuously. There are many other heuristics for selecting clauses. See Sect. 2 for some pointers in this regard.

In the following, the set of all predicate and function symbols in a formula F is represented as sym(F). In a slight abuse of notation, we use sym(KB) to denote the set containing all predicate and function symbols occurring in a knowledge base KB. Furthermore, we assume that there are multiple proof tasks to solve for a given knowledge base.

## 3.1 Distributional Semantics

Our approach uses the meaning of the names of the function and predicate symbols. To do this, we rely on the distributional semantics of natural language. This is best explained using Firth's famous statement:

> You shall know a word by the company it keeps. [7]

In other words: If we look at very large texts, we can observe that words that occur in a similar context are similar [18].
One approach in this area are word embeddings [14,15]. These are vector representations of words, usually learned using neural networks on very large amounts of text. For a given set of words $V$, also called a vocabulary, a word embedding is a function, $f: V \to \mathbb{R}^n$, that assigns an $n$-dimensional vector to each word in the vocabulary. Since our approach uses existing word embeddings and does not train new ones, we refrain from going into details on the training process of word embeddings.

It is very interesting that words with similar meanings are mapped to similar vectors. Usually, the similarity of two word vectors is calculated with the help of the cosine similarity.

**Definition 1 (Cosine similarity of two vectors).** Let $u, v \in \mathbb{R}^n$, both non-zero. The cosine similarity of $u$ and $v$ is defined as:

$$cos\_sim(u, v) = \frac{u \cdot v}{||u|| ||v||}$$

The cosine similarity of two vectors $u$ and $v$ takes values between $-1$ and $1$. For exactly opposite vectors the value is $-1$, for orthogonal vectors the value is $0$ and for equal vectors the value $1$. The more similar two vectors are, the greater is their cosine similarity.

In our approach, we use a trained word embedding to determine similarities between the names of symbols in a knowledge base and the proof task. The next section describes how we do this.

# 4 Guiding the Reasoning Process by the Meaning of Symbol Names

Automated theorem provers usually calculate the weight of a clause from the weights of the symbols occurring in the clause. For example, the theorem prover E can be given values for weights for function and predicate symbols. These weights then determine which weights the clauses receive and therefore which clauses are preferred in the reasoning process.

We now present an approach to determine symbol weights, and thus clause weights, that uses the meaning of symbol names. As described above, we assume that there are multiple proof tasks to solve for a given knowledge base. In the following, when we talk about a knowledge base or a goal, we refer to the knowledge base or the goal in this scenario.

Our approach uses a word embedding. It is important that the word embedding fits to the domain of the knowledge base. For example if the knowledge base is Yago [31] it would be suitable to use a word embedding which was learnt on Wikipedia articles. In the following, we refer to the word embedding used, as a function $f: V \to \mathbb{R}^n$, where $V$ is the vocabulary of the word embedding.

Figure 1 shows the first step of our approach, which determines a vector representation for all function and predicate symbols occurring in the knowledge base under consideration. To achieve this, in a first step, all function and predicate
<figure><img src="image_57.png" /><figcaption>**Fig. 1.** Overview of the preprocessing step which determines a vector representation for all function and predicate names occurring in a knowledge base *KB*.</figcaption></figure>

symbols are extracted from the knowledge base resulting in the set $sym(KB)$. Next, during the vector transformation, all extracted symbols $s \in sym(KB)$ are mapped to the vocabulary *V* of a word embedding. This mapping step is typically not trivial and highly depends on the knowledge base in use. One possibility is to build this mapping upon an existing WordNet [17] mapping for the knowledge base. WordNet is an extensive lexical database of the English language, which groups words according to their meaning and forms synonymous groups, called synsets. For example for the knowledge base Adimen SUMO [3] such a WordNet mapping is available. We do not go into detail here and refer the reader to [25] for more information on the mapping process. In the following we assume that this step is possible for all symbols extracted from the knowledge base and that there is a mapping function $map: sym(KB) \to V$ which performs this step. Once a function or predicate symbol $s \in sym(KB)$ has been assigned a word $map(s)$ from the vocabulary of the word embedding used, the vector $v_s = f(map(s))$ corresponding to the word is assigned to the symbol. This vector $v_s$ is used as the vector representation of the symbol *s*. This step only needs to be performed once for a knowledge base. Therefore, it can be considered as a pre-processing step.

Since we assume that for a large number of goals it has to be proven that they are entailed from the same knowledge base, the effort of this preprocessing step is relativized.

Figure 2 provides an overview of the process of proving a goal using the symbol-name heuristic. First, a vector representation of the goal is computed for a given goal *G*. To do this, all function and predicate symbols are extracted from the goal leading to the set $sym(G)$ and mapped to words in the vocabulary of the word embedding used. For this, the above mentioned function *map* is used. It is important to use the same word embedding that was chosen for the knowledge base in the pre-processing step. The next step is to compute the vector representation for the goal: For each symbol $s \in sym(G)$ in the goal, the
vector $v_s$ of the word $map(s)$ is looked up in the word embedding. The vectors of all symbols in $sym(G)$ are summed and divided by the number of symbols in the goal resulting in vector $v_G$:

$$v_G = \frac{\sum_{s \in sym(G)} v_s}{|sym(G)|} \qquad (1)$$

In other words, the vector representation of a goal corresponds to the average of the vector representations of all the symbols in the goal.

In the next step, weights for symbols in the knowledge base are computed based on the vector representations of the function and predicate symbols in the knowledge base and the vector representation of the goal. To compute the weight of a symbol $s \in sym(KB)$, we first compute the similarity of its vector representation $v_s$ and the vector representation of the goal $v_G$. Cosine similarity is used for this. The values of cosine similarity are between -1 and 1. The higher the similarity of the two vectors, the higher the value. In contrast to that, symbol with a low weight are preferred by provers. Therefore, we convert the cosine similarities into weights as follows:

We assume a default weight of 1,000. From this we subtract 1,000 times the cosine similarity. The reason for setting the default weight to 1,000 is that we want to accurately incorporate the cosine similarity between $v_s$ and $v_G$ into the symbol weights. Since the cosine similarity of two vectors ranges from -1 to 1, multiplying this value by 1,000 and subtracting it from the default weight of 1,000 allows us to account for up to three decimal places in the similarity measure. This results in the weight of a symbol $s$ w.r.t. the goal $G$ as

$$weight(s, G) = 1000 - 1000 \cdot \cos\_sim(v_s, v_G) \qquad (2)$$

The weights of the symbols calculated in this way are now passed to the theorem prover together with the proof task. The prover calculates the weights for the clauses from the weights for the symbols and uses them to control the proof process.

# 5 Experimental Results

The introduced approach is implemented<fnref n="2" />. To evaluate the approach, we need a knowledge base with function and predicate symbols that are, or can be, mapped to natural language words. We also need a large number of proof tasks for this knowledge base. Adimen SUMO [3] is a first-order logic ontology based on the Suggested Upper Merged Ontology (SUMO) [20]. Since a mapping to WordNet synsets is available for most of the symbols of Adimen SUMO, this ontology is interesting for our evaluation. For the vectorization we use the pretrained word

<footnote n="2">² Code and all data to redo the experiments can be found in the following repository: https://gitlab.rlp.net/clsc0474908343/symbol_meaning_proof_guidance.</footnote>
<figure><img src="image_58.png" /><figcaption>**Fig. 2.** Overview of the process of proving goal *G* from knowledge base *KB* using the symbol name heuristic. Note that the vector representation of *KB* used here was computed in the preprocessing step depicted in Fig. 1 which determines a vector representation for all function and predicate names occurring in a knowledge base *KB*.</figcaption></figure>

embedding ConceptNet Numberbatch [30] which is well suited for the common-sense area.

The proof tasks considered in the experiments are the Adimen SUMO White-BoxTruthTests [2] which are a collection of automatically generated tests that were used to check and validate the Adimen-SUMO ontology. Each proof task consists of a single formula, the goal, for which it must be shown that it can be inferred from the Adimen SUMO ontology. We randomly choose two disjoint sets of 1,000 of these problems. The first of these two sets will be used to determine the best values for the parameters of the similarity-guided selection of the given clause. This set will be called the *parameter-tuning set*. The second set is disjoint from the *parameter-tuning set* and is used for the actual evaluation. This set will be called the *evaluation set*. As finding the optimal parameter values for the similarity-guided selection of clauses is similar to hyperparameter tuning in machine learning, we use a similar approach. This involves ensuring that the set of problems used for parameter selection is disjoint from the set used for the final evaluation.

The WhiteBoxTruthTests are challenging even for highly optimised theorem provers. In all our experiments, we use the theorem prover E with a timeout of
<table><caption>**Table 1.** Configurations of E considered in the experiments. For example k1000_PG5_aF corresponds to the configuration of using the symbol weights for top 1000 symbols, PickGiven = 5 without the auto parameter</caption><thead><tr><td>Abbreviation</td><td>Description and Example</td></tr></thead><tbody><tr><td>k [Num]</td><td>Uses the symbol weights of the Num symbols most similar to the conjecture. Example: k1000 uses the top 1000 symbols</td></tr><tr><td>PG [Num]</td><td>Sets the Pick Given parameter to Num, i.e., the given clause is selected Num times using similarity-guided symbol weights, after which the oldest clause is selected once. Example: PG5 sets PickGiven to 5</td></tr><tr><td>aT/aF</td><td>Indicates whether the auto parameter is enabled (aT) or not enabled (aF). Example: aT enables the auto parameter</td></tr></tbody></table>

10s. We call it with different combinations of parameters<fnref n="3" />: We use E without any parameters as well as E with the auto parameter which allows E to choose literal selection strategy, clause evaluation heuristic, and term ordering, as well as several instantiations of the SInE algorithm automatically. The SInE algorithm is used to select formulae relevant for a given proof task. For proof tasks such as the Adimen SUMO WhiteBoxTruthTests, a selection such as SInE is usually used, since theorem provers without selection are often overwhelmed by the number and complexity of the formulas in Adimen SUMO. SInE makes the prover potentially incomplete.

Furthermore, E allows to pass weights for symbols. These weights can be used to determine which clause to use as the next given clause. As described above, to evaluate our approach we use a default weight of 1,000 for each symbol and change the weights of the *k* symbols that are most similar to the proof goal as given in Eq. 2. To ensure that the reasoner is refutationally complete, we alternate this given clause selection, guided by symbol weights, with the FIFO strategy, where the oldest clause is selected first. The combination of *N* times symbol weight guided given clause selection followed by a single selection using the FIFO strategy is called *PickGiven* ratio. Table 1 gives an overview of the different prover configurations used in our experiments.

## 5.1 Determination of Parameters on the Parameter-Tuning Set

First, we determine the most suitable parameters for similarity-guided selection of the given clause. To achieve this, we systematically varied the parameters listed in Table 1 and ran E over the 1,000 problems of the *parameter-tuning set* for each of these parameter configurations. We then recorded both the number of proofs found (see Fig. 3) and the average number of clauses processed (see Fig. 4).

<footnote n="3">³ Detailed information on the different parameters used for the theorem prover E can be found in the manual which is available at: https://wwwlehre.dhbw-stuttgart.de/~sschulz/WORK/E_DOWNLOAD/V_2.4/eprover.pdf.</footnote>
<figure><img src="image_59.png" /><figcaption>**Fig. 3.** Number of proofs found by E using different parameter configurations (see Table 1) on the 1,000 randomly selected problems of the *parameter-tuning set*.</figcaption></figure>

Figure 3 shows the number of proofs found for the different E configurations we considered on the *parameter-tuning set*. In the graph, the bars representing the parameter configurations that differ only in whether the **auto** parameter is set or not are always shown directly next to each other. For all parameter configurations, we can see that the variant without the **auto** parameter found more proofs than the variant with the **auto** parameter. Therefore, in our final evaluation, we will not consider the **auto** parameter in combination with the similarity-guided symbol weights. Furthermore, we can see that the number of proofs found differs only slightly for parameter configurations without **auto** parameter. The lowest number of proofs found is 486 for the configuration k2000_PG5_aF, and the highest is 555 for k1500_PG8_aF.

As the aim of the similarity-guided selection of the given clause is to enable goal-oriented reasoning, it is interesting to examine the average number of clauses processed. The smaller the number of processed clauses, the more goal-oriented the proof. Ideally, the number of processed clauses is equal to the number of clauses in the proof, and no unnecessary conclusions have been drawn. Figure 4 shows the average number of clauses processed by the considered parameter configurations for the *parameter-tuning set* of problems. The 328 problems for which all parameter configurations have found a proof are considered here.

We observe that setting the **auto** parameter leads to a significantly higher number of processed clauses. For configurations without the **auto** parameter, the lowest average number of processed clauses (9,949) is obtained for k10_PG8_aF. The configuration k10_PG10_aF yields the highest average number of processed clauses (14,301). Examining Figs. 3 and 4 together, the parameter configurations k1000_PG5_aF and k1500_PG5_aF are also notable, both with 554 proofs found, just below the maximum of 555. The average number of clauses processed for these two configurations is also low at 10,748 and 10,440, respectively.
<figure><img src="image_60.png" /><figcaption>**Fig. 4.** Average number of clauses processed during proof search. Different parameters for E were considered (see Table 1). Problems considered were the 328 problems of the *evaluation set* for which E was able to find a proof with all considered parameter configurations.</figcaption></figure>

The configuration k1500 PG8 aF, with which the highest number of proofs was found, processed an average of 13,657 clauses, placing it at the higher end of the observed range. Based on the values observed on the *parameter-tuning set*, the configurations k1500 PG8 aF, k1000 PG5 aF and k1500 PG5 aF will be examined on the *evaluation set*.

## 5.2 Experiments on the Evaluation Set

We now consider the parameter configurations k1500 PG8 aF, k1000 PG5 aF and k1500 PG5 aF selected on the problems of the *parameter-tuning set* in comparison to the parameter configurations aF and aT, which work without similarity-guided symbol weights. For these experiments, we use the *evaluation set* described above, which consists of 1,000 randomly selected Adimen SUMO WhiteBoxTruthTests and is disjoint from the *parameter-tuning set*.

Figure 5 shows that a higher number of proofs is found using similarity-guided symbol weights than with the parameter configurations not considering symbol meanings: While 376 and 414 proofs were found with configurations aF and aT respectively, a significantly higher number of proofs was found when using similarity-guided symbol weights: 541, 543 and 548. This suggests that the meaning of symbol names is a valuable source of information for the proof process.

As described above, the number of clauses processed is another factor to consider when evaluating our approach. The fewer clauses were processed in constructing a proof, the more targeted the process was. Ideally, only the clauses necessary for the proof would be processed. Figure 6 shows the average number
<figure><img src="image_61.png" /><figcaption>**Fig. 5.** Number of proofs found by E using different parameter configurations on the problems of the *evaluation set*. Parameter configurations selected in the parameter tuning step as well as parameter configurations without similarity-guided symbol weights are considered (see Table 1).</figcaption></figure>

of clauses processed by each parameter configuration during proof search for the problems in the *evaluation set*. In order to make meaningful comparisons, we only consider problems that could be proven using all parameter configurations. We observe that parameter configurations **aF** and **aT**, which do not use similarity-guided symbol weights, processed an average of 17,583 and 14,548 clauses, respectively. By contrast, the configurations using similarity-guided symbol weights processed significantly fewer clauses, with averages of 10,390, 10,364 and 11,514 respectively.

Another interesting observation concerns the number of proofs found. We already observed that with the k1500_PG8_aF configuration, significantly more proofs can be found than with aT (548 proofs versus 414 proofs). However, the proofs found with parameter configuration k1500_PG8_aF are not a superset of those found with aT. There are 275 problems where both configurations find a proof. However, k1500_PG8_aF found a proof for 273 problems for which aT was not able to find a proof. Similarly there were 139 problems where aT found a proof but k1500_PG8_aF was not able to find a proof. These findings suggest that the two configurations explore different parts of the search space and follow divergent reasoning paths. To investigate this further, we compared the sizes of the proofs for the 275 problems, both configurations were able to solve. Figure 7 shows the results. There is no clear indication that one of the configurations leads to shorter proofs. On average, the size of a proof is 30 for k1500_PG8_aF and 29.5 for aT. However, we observe that the two configurations produce proofs
<figure><img src="image_62.png" /><figcaption>**Fig. 6.** Average number of clauses processed during proof search. Parameter configurations selected in the parameter tuning step as well as parameter configurations without similarity-guided symbol weights are considered (see Table 1). Problems considered were the 197 problems of the *evaluation set* for which E was able to find a proof with all considered parameter configurations.</figcaption></figure>

of different sizes for almost all problems. Therefore, they do not find the same proofs. This observation, together with the fact that each configuration solves a substantial number of unique problems indicates that the two configurations result in a different exploration of the search space. This suggests that combining these two configurations could be beneficial. However, as our experiments on the *parameter-tuning set* revealed, simply adding the *auto* parameter to the similarity-guided symbol weights deteriorates the results. Therefore, combining the two approaches will require a different approach.

# 6 Summary and Future Work

In this paper we have developed an approach to clause selection in automated theorem provers that aims to make the selection of the clause for the next inference step more goal-directed. The approach is based on the assumption that symbols in knowledge bases have meaningful names that can be mapped to natural language words. If this assumption is correct, techniques from natural language processing can be used to determine the similarity between the proof goal and the symbols in the knowledge base. These similarities are then used to derive symbol weights that guide the selection of clauses for the next inference step. The approach has been implemented and evaluated using the theorem prover E. Our experimental results show that more proofs can be found using
<figure><img src="image_63.png" /><figcaption>**Fig. 7.** Comparison of proof sizes for the 275 problems of the *evaluation set* which E was able to find a proof with parameter configuration aT and k1500 PG8 aF.</figcaption></figure>

these similarity-guided symbol weights. Furthermore, we observe a reduction in the average number of clauses processed during proof search, indicating a more goal-directed and efficient proof process.

In our experiments, we have observed that the use of similarity-guided symbol weights leads to different proofs being found compared to using the *auto* parameter. This suggests that a combination of the two methods could be promising. In future work, we want to develop approaches for such a combination.

Another promising direction for future work is to evaluate the approach of similarity-guided symbol weights on mathematical problems. To make effective use of symbol similarities in this domain, we plan to employ a word embedding that has been trained specifically on mathematical texts. This would allow us to capture domain-specific semantic relationships between symbols and explore whether semantic guidance can also improve theorem proving in formalized mathematics.

## References

1. Alama, J., Heskes, T., Kühlwein, D., Tsivtsivadze, E., Urban, J.: Premise selection for mathematics by corpus analysis and kernel methods. J. Autom. Reason. **52**(2), 191–213 (2014). https://doi.org/10.1007/S10817-013-9286-5

2. Álvez, J., Hermo, M., Lucio, P., Rigau, G.: Automatic white-box testing of first-order logic ontologies. CoRR abs/1705.10219 (2017). http://arxiv.org/abs/1705.10219
3. Álvez, J., Lucio, P., Rigau, G.: Adimen-sumo: reengineering an ontology for first-order reasoning. Int. J. Semant. Web Inf. Syst. 8, 80–116 (2012)

4. Bancerek, G., et al.: Mizar: state-of-the-art and beyond. In: Kerber, M., Carette, J., Kaliszyk, C., Rabe, F., Sorge, V. (eds.) CICM 2015. LNCS (LNAI), vol. 9150, pp. 261–279. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-20615-8_17

5. Bártek, F., Suda, M.: How much should this symbol weigh? A GNN-advised clause selection. In: Piskac, R., Voronkov, A. (eds.) LPAR 2023: Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Manizales, Colombia, 4-9th June 2023. EPiC Series in Computing, vol. 94, pp. 96–111. EasyChair (2023). https://doi.org/10.29007/5F4R

6. Denzinger, J., Schulz, S.: Learning domain knowledge to improve theorem proving. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS, vol. 1104, pp. 62–76. Springer, Heidelberg (1996). https://doi.org/10.1007/3-540-61511-3_69

7. Firth, J.R.: Papers in Linguistics 1934–1951: Rep. Oxford University Press (1991)

8. Furbach, U., Krämer, T., Schon, C.: Names are not just sound and smoke: word embeddings for axiom selection. In: Fontaine, P. (ed.) CADE 2019. LNCS (LNAI), vol. 11716, pp. 250–268. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-29436-6_15

9. Irving, G., Szegedy, C., Alemi, A.A., Eén, N., Chollet, F., Urban, J.: Deepmath - deep sequence models for premise selection. In: Lee, D.D., Sugiyama, M., von Luxburg, U., Guyon, I., Garnett, R. (eds.) Advances in Neural Information Processing Systems 29: Annual Conference on Neural Information Processing Systems 2016, Barcelona, Spain, pp. 2235–2243 (2016)

10. Jakubův, J., Urban, J.: ENIGMA: efficient learning-based inference guiding machine. In: Geuvers, H., England, M., Hasan, O., Rabe, F., Teschke, O. (eds.) CICM 2017. LNCS (LNAI), vol. 10383, pp. 292–302. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-62075-6_20

11. Jakubův, J., Urban, J.: Enhancing ENIGMA given clause guidance. In: Rabe, F., Farmer, W.M., Passmore, G.O., Youssef, A. (eds.) CICM 2018. LNCS (LNAI), vol. 11006, pp. 118–124. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-96812-4_11

12. Jakubuv, J., Urban, J.: Hammering Mizar by learning clause guidance (short paper). In: Harrison, J., O'Leary, J., Tolmach, A. (eds.) 10th International Conference on Interactive Theorem Proving, ITP 2019, Portland, OR, USA, 9–12 September 2019. LIPIcs, vol. 141, pp. 34:1–34:8. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019). https://doi.org/10.4230/LIPICS.ITP.2019.34

13. Kahneman, D.: Thinking, Fast and Slow. Macmillan (2011)

14. Mikolov, T., Chen, K., Corrado, G., Dean, J.: Efficient estimation of word representations in vector space. CoRR abs/1301.3781 (2013). http://arxiv.org/abs/1301.3781

15. Mikolov, T., Sutskever, I., Chen, K., Corrado, G.S., Dean, J.: Distributed representations of words and phrases and their compositionality. In: NIPS, pp. 3111–3119 (2013)

16. Mikula, M., et al.: Magnushammer: a transformer-based approach to premise selection. CoRR abs/2303.04488 (2023). https://doi.org/10.48550/ARXIV.2303.04488

17. Miller, G.A.: WordNet: a lexical database for English. Commun. ACM 38(11), 39–41 (1995). https://doi.org/10.1145/219717.219748

18. Miller, G.A., Charles, W.G.: Contextual correlates of semantic similarity. Lang. Cogn. Process. 6(1), 1–28 (1991). http://eric.ed.gov/ERICWebPortal/recordDetail?accno=EJ431389
19. Jakobs, O., Schon, C.: Context-specific selection of commonsense knowledge using large language models. In: Hotho, A., Rudolph, S. (eds.) KI 2024. LNCS, vol. 14992, pp. 218–231. Springer, Cham (2024). https://doi.org/10.1007/978-3-031-70893-0_16

20. Pease, A.: Ontology: A Practical Guide. Articulate Software Press, Angwin (2011)

21. Piotrowski, B., Urban, J.: Stateful premise selection by recurrent neural networks. In: Albert, E., Kovács, L. (eds.) LPAR 2020: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Alicante, Spain, 22–27 May 2020. EPiC Series in Computing, vol. 73, pp. 409–422. EasyChair (2020). https://doi.org/10.29007/J5HD

22. Proroković, K., Wand, M., Schmidhuber, J.: Improving stateful premise selection with transformers. In: Kamareddine, F., Sacerdoti Coen, C. (eds.) CICM 2021. LNCS (LNAI), vol. 12833, pp. 84–89. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-81097-9_6

23. Riazanov, A., Voronkov, A.: The design and implementation of VAMPIRE. AI Commun. 15(2-3), 91–110 (2002). http://content.iospress.com/articles/ai-communications/aic259

24. de Rooij, S., Beek, W., Bloem, P., van Harmelen, F., Schlobach, S.: Are names meaningful? Quantifying social meaning on the semantic web. In: Groth, P., et al. (eds.) ISWC 2016. LNCS, vol. 9981, pp. 184–199. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-46523-4_12

25. Schon, C.: Selection strategies for commonsense knowledge (2022). https://doi.org/10.48550/ARXIV.2202.09163

26. Schon, C.: Associative reasoning for commonsense knowledge. In: Seipel, D., Steen, A. (eds.) KI 2023. LNCS, vol. 14236, pp. 170–183. Springer, Cham (2023). https://doi.org/10.1007/978-3-031-42608-7_14

27. Schon, C.: Using the meaning of symbol names to guide first-order logic reasoning. In: Özcep, Ö.L., Rußwinkel, N., Sauerwald, K., Wolter, D. (eds.) Proceedings of the 10th Workshop on Formal and Cognitive Reasoning co-located with the 47th German Conference on Artificial Intelligence (KI 2024), Würzburg, Germany, 23 September 2024. CEUR Workshop Proceedings, vol. 3763, pp. 19–27. CEUR-WS.org (2024). https://ceur-ws.org/Vol-3763/paper2.pdf

28. Schulz, S., Cruanes, S., Vukmirović, P.: Faster, higher, stronger: E 2.3. In: Fontaine, P. (ed.) CADE 2019. LNCS (LNAI), vol. 11716, pp. 495–507. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-29436-6_29

29. Schulz, S., Möhrmann, M.: Performance of clause selection heuristics for saturation-based theorem proving. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS (LNAI), vol. 9706, pp. 330–345. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-40229-1_23

30. Speer, R., Chin, J., Havasi, C.: Conceptnet 5.5: an open multilingual graph of general knowledge. In: AAAI, pp. 4444–4451. AAAI Press (2017)

31. Suchanek, F.M., Kasneci, G., Weikum, G.: YAGO: a large ontology from Wikipedia and WordNet. Web Semant. 6(3), 203–217 (2008). https://doi.org/10.1016/j.websem.2008.06.001

32. Suda, M.: Improving ENIGMA-style clause selection while learning from history. In: Platzer, A., Sutcliffe, G. (eds.) CADE 2021. LNCS (LNAI), vol. 12699, pp. 543–561. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-79876-5_31
**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.

<figure><img src="image_64.png" /></figure>
Specific Reasoning Procedures
# When GNNs Met a Word Equations
## Solver: Learning to Rank Equations

Parosh Aziz Abdulla<fnref n="1" /> ID, Mohamed Faouzi Atig<fnref n="1" />, Julie Cailler<fnref n="3" /> ID,
Chencheng Liang<fnref n="1" />(✉) ID, and Philipp Rümmer<fnref n="1" />,<fnref n="2" />(✉) ID

**Abstract.** Nielsen transformation is a standard approach for solving word equations: by repeatedly splitting equations and applying simplification steps, equations are rewritten until a solution is reached. When solving a conjunction of word equations in this way, the performance of the solver will depend considerably on the order in which equations are processed. In this work, the use of Graph Neural Networks (GNNs) for ranking word equations before and during the solving process is explored. For this, a novel graph-based representation for word equations is presented, preserving global information across conjuncts, enabling the GNN to have a holistic view during ranking. To handle the variable number of conjuncts, three approaches to adapt a multi-classification task to the problem of ranking equations are proposed. The training of the GNN is done with the help of minimum unsatisfiable subsets (MUSes) of word equations. The experimental results show that, compared to state-of-the-art string solvers, the new framework solves more problems in benchmarks where each variable appears at most once in each equation.

**Keywords:** Word equation · Graph neural network · String theory

## 1 Introduction

A *word equation* is an equality between two *strings* that may contain variables representing unknown substrings. Solving a *word equation problem* involves finding assignments to these variables that satisfy the equality. Word equations are crucial in string constraints encountered in program verification tasks, such as validating user inputs, ensuring proper string manipulations, and detecting potential security vulnerabilities like injection attacks. The word equation problem is decidable, as shown by Makanin [33]; while the precise complexity of the problem is still open, it is known to be NP-hard and in PSPACE [38].

Abdulla et al. [11] recently proposed a Nielsen transformation-based algorithm for solving word equation problems [36]. This algorithm solves word equations by recursively applying a set of inference rules to branch and simplify the

<footnote n="1">¹ Uppsala University, Uppsala, Sweden</footnote>

<footnote>chencheng.liang@it.uu.se</footnote>

<footnote n="2">² University of Regensburg, Regensburg, Germany</footnote>

<footnote>ph.r@gmx.net</footnote>

<footnote n="3">³ University of Lorraine, CNRS, Inria, LORIA, Nancy, France</footnote>
problem until a solution is reached, in a tableau-like fashion. When multiple word equations are present, the algorithm must select the equation to process next at each proof step. This selection process is critical and heavily influences the performance of the algorithm, as the unsatisfiability of a set of equations can often be shown by identifying a small unsatisfiable core of equations. At the same time, the search tree can contain infinite branches on which no solutions can be found, so that bad decisions can lead a solver astray. The situation is similar to the case of first-order logic theorem provers, where the choice of clauses to process plays a decisive role in determining efficiency. In the latter context, several deep learning techniques have been introduced to guide theorem provers [10, 16, 17, 27, 44]. However, for word equation problems, the application of learning techniques for selecting equations remains largely unexplored.

In this work, we employ Graph Neural Networks (GNNs) [15] to guide the selection of word equations at each iteration of the algorithm. Our research complements existing techniques for learning branching heuristics in word equation solvers [11]. We refer to the selection step as the *ranking process*. For this, we enhanced the existing algorithm [11] to enable the re-ordering of conjunctive word equations. The extension preserves the soundness and the completeness (for finding solutions) of the algorithm. We refer to this extended algorithm as the *split algorithm* throughout the paper.

The primary challenge in training a deep learning model to guide the ranking process lies in managing a variable number of inputs. In our work, this specifically involves handling a varying number of word equations depending on the input. Unlike with branching heuristics, which have to handle only a fixed and small number of branches (typically 2 to 3), the ranking process must handle a variable number of conjuncts. To address this challenge, we adapt multi-classification models to accommodate inputs of varying sizes using three distinct approaches. Additionally, to effectively train the GNNs, we enhance the graph representations of word equations from [11] by incorporating global term occurrence information.

Our model is trained using data from two sources: (1) Minimal Unsatisfiable Subsets (MUSes) of word equations computed by other solvers, and (2) data extracted by running the split algorithm with non-GNN-based ranking heuristics. MUSes computed by solvers such as Z3 [35] and cvc5 [14] help detect unsatisfiable conjuncts early, enabling prompt termination and improved efficiency. When the split algorithm tackles conjunctive word equations, each ranking decision creates a branch in a decision tree. By extracting the shortest path from this tree, we obtain the most effective sequence of choices, which we then use as training data.

Moreover, we explore seven options that combine the trained model with both random and manually designed heuristics for the ranking process.

We evaluated our framework on artificially generated benchmarks inspired by [20]. The benchmarks are divided into two categories: *linear* and *non-linear*, where linear means that, within a single equation, a variable can occur only once, while non-linear allows a variable to appear multiple times. Note that this definition of linearity applies to individual equations: in systems with multiple equations, even if each equation is linear, shared variables can cause a variable to appear multiple times within the system.
Finally, we compare our framework with several leading SMT solvers and a word equation solver, including Z3, Z3-Noodler [19], cvc5, Ostrich [18], and Woorpje [20]. The experimental results show that for linear problems, our framework outperforms all leading solvers in terms of the number of solved problems. For non-linear problems, when the occurrence frequency of the same variables (non-linearity) is low, our algorithm remains competitive with other solvers.

In summary, the contributions of this paper are as follows: (i) We adapt the Nielsen transformation-based algorithm [11] to allow control over the ordering of word equations at each iteration. (ii) We develop a framework to train and deploy a deep learning model for ranking and ordering conjunctive word equations within the split algorithm. The model leverages MUSes generated by leading solvers and uses graph representations enriched with global information of the formula. We propose three strategies to adapt multi-classification models for ranking tasks and explore various integration methods within the split algorithm. (iii) Experimental results demonstrate that our framework performs effectively on linear problems, with the deep learning model significantly enhancing performance. However, its effectiveness on non-linear problems is constrained by the limitations of the inference rules.

## 2 Preliminaries

We first define the syntax of word equations and the concept of satisfiability. Next, we explain the message-passing mechanism of Graph Neural Networks (GNNs) and describe the specific GNN model employed in our experiments.

**Word Equations.** We assume a finite non-empty alphabet $\Sigma$ and write $\Sigma^*$ for the set of all strings (or words) over $\Sigma$. The empty string is denoted by $\epsilon$. We work with a set $\Gamma$ of string variables, ranging over words in $\Sigma^*$. The symbol $\cdot$ denotes the concatenation of two strings; in our examples, we often write $uv$ as shorthand for $u \cdot v$. The syntax of word equations is defined as follows, where $X \in \Gamma$ ranges over variables and $c \in \Sigma$ over letters:

$$ \text{Formulae } \phi ::= true \mid e \land \phi $$

$$ \text{Words } w ::= \epsilon \mid t \cdot w $$

$$ \text{Equations } e ::= w = w $$

$$ \text{Terms } t ::= X \mid c $$

**Definition 1 (Satisfiability of conjunctive word equations).** A formula $\phi$ is satisfiable (SAT) if there exists a substitution $\pi : \Gamma \to \Sigma^*$ such that, when each variable $X \in \Gamma$ in $\phi$ is replaced by $\pi(X)$, all equations in $\phi$ hold.

**Definition 2 (Linearity of a word equation).** A word equation is called linear if each variable occurs at most once. Otherwise, it is non-linear.

**Graph Neural Networks.** Message Passing-based GNNs (MP-GNNs) [23] are designed to learn features of graph nodes (and potentially the entire graph) by iteratively aggregating and transforming feature information from the neighborhood of a node. Consider a graph $G = (V, E)$, with $V$ as the set of nodes and
$E \subseteq V \times V$ as the set of edges. Each node $v \in V$ has an initial representation $x_v \in \mathbb{R}^n$ and a set of neighbors $N_v \subseteq V$. In an MP-GNN comprising $T$ message-passing steps, node representations are iteratively updated. The initial node representation of $v$ at time step 0 is $H_v^0 = x_v$. At each step $t$, the representation of node $v$, denoted as $H_v^t$, is updated using the equation:

$$H_v^t = \eta_t(\rho_t(\{H_u^{t-1} | u \in N_v\}), H_v^{t-1}), \quad (1)$$

where $H_u^{t-1}$ is the node representation of $u$ in the previous iteration $t-1$, and node $u$ is a neighbor of node $v$. In this context, $\rho_t : (\mathbb{R}^n)^{|N_v|} \to \mathbb{R}^n$ is an aggregation function with trainable parameters (e.g., an MLP followed by sum, mean, min, or max) that aggregates the node representations of $v$'s neighboring nodes at the $t$-th iteration. Along with this, $\eta_t : (\mathbb{R}^n)^2 \to \mathbb{R}^n$ is an update function with trainable parameters (e.g., an MLP) that takes the aggregated node representation from $\rho_t$ and the node representation of $v$ in the previous iteration as input, and outputs the node representation of $v$ at the $t$-th iteration.

In this study, we employ Graph Convolutional Networks (GCNs) [29] to guide our algorithm due to their computational efficiency to generalize across tasks without the need for task-specific architectural modifications. In GCNs, the node representation $H_v^t$ of $v$ at step $t \in \{1, ..., T\}$ where $T \in \mathbb{N}$ is computed by

$$H_v^t = \text{ReLU}(\text{MLP}^t(\text{mean}\{H_u^{t-1} | u \in N_v \cup \{v\}\})), \quad (2)$$

where each MLP$^t$ is a fully connected neural network, ReLU (Rectified Linear Unit) [13] is the non-linear function $f(x) = max(0, x)$, and $H_v^0 = x_v$.

## 3 Split Algorithm with Ranking

**Split Algorithm.** Algorithm 1, SPLITEQUATIONS, determines the satisfiability of a word equation formula $\phi$ by recursively applying inference rules from [11].

The algorithm begins by checking the satisfiability of the conjunctive formula (Line 2). If all word equations can be eliminated in this way, then $\phi$ is SAT. If any conjunct is unsatisfiable (UNSAT), then $\phi$ is UNSAT. Otherwise, the satisfiability status remains unknown (UKN). If $\phi$ is in one of the first two cases, its status is returned (Line 3).

Otherwise (Line 4), RANKEQS orders all conjuncts using either manually designed or data-driven methods. Next, the function APPLYRULES matches and applies the corresponding inference rules to generate branches—alternative prospective solving paths for the same equation. This step is called the *branching process*. Notably, rules $R_7$ and $R_8$ generate two and three branches, respectively, while all the other rules do not cause any branching.

Next, the SPLITEQUATIONS call (Line 9) recursively checks the satisfiability of each branch. Let $\{b_1, ..., b_n\}$ be the set of branches. The formula $\phi$ has status SAT if at least one branch $b_i$ is satisfiable, UNSAT if all branches are unsatisfiable, and UKN otherwise.
**Data:** A formula $\phi$

**Result:** The satisfiability status of $\phi$ (i.e., *SAT*, *UNSAT*, or *UKN*) and the simplified version of $\phi$

1. **begin**
2. &nbsp;&nbsp;&nbsp;&nbsp;`res ← CHECKFORMULASATISFIABILITY(φ)`
3. &nbsp;&nbsp;&nbsp;&nbsp;`if res ≠ UKN then return res, φ`
4. &nbsp;&nbsp;&nbsp;&nbsp;**else**
5. &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;`φs = RANKEQS(φ)` // Ranking process
6. &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;`Branches = APPLYRULES(φs)` // Branching process
7. &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;`uknFlag ← 0`
8. &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**for** `b in Branches**do**
9. &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;`resb, φb=SPLITEQUATIONS(b)`
10. &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;`if resb = SAT then return SAT, φb`
11. &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;`if resb = UKN then uknFlag ← 1`
12. &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;`if uknFlag = 1 then return UKN, φ`
13. &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**else** return UNSAT, $\phi$

<caption>**Algorithm 1:** SPLITEQUATIONS algorithm.</caption>

Since the inference rules apply to the leftmost equation, the performance of the algorithm is strongly influenced by both the order in which branches are processed (Line 8) and the ordering of equations in $\phi$ (Line 5). While the impact of branch ordering has been studied in [11], this paper explores whether employing a data-driven heuristic in RANKEQS can enhance termination.

The baseline option to implement RANKEQS is referred to as **RE1: Baseline**. It computes the priority of a word equation $p$ using the following definition:

$$p = \begin{cases} 1 & \text{if } \epsilon = \epsilon \\ 2 & \text{otherwise, if } \epsilon = u \cdot v \text{ or } u \cdot v = \epsilon \\ 3 & \text{otherwise, if } a \cdot u = b \cdot v \text{ or } u \cdot a = v \cdot b \\ 4 & \text{otherwise, if } a \cdot u = a \cdot v \\ 5 & \text{otherwise} \end{cases}$$

where $a, b \in \Sigma$, and $u, v$ are sequences of variables and letters. Smaller numbers indicate higher priority, assigning greater precedence to simpler cases where satisfiability is obvious. Word equations with the same priorities between 1 and 4 are further ordered by their length (i.e., the number of terms), with shorter equations taking precedence. For word equations with a priority of 5, the original input order is maintained. The newly created equations inherit the ranking of their parents. We refer to the split algorithm using **RE1** for RANKEQS as **DragonLi**. The correctness of Algorithm 1 follows directly from the soundness and local completeness of the inference rules in [11]:

**Lemma 1 (Soundness of Algorithm 1).** For a conjunctive word equation formula $\phi$, if Algorithm 1 terminates with the result *SAT* or *UNSAT*, then $\phi$ is *SAT* or *UNSAT*, respectively.
**AND-OR Tree.** The search tree explored by the algorithm can be represented as an AND-OR tree, as shown in Fig. 1. The example illustrates the three paths, each placing different equations in the first position, generated by the ranking and branching process to solve the word equation $\phi = (Xb = bXX \land \epsilon = \epsilon \land X = a)$, where $a, b \in \Sigma$ and $X \in \Gamma$.

*Example 1.* In the first step, $\phi$ can be reordered in three distinct ways by prioritizing one conjunct to occupy the leftmost position (we ignore the order of the rest two equations, as their order does not influence the next rule application). Thus, the root of the tree branches into three paths. For each ranked formula, the inference rules are then applied to execute the branching process. By iterating these two steps alternately, the complete AND-OR tree is constructed. Notably, continuously selecting the leftmost branch that prioritizes $Xb = bXX$ at the root and applying the left branch of $R_7$ may lead to non-termination, as the length of the word equation keeps increasing. In contrast, prioritizing $X = a$ at the root results in a solution (UNSAT) at a relatively shallow depth, avoiding the risk of non-termination caused by further ranking and branching. In this case, exploring only a single branch during the ranking process suffices to determine the satisfiability of $\phi$. This optimal path is highlighted with solid edges.

<figure><img src="image_65.png" /><figcaption>**Fig. 1.** AND-OR tree resulting from the word equation $Xb = bXX \land \epsilon = \epsilon \land X = a$. The formulas enclosed in boxes are generated by RANKEQS, while the formulas without boxes are obtained from APPLYRULES.</figcaption></figure>

# 4 Guiding the Split Algorithm

This section details the training and application of a GNN model in Algorithm 1. We first describe the process of collecting training data, followed by the graph-based representation of each word equation. Next, we outline three model structures for ranking a set of word equations. Finally, we discuss methods for integrating the trained model back into the algorithm.