## 4.1 Training Data Collection

Assume that $\phi$ is an unsatisfiable conjunctive word equation consisting of a set of conjuncts $\mathcal{E}$.

**Definition 3 (Minimal Unsatisfiable Set).** A subset $U \subseteq \mathcal{E}$ is a Minimal Unsatisfiable Set (MUS) if the conjunction of $U$ is unsatisfiable, and for all conjuncts $e \in U$, the conjunction of subset $U \setminus \{e\}$ is satisfiable.

We collect training data from two sources: (1) MUSes extracted by other solvers, including Z3, Z3-Noodler, cvc5, and Ostrich; and (2) formulas from the ranking process that lie on the shortest path from the subtree leading to UNSAT in the AND-OR trees. A numerical example of these two sources is provided in Sect. 5.2.

For training data from source (1), we first pass all problems to DragonLi. Next, we identify unsolvable problems and forward them to other solvers. If any solver successfully solves a problem, we select the one that finds a solution in the shortest time. This solver is then used to extract the MUS by exhaustively checking the satisfiability of all subsets of the conjuncts. Finally, each conjunct within a set of word equations is labeled based on its membership in the MUS and its length.

Formally, given a formula $\phi = e_1 \wedge \dots \wedge e_n$, its conjuncts are denoted $\mathcal{E} = \{e_1, \dots, e_n\}$, and an MUS $U \subseteq \mathcal{E}$. The corresponding labels of $e_i \in \mathcal{E}$ are $Y_n = \{y_1, \dots, y_n\}$, where $y_i \in \{0, 1\}$, and their length is denoted $|e_i|$. The label $y_i$ is computed as follows:

$$ y_i = \begin{cases} 1 & \text{if } e_i \in U \text{ and } |e_i| = \min(\{|e_i| \mid e_i \in U\}), \\ 0 & \text{otherwise.} \end{cases} \qquad (3) $$

We assign label 1 only to the shortest equation in the MUS, rather than labeling all MUS equations as 1 and non-MUS equations as 0, because the algorithm selects only one equation to proceed at each iteration. Our goal is to identify the most efficient choice. We assume that the shortest equation in the MUS is more likely to lead to quicker termination, as the branching process aims to reduce equation length until a form is reached where satisfiability (or unsatisfiability) can be easily concluded.

To collect training data from source (2), we pass the problems, along with the MUS extracted from other solvers, to DragonLi. If DragonLi solves the problem, multiple paths to UNSAT are generated by sequentially prioritizing each equation at the leftmost position in the ranked word equation.

Subsequently, we export and label each conjunctive word equation along the shortest path in the subtree leading to UNSAT. Formally, given a set of conjuncts $\mathcal{E} = \{e_1, \dots, e_n\}$ of a conjunctive word equation, the corresponding labels $Y_n = (y_1, \dots, y_n)$ are computed by

$$ y_i = \begin{cases} 1 & \text{if } e_i \text{ in the shortest path of a subtree leading to UNSAT,} \\ 0 & \text{otherwise.} \end{cases} \qquad (4) $$
<figure><img src="image_66.png" /><figcaption>**Fig. 2.** The steps for constructing graph representation for the conjunctive word equations $XaX = Y \land aaa = XaY$ where X, Y are variables and a is a letter.</figcaption></figure>

For both sources, when $\sum_{i=1}^{n} y_i > 1$, we keep the first equation with label 1 and discard the rest equations with label 1 to ensure $\sum_{i=1}^{n} y_i = 1$. When $\sum_{i=1}^{n} y_i = 0$, we discard this training data due to no positive label.

## 4.2 Graph Representation for Conjunctive Word Equations

The graph representation of a single word equation is discussed in [11]. However, since word equations are interconnected through shared variables, ranking them requires not only local information about individual equations but also a global perspective. By considering the entire set of word equations collectively, we can incorporate dependencies and shared structures, improving the ranking process.

To achieve this, we first represent each conjunctive word equation independently. Then, we compute the occurrences of variables and letters across all equations and integrate this global information into each individual graph representation. This enriched representation captures both the complexity of individual equations and their interactions within the system.

In details, the graph representation of a word equation is defined as $G = (V, E, v_=, V_T, V_{Var}, V_T^0, V_T^1, V_{Var}^0, V_{Var}^1)$, where V is the set of nodes, $E \subseteq V \times V$ is the set of edges, and $v_= \in V$ is a special node representing the “=” symbol. The sets $V_T \subseteq V$ and $V_{Var} \subseteq V$ contain letter and variable nodes, respectively. Additionally, $V_T^0$ and $V_T^1$ are special nodes representing letter occurrences and $V_{Var}^0$ and $V_{Var}^1$ analogously represent variable occurrences.

Figure 2 illustrates the two steps involved in constructing the graph representation of the conjunctive word equations $XaX = Y \land aaa = XaY$, where $\{X, Y\} \subseteq \Gamma$ and $a \in \Sigma$:

- **Step 1:** Inspired by Abstract Syntax Trees (ASTs), we begin to build the graph by placing the “=” symbol as the root node. The left and right children of the root represent the leftmost terms of each side of the equation, respectively. Subsequent terms are organized as singly linked lists of nodes.
- **Step 2:** Calculate the number of occurrences of all terms across the conjunctive word equations. In this example, Occurrence($X$) = 3, Occurrence($Y$) = 2, and Occurrence($a$) = 5. Their binary encodings are 11, 10 and 101 respectively. We encode these as sequentially connected nodes: ($V_{Var}^1, V_{Var}^1$) for $X$, ($V_{Var}^1, V_{Var}^0$) for $Y$, and ($V_T^1, V_T^0, V_T^1$) for $a$. Finally, we connect the roots of these nodes to their corresponding variable and letter nodes.

We chose binary encoding because using unary encoding would significantly increase the graph size, making computation inefficient. Higher-base encodings like ternary or decimal tend to blur structural distinctions, i.e., different values may be represented using the same number of nodes, making it hard for the graph structure to reflect meaningful differences. Binary encoding strikes a balance. It keeps the graph size manageable while preserving enough structural information for our GNN to effectively process word equations at the scale we target.

The rationale behind our other choices of graph representation for word equations, along with a discussion of alternative representations, is provided in the repository [2].

## 4.3 Training of Graph Neural Networks

In the function RANKEQS of Algorithm 1, equations can be ranked and sorted based on predicted rank scores from a trained model. Given a conjunctive word equation $\phi = e_1 \wedge \dots \wedge e_n$, the model outputs a ranking, i.e., a list of real numbers $\hat{Y}_n = (\hat{y}_1, \dots, \hat{y}_n)$ in which a higher value indicates a higher rank. For example, for a conjunctive word equation $e_1 \wedge e_2$, the model might output $\hat{Y}_2 = (0.3, 0.7)$, indicating that $e_2$ is expected to lead to a solution more quickly than $e_1$, and the equations should be reordered as $e_2 \wedge e_1$.

**Forward Propagation.** To compute this ranking, we first transform the word equations $\{e_1, \dots, e_n\}$ to their graph representations $G = \{G_1, \dots, G_n\}$ where $G_i = (V, E, v_-, V_T, V_{Var}, V_T^0, V_T^1, V_{Var}^0, V_{Var}^1)$. Each node $v \in V$ is first assigned an integer representing the node type: $v \in \bigcup \{V_T, V_{Var}, V_T^0, V_T^1, V_{Var}^0, V_{Var}^1\} \cup \{v_-=\}$. Those integers are then passed to a trainable embedding function $MLP_0: \mathbb{Z} \to \mathbb{R}^m$ to compute all the initial node representations $H_i^0$ in $G_i$.

Equation (2) defines how node representations are updated. By iterating this update rule, we obtain the node representations $H_i^t = \text{GCN}(H_i^{t-1}, E)$ for $t \in \{1, \dots, T\}$, where the relation $E$ is used to identify neighbors. Subsequently, the representation of the entire graph is obtained by summing the node representations at time step $T$, resulting in $H_{G_i} = \frac{1}{n} \sum_{i=1}^n H_i^T$.
Then, we introduce three ways to compute the $\hat{Y}_n$:

- **Task 1:** Each graph representation $H_{G_i}$ is given to a trainable classifier $MLP_1: \mathbb{R}^m \to \mathbb{R}^2$, which outputs $\mathbf{z}_i = \text{MLP}_1(H_{G_i}) = (z_1, z_2)$. The score for graph $i$ is then computed as $y_i = \text{softmax}(\mathbf{z}_i)_1$ for $y_i \in \hat{Y}_n$ where $\text{softmax}(\mathbf{z}_i) = (\frac{e^{z_1}}{\sum_{j=1}^n e^{z_j}}, \dots, \frac{e^{z_n}}{\sum_{j=1}^n e^{z_j}})$ and $\text{softmax}(\cdot)_1$ is the first element of $\text{softmax}(\cdot)$. It represents the probability of the class in the first index.
- **Task 2:** All graph representations in a conjunctive word equations are first aggregated by $H_G = \frac{1}{n} \sum_{i=1}^{n} H_{G_i}$. Then, we compute the score by of each graph by $y_i = softmax(MLP_2(H_{G_i}||H_G))_1$ for $y_i \in \hat{Y}_n$ where $MLP_2: \mathbb{R}^{2m} \rightarrow \mathbb{R}^2$ is a trainable classifier and $||$ denotes concatenation of two vectors.

- **Task 3:** We begin by fixing a limit $n$ of equation within a conjunctive word equation. For conjunctive word equations containing more than $n$ word equations, we first sort them by length (in ascending order) and then trim the list to $n$ equations. Next, we compute scores for resulting equations using $\hat{Y}_n = MLP_3(H_{G_1},...,H_{G_n})$ where $MLP_3: \mathbb{R}^{nm} \rightarrow \mathbb{R}^n$ is a trainable classifier. Scores for any trimmed word equations are set to 0. If a conjunctive word equations contains fewer than $n$ word equations, we fill the list with empty equations to reach $n$, and then compute $\hat{Y}_n$ in the same way.

**Backward Propagation.** The trainable parameters of the model include the weights of the embedding function $MLP_0$, the classifiers $MLP_1$, $MLP_2$, $MLP_3$, and the GCNs. Those trainable parameters are optimized together by minimizing the categorical cross-entropy loss between the predicted label $\hat{y}_i \in \hat{Y}_n$ and the true label $y_i \in Y_n$, using the equation $loss = -\frac{1}{n} \sum_{i=1}^{n} y_i \log(\hat{y}_i)$ where $n$ is the number of conjuncts in the conjunctive word equations.

## 4.4 Ranking Options

In Algorithm 1, we introduce seven implementations of RANKEQS, aimed at evaluating the efficiency of deterministic versus stochastic ranking methods.

- **RE1, Baseline:** A baseline defined in Sect. 3.

- **RE2, Random: RE1** is first used to compute the priority of each word equation, and then equations with a priority of 5 are randomly ordered. This approach aims to add some randomness to the baseline.

- **RE3, GNN:** Equations ranked at 5 by **RE1** are then ranked and sorted using the GNN model. While this option incurs higher overhead due to frequent use of the GNN model, it provides the most fine-grained guidance.

- **RE4, GNN-Random:** Based on **RE3**, there is a 50% chance of invoking the GNN model and a 50% chance of randomly sorting word equations with a priority of 5. This option provides insight into the performance when introducing a random process into GNN-based ranking.

- **RE5, GNN-one-shot:** Based on the priority assigned by **RE1**, the GNN model is used to rank and sort equations with a priority of 5 the first time they occur, while it is managed by **RE1** in subsequent iterations. This option invokes the GNN only once to minimize its overhead, while still maintaining its influence on subsequent iterations. Ranking and sorting the word equations early in the process has a greater impact on performance than doing them later.

- **RE6, GNN-each-n-iteration:** Based on **RE3**, instead of calling the GNN model each time multiple word equations have priority 5, it is invoked only every $n = 5000$ calls to the RANKEQS function. This option explores a balance between **RE3** and **RE5**.
- **RE7, GNN-formula-length:** Based on RE3, instead of calling the GNN model each time multiple word equations have priority 5, it is invoked only after $n = 1000$ calls to the RANKEQS function when the length of the current word equation does not decrease. This option introduces dynamic control over calling the GNN model.

# 5 Experimental Results

This section describes the benchmarks and the methods used for training data collection. We also compare our evaluation data with leading solvers. The training and prediction workflow can be found in the repository [5].

## 5.1 Benchmarks

We initially transformed real-world benchmarks from the non-incremental QF_S, QF_SLIA, and QF_SNLIA tracks of the SMT-LIB benchmark suite [6], as well as those from the Zaligvinder benchmark suite [7], into word equation problems by removing length constraints, boolean operators, and regular expressions. However, these transformed problems were overly simplistic, as most solvers, including DragonLi, solved them easily. Consequently, we shifted to evaluating solvers using artificially generated word equation problems inspired by prior research [11,20]. We summarize the benchmarks as follows:

- **Benchmark A1:** Given a finite set of letters $T$ and a set of variables $V$, the process begins by generating individual word equations of the form $s = s$, where $s$ is a string composed of randomly selected letters from $T$. The maximum length of $s$ is capped at 60. Next, substrings in $s$ on both sides of the equation are replaced $n$ times with the concatenation of $m$ fresh variables from $V$. Here $|T| = 6$, $|V| = 10$, $n \in [0, 5]$, and $m \in [1, 5]$. Finally, multiple such word equations are conjoined to form a conjunctive word equation problem. The number of equations to be conjoined is randomly selected between 1 and 100. Since each replacement variable is a fresh variable from $V$, individual equations in the problem remain linear.

- **Benchmark A2:** This benchmark is generated using the same method as Benchmark A1; however, different parameters are employed to increase the difficulty while ensuring that the problem remains linear. Specifically, we use $|T| = 26$, $|V| = 100$, $n \in [0, 16]$, and $m = 1$.

- **Benchmark B:** This benchmark is generated by the same method as Benchmark A1, except it does not use fresh variables to replace substrings in $s$. This causes a single variable to potentially occur multiple times in an equation, making the problem non-linear. The number of equations to be conjoined is randomly picked between 2 and 50, and the maximum length of $s$ is capped at 50. In this benchmark, we use $|T| = 10$, $|V| = 10$, $n \in [0, 5]$, and $m = 1$.
- **Benchmark C:** We first generate a word equation in the following format:

$$X_n a X_n b X_{n-1} \cdots b X_1 = a X_n X_{n-1} X_{n-1} b \cdots X_1 X_1 b a a$$

where $X_1, ..., X_n$ are variables and $a$ and $b$ are letters. Then, we replace each $b$ with one side of an individual equation generated by Benchmark A1. Finally, we join the individual equations to form a conjunctive word equation problem, with the maximum number of conjuncts capped at 100. This method ensures that the resulting benchmark is highly non-linear.

The statistics of the evaluation data for benchmarks is shown in the repository [3].

## 5.2 Training Data Collection

Table 1 outlines the training data collection. We generate 60,000 problems per benchmark and check their satisfiability with DragonLi. For instance, Benchmark A1 contains 1,859 unsolved problems, which are then passed to solvers such as Z3, Z3-Noodler, cvc5, and Ostrich. Together, these solvers identify 181 SAT and 1,678 UNSAT problems, with no single tool able to solve them all.

For UNSAT problems, we extract Minimal Unsatisfiable Subsets (MUSes) using the fastest solver. This yields 909 problems with extractable MUSes, as detailed in the repository [4]. We rank word equations within each problem based on their presence in the MUS and their length, then pass the ranked problems back to DragonLi. This allows DragonLi to prioritize word equations appearing in the MUS, enabling it to solve 518 new problems. Problems in the row *Have MUS* are transformed into a single labeled data (a conjunctive word equation). Problems in the row *DragonLi* using MUS are transformed into multiple labeled data, each representing a ranking process step on the shortest path to the solution.

The ranking heuristic's effectiveness varies with problem benchmarks. For Benchmarks A1 and A2, 57% to 58% of problems with MUSes are solved. In Benchmark B, the success rate drops to 20%, while for Benchmark C, the heuristic has no effect, solving 0 additional problems. Consequently, no training data or model was generated for Benchmark C.

## 6 Experimental Settings

To better investigate the influence of conjuncts order at a conjunctive word equations, we fixed the branch order for all inference rules. Additionally, we fixed the inference rule to the prefix version, meaning it always simplifies the word equation starting from the leftmost term.

Benchmarks were split uniformly into training, validation, and test sets, following standard deep-learning practice. We save the model from the epoch with the highest validation accuracy.
<table><caption>**Table 1.** Number of problems solved by different solvers and having extracted MUS. The row *Other solvers* shows the number of solved problem in total by Z3, Z3-Noodler, cvc5, and Ostrich where ✓, ×, and ∞ denotes SAT, UNSAT, and UKN respectively. The row *DragonLi* using MUS is the number of problems solved by *DragonLi* when using MUS to rank word equations in the first iteration.</caption><thead><tr><th>Type</th><th colspan="2">Linear</th><th colspan="4">Non-linear</th></tr><tr><th>Bench</th><th>A1</th><th>A2</th><th colspan="2">B</th><th colspan="2">C</th></tr><tr><th>Total</th><td>60000</td><td>60000</td><td colspan="2">60000</td><td colspan="2">60000</td></tr></thead><tbody><tr><th rowspan="2">DragonLi</th><td>Solved</td><td>∞</td><td>Solved</td><td>∞</td><td>Solved</td><td>∞</td></tr><tr><td>58141</td><td>1859</td><td>50610</td><td>9390</td><td>52056</td><td>7944</td></tr><tr><th>Other solvers</th><td>✓ ×</td><td>✓ ×</td><td>✓ ×</td><td>✓ ×</td><td>✓ ×</td><td>✓ ×</td></tr><tr><th>Have MUS</th><td>181 1678</td><td>667 4167</td><td>640 7304</td><td>383 58259</td><td>15875</td><td></td></tr><tr><th>DragonLi using MUS</th><td>518</td><td>594</td><td>607</td><td>0</td><td></td><td></td></tr></tbody></table>

All training records and corresponding hyperparameters, such as a hidden layer size of 128 for all neural networks and number of message passing rounds are available in our repository [8]. For example, the experimental results for Benchmark A and Task 2 can be found in [1].

Each problem in the benchmarks is evaluated on a computer equipped with two Intel Xeon E5 2630 v4 at 2.20 GHz/core and 128GB memory. The GNNs are trained on NVIDIA A100 GPUs. We measured the number of solved problems and the average solving time (in seconds), with timeout of 300s for each proof attempt.

## 6.1 Comparison with Other Solvers

Table 2 compares the results of three RANKEQS options, **RE1**, **RE2**, and **RE5** (corresponding to *DragonLi*, *Random-DragonLi*, and *GNN-DragonLi*), against five solvers: Z3 [35], Z3-Noodler [19], cvc5 [14], Ostrich [18], and Woopje [20].

The primary metric is the number of solved problems. In Benchmark A1, GNN-DragonLi achieves the best performance for both SAT and UNSAT problems. For Benchmark A2, GNN-DragonLi solves the most problems overall (895 problems solved), despite not being the best in either category individually. GNN-DragonLi outperforms both *DragonLi* and *Random-DragonLi*, showing the effectiveness of data-driven heuristics over fixed and random heuristics.

As problem non-linearity increases (in Benchmark B), some solvers outperform all *DragonLi* options. For highly non-linear problems (Benchmark C), *DragonLi* solves almost no problems, regardless of the options. This is an effect entirely orthogonal to the ranking problem, however: for non-linear equations, substituting variables that appear multiple times can increase equation length, resulting in mostly infinite branches in the search tree. It then becomes more important
<table><caption>**Table 2.** Number of problems, average solving time, and average split counts for solvers across four benchmarks. The GNN model used in this table is trained on Task 2. Columns “UNI”, “CS”, and “CU” indicate uniquely solved, common SAT, and common UNSAT problems, respectively. The “-” denotes unavailable data. Each benchmark consists of 1000 problems.</caption><thead><tr><th rowspan="2">Bench</th><th rowspan="2">Solver</th><th colspan="4">Number of solved problems</th><th colspan="4">Average solving time<br>(split number)</th></tr><tr><th>SAT</th><th>UNSAT</th><th>UNICS</th><th>CU</th><th>SAT</th><th>UNSAT</th><th>CS</th><th>CU</th></tr></thead><tbody><tr><td rowspan="10">A1</td><td>DragonLi</td><td>24</td><td>955</td><td>0</td><td></td><td>5.6<br>(244.8)</td><td>6.5<br>(1085.3)</td><td>5.0<br>(94.4)</td><td>5.7<br>(126.3)</td></tr><tr><td>Random-<br>DragonLi</td><td>22</td><td>944</td><td>0</td><td></td><td>5.6<br>(198.8)</td><td>6.3<br>(932.6)</td><td>5.6<br>(137.6)</td><td>5.7<br>(180.5)</td></tr><tr><td>GNN-<br>DragonLi</td><td>24</td><td>961</td><td>0</td><td>13</td><td>6.1<br>(164.7)</td><td>7.5<br>(1974.8)</td><td>6.1<br>(96.4)</td><td>6.3<br>(60.5)</td></tr><tr><td>cvc5</td><td>24</td><td>952</td><td>1</td><td></td><td>0.5</td><td>0.6</td><td>0.1</td><td>0.3</td></tr><tr><td>Z3</td><td>17</td><td>960</td><td>0</td><td></td><td>8.7</td><td>0.4</td><td>1.1</td><td>0.1</td></tr><tr><td>Z3-Noodler</td><td>22</td><td>939</td><td>2</td><td></td><td>5.7</td><td>0.3</td><td>4.8</td><td>0.1</td></tr><tr><td>Ostrich</td><td>17</td><td>931</td><td>0</td><td></td><td>15.0</td><td>5.5</td><td>8.0</td><td>4.7</td></tr><tr><td>Woorpje</td><td>23</td><td>744</td><td>0</td><td></td><td>3.0</td><td>12.5</td><td>0.1</td><td>12.2</td></tr><tr><td>DragonLi</td><td>59</td><td>824</td><td>0</td><td></td><td>8.5<br>(4233.4)</td><td>11.8<br>(1231.3)</td><td>4.7<br>(27.3)</td><td>-</td></tr><tr><td>Random-<br>DragonLi</td><td>44</td><td>806</td><td>1</td><td>3</td><td>24.7<br>(29779.6)</td><td>6.2<br>(210.9)</td><td>4.6<br>(27.3)</td><td>-</td></tr><tr><td rowspan="10">A2</td><td>GNN-<br>DragonLi</td><td>59</td><td>836</td><td>4</td><td></td><td>8.4<br>(1330.6)</td><td>11.6<br>(1074.1)</td><td>5.9<br>(27.3)</td><td>-</td></tr><tr><td>cvc5</td><td>67</td><td>142</td><td>15</td><td></td><td>0.6</td><td>56.0</td><td>0.1</td><td>-</td></tr><tr><td>Z3</td><td>8</td><td>870</td><td>10</td><td></td><td>1.1</td><td>0.6</td><td>0.1</td><td>-</td></tr><tr><td>Z3-Noodler</td><td>22</td><td>7</td><td>1</td><td></td><td>15.4</td><td>3.8</td><td>0.4</td><td>-</td></tr><tr><td>Ostrich</td><td>13</td><td>18</td><td>2</td><td></td><td>24.8</td><td>38.8</td><td>8.6</td><td>-</td></tr><tr><td>Woorpje</td><td>0</td><td>0</td><td>0</td><td>-</td><td>-</td><td>-</td><td>-</td><td>-</td></tr><tr><td>DragonLi</td><td>11</td><td>805</td><td>0</td><td></td><td>4.9<br>(62.5)</td><td>5.2<br>(81.5)</td><td>4.9<br>(29.2)</td><td>5.3<br>(82.4)</td></tr><tr><td>Random-<br>DragonLi</td><td>10</td><td>894</td><td>0</td><td></td><td>5.0<br>(58.7)</td><td>5.8<br>(295.2)</td><td>5.0<br>(27.25)</td><td>5.2<br>(73.1)</td></tr><tr><td rowspan="10">B</td><td>GNN-<br>DragonLi</td><td>11</td><td>821</td><td>0</td><td>4</td><td>6.5<br>(65.1)</td><td>6.8<br>(70.0)</td><td>6.5<br>(28.25)</td><td>6.8<br>(60.2)</td></tr><tr><td>cvc5</td><td>12</td><td>915</td><td>0</td><td></td><td>0.1</td><td>0.6</td><td>0.1</td><td>0.7</td></tr><tr><td>Z3</td><td>11</td><td>859</td><td>3</td><td></td><td>0.1</td><td>0.2</td><td>0.1</td><td>0.1</td></tr><tr><td>Z3-Noodler</td><td>24</td><td>911</td><td>1</td><td></td><td>4.9</td><td>0.4</td><td>1.3</td><td>0.4</td></tr><tr><td>Ostrich</td><td>12</td><td>917</td><td>2</td><td></td><td>6.9</td><td>3.7</td><td>3.3</td><td>4.2</td></tr><tr><td>Woorpje</td><td>19</td><td>330</td><td>1</td><td></td><td>29.5</td><td>6.0</td><td>0.2</td><td>5.0</td></tr><tr><td>DragonLi</td><td>2</td><td>0</td><td>0</td><td>-</td><td>5.1<br>(85.5)</td><td>-</td><td>-</td><td>-</td></tr><tr><td>Random-<br>DragonLi</td><td>2</td><td>0</td><td>0</td><td>-</td><td>5.0<br>(85.5)</td><td>-</td><td>-</td><td>-</td></tr><tr><td rowspan="10">C</td><td>GNN-<br>DragonLi</td><td>-</td><td>-</td><td>-</td><td>-</td><td>-</td><td>-</td><td>-</td><td>-</td></tr><tr><td>cvc5</td><td>0</td><td>909</td><td>17</td><td>-</td><td>-</td><td>46.9</td><td>-</td><td>17.3</td></tr><tr><td>Z3</td><td>1</td><td>821</td><td>12</td><td>1</td><td>0.8</td><td>1.7</td><td>0.8</td><td>0.1</td></tr><tr><td>Z3-Noodler</td><td>7</td><td>657</td><td>4</td><td>1</td><td>0.2</td><td>94.1</td><td>0.1</td><td>1.0</td></tr><tr><td>Ostrich</td><td>0</td><td>61</td><td>0</td><td>-</td><td>-</td><td>77.2</td><td>-</td><td>27.1</td></tr><tr><td>Woorpje</td><td>3</td><td>62</td><td>0</td><td>1</td><td>65.0</td><td>28.4</td><td>0.2</td><td>223.1</td></tr></tbody></table>

to implement additional criteria to detect unsatisfiable equations, for instance in terms of word length or letter count (e.g., [30]), which are present in other solvers. DragonLi deliberately does not include such optimizations, as we aim at investigating the ranking problem in a controlled setting.

For commonly solved problems, the average solving time provides sufficient data only for Benchmarks A1 and B (678 and 294 problems, respectively). In these cases, DragonLi shows no time advantage, partly due to its implementation in Python. Re-implementing the algorithm in a more efficient language, such as Rust [9], can yield over a 100x speedup for single word equation problems.
We also measure the average number of splits in solved problems to evaluate ranking efficiency. GNN-DragonLi demonstrates fewer average splits compared to other options, indicating higher problem-solving efficiency in Benchmarks A1 and B. Our results can be summarized as follows:

1. For linear problems, all DragonLi ranking options perform competitively, with GNN-DragonLi solving the highest number of problems.

2. For moderately non-linear problems (Benchmark B), DragonLi shows moderate performance, but the ranking heuristic offers limited benefits to GNN-DragonLi, leading to reduced performance compared to other options.

3. For highly non-linear problems (Benchmark C), DragonLi fails to solve most problems due to limitations in its calculus.

4. The current implementation of DragonLi offers no time advantage for commonly solved problems, though significant improvements are achievable by reimplementation.

Increasing training data for Benchmark A2 from 20,000 to 60,000 allowed GNN-DragonLi to solve additional problems, suggesting that larger training sets may enhance performance. An ablation study on alternative RANKEQS options is provided as an appendix in the repository [2]. All benchmarks, evaluation results, and implementation details, including hyperparameters, are available in our GitHub repository [8].

# 7 Related Work

Axel Thue [39] laid the theoretical foundation of word equations by studying the combinatorics of words and sequences, providing an initial understanding of repetitive patterns. The first deterministic algorithm to solve word equations was proposed by Makanin [33], but the complexity is non-elementary. Plandowski [38] designed an algorithm that reduces the complexity to PSPACE by using a form of run-length encoding to represent strings and variables more compactly during the solving process. Artur Jeż [28] proposed a nondeterministic algorithm that runs in $O(n \log n)$ space. Closer to our approach, recent research has focused on improving the practical efficiency of solving word equations. Perrin and Pin [37] offered an automata-based technique that represents equations in terms of states and transitions. This allows the automata to capture the behavior of strings satisfying the equation. Markus et al. [22] explored graph representations and graph traversal methods to optimize the solving process for word equations, while Day et al. [20] reformulated the word equation problem as a reachability problem for nondeterministic finite automata, then encoded it as a propositional satisfiability problem that can be handled by SAT solvers. Day et al. [21] proposed a transformation system that extends the Nielsen transformation [31] to work with linear length constraints.

Deep learning [24] has been integrated with various formal verification techniques, such as scheduling SMT solvers [26], loop invariant reasoning [42, 43], and guiding premise selection for Automated Theorem Provers (ATPs) [27, 45].
Closely related work in learning from Minimal Unsatisfiable Subsets (MUSes) includes NeuroSAT [40,41], which utilizes GNNs to predict the probability of variables appearing in unsat cores, guiding variable branching decisions for Conflict-Driven Clause Learning (CDCL) [34]. Additionally, some recent works [12,32] explore learning MUSes to guide CHC [25] solvers.

# 8 Conclusion and Future Work

In this work, we extend a Nielsen transformation based algorithm [11] to support the ranking of conjunctive word equations. We adapt a multi-classification task to handle a variable number of inputs in three different ways in the ranking task. The model is trained using MUSes to guide the algorithm in solving UNSAT problems more efficiently. To capture global information in conjunctive word equations, we propose a novel graph representation for word equations. Additionally, we explore various options for integrating the trained model into the algorithms. Experimental results show that, for linear benchmarks, our framework outperforms the listed leading solvers. However, for non-linear problems, its advantages diminish due to the inherent limitations of the inference rules. Our framework not only offers a method for ranking word equations but also provides a generalized approach that can be extended to a wide range of formula ranking problems which plays a critical role is symbolic reasoning.

As future work, we aim to optimize GNN overhead, integrate GNN guidance for both branching and ranking, and extend the solver to support length constraints and regular expressions for greater real-world applicability. Our framework can be generalized to handle more decision processes in symbolic methods that take symbolic expressions as input and output a decision choices.

**Acknowledgement.** The computations were enabled by resources provided by the National Academic Infrastructure for Supercomputing in Sweden (NAISS) at Chalmers Centre for Computational Science and Engineering (C3SE) and Uppsala Multidisciplinary Center for Advanced Computational Science (UPPMAX) partially funded by the Swedish Research Council through grant agreement no. 2022-06725. The research was also partially supported by the Swedish Research Council through grant agreement no. 2021-06327, by a Microsoft Research PhD grant, and the Wallenberg project UPDATE.

**Disclosure of Interests.** The authors have no competing interests to declare that are relevant to the content of this article.

# References

1. DragonLi solver experimental report for benchmark a and task 2. https://github.com/ChenchengLiang/DragonLi/tree/rank/experimental_results_tables/eval_data_GNN/A1/task_2/model. Accessed 16 May 2025

2. Github repository for the ablation study. https://github.com/ChenchengLiang/DragonLi/blob/rank/Appendix/Ablation-study.md. Accessed 30 June 2025
3. Github repository for the statistics of evaluation data. https://github.com/ChenchengLiang/DragonLi/blob/rank/Appendix/Statistics-of-evaluation-data.
   md. Accessed 30 June 2025

4. Github repository for the statistics of muse. https://github.com/ChenchengLiang/DragonLi/blob/rank/Appendix/Statistics-of-MUSes.md. Accessed 30 June 2025

5. Github repository for the workflow. https://github.com/ChenchengLiang/DragonLi/blob/rank/Appendix/Workflow.md. Accessed 30 June 2025

6. The satisfiability modulo theories library (SMT-LIB). https://smtlib.cs.uiowa.edu/benchmarks.shtml. Accessed 16 May 2025

7. Zaligvinder: A string solving benchmark framework. https://zaligvinder.github.io.
   Accessed 16 May 2025

8. DragonLi github repository branch:rank (2025). https://github.com/ChenchengLiang/boosting-string-equation-solving-by-GNNs/tree/rank. Accessed 16 May 2025

9. wordeq solver (2025). https://github.com/tage64/wordeq solver. Accessed 16 May 2025

10. Abdelaziz, I., et al.: Learning to guide a saturation-based theorem prover (2021).
   https://arxiv.org/abs/2106.03906

11. Abdulla, P.A., Atig, M.F., Cailler, J., Liang, C., Rümmer, P.: Guiding word equation solving using graph neural networks. In: Akshay, S., Niemetz, A., Sankaranarayanan, S. (eds.) Automated Technology for Verification and Analysis, pp. 279–301. Springer, Cham (2025)

12. Abdulla, P.A., Liang, C., Rümmer, P.: Boosting constrained Horn solving by unsat core learning. In: Dimitrova, R., Lahav, O., Wolff, S. (eds.) Verification, Model Checking, and Abstract Interpretation, pp. 280–302. Springer, Cham (2024)

13. Agarap, A.F.: Deep Learning using Rectified Linear Units (ReLU) arXiv:1803.08375 (2018). https://doi.org/10.48550/arXiv.1803.08375

14. Barbosa, H., et al.: cvc5: a versatile and industrial-strength SMT solver. In: Fisman, D., Rosu, G. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, pp. 415–442. Springer, Cham (2022)

15. Battaglia, P.W., et al.: Relational inductive biases, deep learning, and graph networks. CoRR abs/1806.01261 (2018). http://arxiv.org/abs/1806.01261

16. Bártek, F., Suda, M.: Neural precedence recommender. In: Platzer, A., Sutcliffe, G. (eds.) CADE 2021. LNCS (LNAI), vol. 12699, pp. 525–542. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-79876-5_30

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

18. Chen, T., Hague, M., Lin, A.W., Rümmer, P., Wu, Z.: Decision procedures for path feasibility of string-manipulating programs with complex operations. Proc. ACM Program. Lang. 3(POPL), 49:1–49:30 (2019). https://doi.org/10.1145/3290362

19. Chen, Y.F., Chocholatý, D., Havlena, V., Holík, L., Lengál, O., Síč, J.: Z3-noodler: an automata-based string solver. In: Finkbeiner, B., Kovács, L. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, pp. 24–33. Springer, Cham (2024). https://doi.org/10.1007/978-3-031-57246-3_2

20. Day, J.D., Ehlers, T., Kulczynski, M., Manea, F., Nowotka, D., Poulsen, D.B.: On solving word equations using SAT. In: Filiot, E., Jungers, R., Potapov, I. (eds.) RP 2019. LNCS, vol. 11674, pp. 93–106. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-30806-3_8
21. Day, J.D., Kulczynski, M., Manea, F., Nowotka, D., Poulsen, D.B.: Rule-based word equation solving. In: Proceedings of the 8th International Conference on Formal Methods in Software Engineering, FormalISE 2020, pp. 87–97. Association for Computing Machinery, New York (2020). https://doi.org/10.1145/3372020.3391556

22. Diekert, V., Lohrey, M.: Word equations over graph products. In: Pandya, P.K., Radhakrishnan, J. (eds.) FSTTCS 2003. LNCS, vol. 2914, pp. 156–167. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-540-24597-1_14

23. Gilmer, J., Schoenholz, S.S., Riley, P.F., Vinyals, O., Dahl, G.E.: Neural message passing for quantum chemistry. CoRR abs/1704.01212 (2017). http://arxiv.org/abs/1704.01212

24. Goodfellow, I.J., Bengio, Y., Courville, A.: Deep Learning. MIT Press, Cambridge (2016). http://www.deeplearningbook.org

25. Horn, A.: On sentences which are true of direct unions of algebras. J. Symb. Log. **16**(1), 14–21 (1951). https://doi.org/10.2307/2268661

26. Hůla, J., Mojžíšek, D., Janota, M.: Graph neural networks for scheduling of SMT solvers. In: 2021 IEEE 33rd International Conference on Tools with Artificial Intelligence (ICTAI), pp. 447–451 (2021). https://doi.org/10.1109/ICTAI52525.2021.00072

27. Jakubův, J., Chvalovský, K., Olšák, M., Piotrowski, B., Suda, M., Urban, J.: ENIGMA anonymous: symbol-independent inference guiding machine (system description). In: Peltier, N., Sofronie-Stokkermans, V. (eds.) IJCAR 2020. LNCS (LNAI), vol. 12167, pp. 448–463. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-51054-1_29

28. Jež, A.: Recompression: a simple and powerful technique for word equations (2014). https://arxiv.org/abs/1203.3705

29. Kipf, T.N., Welling, M.: Semi-supervised classification with graph convolutional networks. In: 5th International Conference on Learning Representations, ICLR 2017, Toulon, France, 24–26 April 2017, Conference Track Proceedings. OpenReview.net (2017). https://openreview.net/forum?id=SJU4ayYgl

30. Kumar, A., Manolios, P.: Mathematical programming modulo strings. In: Formal Methods in Computer Aided Design, FMCAD 2021, New Haven, CT, USA, 19–22 October 2021, pp. 261–270. IEEE (2021). https://doi.org/10.34727/2021/ISBN.978-3-85448-046-4_36

31. Levi, F.W.: On semigroups. Bull. Calcutta Math. Soc. **36**(141–146), 82 (1944)

32. Liang, C., Rümmer, P., Brockschmidt, M.: Exploring representation of horn clauses using GNNs. In: Konev, B., Schon, C., Steen, A. (eds.) Proceedings of the Workshop on Practical Aspects of Automated Reasoning Co-located with the 11th International Joint Conference on Automated Reasoning (FLoC/IJCAR 2022), Haifa, Israel, 11–12 August 2022. CEUR Workshop Proceedings, vol. 3201. CEUR-WS.org (2022). https://ceur-ws.org/Vol-3201/paper7.pdf

33. Makanin, G.S.: The problem of solvability of equations in a free semigroup. Math. Sb. (N.S.) **103**(145)(2(6)), 147–236 (1977)

34. Marques-Silva, J., Sakallah, K.A.: Grasp: a search algorithm for propositional satisfiability. IEEE Trans. Comput. **48**, 506–521 (1999). https://api.semanticscholar.org/CorpusID:13039801

35. de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78800-3_24
36. Nielsen, J.: Die Isomorphismen der allgemeinen, unendlichen Gruppe mit zwei Erzeugenden. Mathematische Annalen **78**, 385–397 (1917). https://api.semanticscholar.org/CorpusID:119726936

37. Pin, J.E., Perrin, D.: Infinite Words: Automata, Semigroups, Logic and Games. Elsevier (2004). https://hal.science/hal-00112831

38. Plandowski, W.: Satisfiability of word equations with constants is in PSPACE. In: 40th Annual Symposium on Foundations of Computer Science (Cat. No. 99CB37039), pp. 495–500 (1999). https://doi.org/10.1109/SFFCS.1999.814622

39. Power, J.F.: Thue’s 1914 paper: a translation. CoRR abs/1308.5858 (2013). http://arxiv.org/abs/1308.5858

40. Selsam, D., Bjørner, N.: Neurocore: guiding high-performance SAT solvers with unsat-core predictions. CoRR abs/1903.04671 (2019)

41. Selsam, D., Lamm, M., Bünz, B., Liang, P., de Moura, L., Dill, D.L.: Learning a SAT solver from single-bit supervision. In: 7th International Conference on Learning Representations, ICLR 2019, New Orleans, LA, USA, 6–9 May 2019. OpenReview.net (2019). https://openreview.net/forum?id=HJMC_iA5tm

42. Si, X., Dai, H., Raghothaman, M., Naik, M., Song, L.: Learning loop invariants for program verification. In: Bengio, S., Wallach, H., Larochelle, H., Grauman, K., Cesa-Bianchi, N., Garnett, R. (eds.) Advances in Neural Information Processing Systems, vol. 31. Curran Associates, Inc. (2018)

43. Si, X., Naik, A., Dai, H., Naik, M., Song, L.: Code2Inv: a deep learning framework for program verification. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12225, pp. 151–164. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-53291-8_9

44. 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

45. Wang, M., Tang, Y., Wang, J., Deng, J.: Premise selection for theorem proving by deep graph embedding. In: Proceedings of the 31st International Conference on Neural Information Processing Systems, NIPS 2017, pp. 2783–2793. Curran Associates Inc., Red Hook (2017)

**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_67.png" /></figure>
# A Finite Abstraction of Real-Valued Functions for Complete Reasoning About Influence

Sören Möller¹(✉) , Florian Bruse²(✉) , and Martin Lange¹(✉)

¹ Theoretical Computer Science/Formal Methods, University of Kassel, Kassel, Germany

soeren.moeller@uni-kassel.de

² TUM School of Computation, Information and Technology, Technical University of Munich, Munich, Germany

**Abstract.** We consider the reasoning problem of logical consequence between simple statements about the behaviour of continuous functions on certain intervals, representing the way that variables influence each other. Automated reasoning for such statements has applications in formal modelling of classroom experiments in natural sciences. A previous attempt, employing a simple proof system for this reasoning task, is known to be incomplete and unlikely to be extendable to obtain completeness for arbitrary experiments. Here we develop an algebraic approach in the form of an abstraction of the uncountable space of finite collections of continuous, real-valued functions, connected by a composition principle, into finitely many representatives of equivalence classes. We show that this is sufficient for the reasoning task at hand. The approach achieves completeness under very reasonable restrictions of the involved statements, extending what has previously been achieved using proof-theoretic means, and yields an upper bound of coNP.

**Keywords:** formal modelling · hybrid systems · formal reasoning · completeness

## 1 Introduction

Formal reasoning forms the basis for automated solutions to many decision problems [9,14], especially when they can be seen as instances of classic logical problems like validity or logical consequence: given a set of formulas $Ψ$ and a single formula $ϕ$, is it the case that $Ψ \models \varphi$, i.e. do all models of $Ψ$ also satisfy $ϕ$? Calculi and algorithms are continuously developed for formal reasoning tasks involving various kinds of logics from general purpose ones like First-Order Logic [15], Higher-Order Logic [1], etc. to specific-purpose ones like program logics [8], description logics [2], temporal logics [7], etc.

Here we are concerned with automated reasoning for logical consequence in a very specific and very simple logic that makes assertions about particular hybrid systems. These comprise collections of continuous, real-valued functions, each of
which is associated with a pair of elements of an underlying finite, partial order of so-called *variables*. A function $F_{a,b}: \mathbb{R} \to \mathbb{R}$, associated with the variable-pair $(a, b)$, models dynamic behaviour. However, this does not necessarily model the evolution of some value over time (as it is the case in e.g. hybrid automata [10]), but it models the dependency of $b$-values on $a$-values where $a$ and $b$ are arbitrary variables. Thus, it models the way that variable *a* *influences* variable *b*. Influence as an abstract concept between a discrete set of variables can naturally form a partial order, in particular it should clearly be transitive: if altitude (Alt) influences air pressure (AP) and air pressure influences oxygen saturation (Ox) then Alt also influences Ox. In particular, $F_{Alt,Ox}$ is determined by $F_{Alt,AP}$ and $F_{AP,Ox}$, imposing constraints on valid combinations of functions and excluding arbitrary collections. The valid collections are called *experiments* for reasons to become clear below when we discuss the motivation for this reasoning task.

Anti-symmetry of influence – the inability of two variables to mutually influ-
ence each other – is arguably not such a natural requirement. For instance,
pressure, temperature and volume of a gas all influence each other mutually.
We impose anti-symmetry as a technical requirement, restricting the domain of
application slightly but not unreasonably. This restriction is needed to obtain a
decision procedure for the reasoning problem under consideration.

The “formulas” of the logic under consideration here are simple atomic statements about observable, abstract behaviour of influence on certain intervals, e.g. “*air pressure decreases steadily from 1bar to 0.8bar at altitudes between 0 m and 2000 m*”. A set of such statements is called a *scheme*, and it describes valid influence behaviour between the underlying variables, formally described as the satisfaction of such statements by an experiment in the sense above. The reasoning problem we study then is: given such a scheme *C* and another statement *H*, called the *hypothesis*, does *C* *|=* *H* hold?

The motivation for this study stems from a particular application, namely the intention to digitalise classroom experiments in natural sciences, in particular biology. As part of standard high school curricula to instigate scientific reasoning, students devise experiments and hypotheses and test them empirically. Virtualisation of this process has advantages [11,17], e.g. by extending the range of experiments that can be done in classrooms, perhaps involving dangerous substances or those of limited accessibility, infeasible time scales, etc. This requires sound, complete and efficient automated reasoning techniques, though.

The use of a formal system from logic or computer science for formal mod-
elling of biological processes is not new (cf. [3, 16, 18]), not even w.r.t. the special
aspect of variable influence [6]. Our work here combines not only aspects of for-
mal modelling and biological systems but also demands imposed by didactics.
The reason for studying simple statements only, for example, is their potential
use in a suitable learning tool that cannot require 8th graders for instance to
possess knowledge in formal logic.

The first approach at providing automated support for the problem of log-
ical consequence between schemes and hypotheses was a proof-theoretic one,
called the *Calculus of Influence* (CoI) [5]. It tries to capture the relation ‘|=’ by
a finite set of proof rules. This is sound and polynomial-time computable, but
unfortunately complete only for very restricted forms of partial orders of the
underyling variable set. In this paper we present an algebraic approach based on
an abstraction of the uncountably many experiments described by schemes into
finitely many representatives of equivalence classes. This abstraction is faithful
w.r.t. logical consequence, leading to a reasoning algorithm that achieves com-
pleteness without restrictions on the underlying partial orders.

The paper is organised as follows. In Sect. 2 we introduce the involved concepts like experiments, schemes, consequence etc. formally. In Sect. 3 we intuitively develop an equivalence relation on experiments that possesses the properties mentioned above, which opens up the path for an algorithmic approach to the consequence relation between schemes and hypotheses. In Sect. 4 we develop this approach for flat partial orders, i.e. those in which transitivity plays no role. This is simply done to separate the technical developments into two steps, first focussing on the discretisation of continuous functions. This is then lifted in Sect. 5 to non-flat orders, there focussing on the issues arising with function composition. We conclude in Sect. 6 with remarks on further work in this area. Technical proofs have been moved to the appendix for space considerations.

## 2 Preliminaries

*Influences and Influence Experiments.* Let $\mathcal{V} = \{a, b, \dots\}$ be a finite set of variables ordered by some partial order $\leq$. For a variable $a \in \mathcal{V}$, Post$(a) := \{b \in \mathcal{V} \mid a < b$ and there is no $b' \in \mathcal{V}$ s.t. $a < b' < b\}$ are all its successors. The set of predecessors, denoted by Pre$(a)$, is defined analogously. An interval is a $[x, y] \subseteq \mathbb{R}$ such that $x \leq y$ as usual.

An influence is a continuous function $f : \mathbb{R} \to \mathbb{R}$ with domain $dom(f) = [x, y]$ for some $x, y \in \mathbb{Q}$. For $x \notin dom(f)$, we define $f(x) = \perp$. Furthermore, we assume that $\perp$ is absorbing under composition, i.e. $f(g(x)) = \perp$ whenever $g(x) = \perp$ for all $x \in \mathbb{R}$.

The behaviour of an influence on a (sub-)domain $[x, y] \subseteq dom(f)$ is monotonic ($\nearrow$) if $f(z) \leq f(z')$, antitonic ($\nwarrow$) if $f(z) \geq f(z')$, constant ($\to$) if $f(z) = f(z')$ for all $x \leq z \leq z' \leq y$, and arbitrary ($\rightsquigarrow$) otherwise.

Behaviours are naturally ordered: $\to$ is a special case of $\nearrow$ and of $\nwarrow$, and these are special cases of $\rightsquigarrow$ in turn. We use $q \prec q'$ to indicate that $q$ is a special case of $q'$. We write $f|_{[x,y]} \preceq q$ with $q \in \{\nearrow, \nwarrow, \to, \rightsquigarrow\}$ to indicate that $f$ exhibits behaviour $q$ on $[x,y]$, and $f|_{[x,y]} = q$ if $f|_{[x,y]} \preceq q$ and $f|_{[x,y]} \not\preceq q'$ for any $q' \prec q$.

The range of an influence $f$ on $[x, y]$ is $rang_{[x,y]}(f) = \{f(z) \mid x \leq z \leq y\}$.

**Definition 1.** A $\mathcal{V}$-influence experiment $\mathcal{F}$ is a collection of influences $\mathcal{F}_{a,b}$ for each pair of variables $a, b \in \mathcal{V}$ such that $a < b$. Moreover, $\mathcal{F}$ must satisfy the coherence property: for all $a, b, c \in \mathcal{V}$ with $a < b < c$ and all $x \in \mathbb{R}$, we have $(\mathcal{F}_{b,c} \circ \mathcal{F}_{a,b})(x) = \mathcal{F}_{a,c}(x)$.

*Example 1.* The $\mathcal{V}$-influence experiment $\mathcal{F}$ illustrated in Fig. 1 depicts the relationships between the variables *Altitude* (Alt) in meters, *Air Pressure* (AP) in kPa, and *Oxygen* (Ox) in percent, using orange lines to indicate the influences
<figure><img src="image_68.png" /><figcaption>**Fig. 1.** Example of an experiment (orange), scheme (grey), and hypothesis (red). (Color figure online)</figcaption></figure>

between them. Specifically, $\mathcal{F}$ captures the influences of altitude on air pressure and air pressure on oxygen levels. We obtain the influence of altitude on oxygen levels via the coherence property, i.e. $\mathcal{F}_{Alt,Ox} = \mathcal{F}_{Alt,AP} \circ \mathcal{F}_{AP,Ox}$.

*Statements and Influence Schemes.* Let $\mathcal{V}$ be as above. A $\mathcal{V}$-statement is a 5-tuple $S = (a, [x, y], q, [l, u], b)$, typically written as $a \xrightarrow{[x,y]q[l,u]} b$, where $a, b \in \mathcal{V}$ are variables s.t. $a < b$, $\text{dom}(S) = [x, y]$ is the statements's domain, $\text{rang}(S) = [l, u]$ is the statements range, and $q \in \{\uparrow, \downarrow, \rightarrow\}$ is the statements' behaviour. It abstractly describes the gradient of influences as functions on the domain as mapping into the range either monotonically ($\uparrow$), antitонically ($\downarrow$) or in a constant fashion $\rightarrow$. The behaviour $\rightsquigarrow$ is disallowed in such statements. Intuitively, the statement $S$ asserts that the influence $\mathcal{F}_{a,b}$ of a $\mathcal{V}$-influence experiment $\mathcal{F}$ is defined on $\text{dom}(S)$, must only take values in $\text{rang}(S)$ on that domain, and behaves just as $q$ asserts.

More formally, influence $f$ satisfies $S$, written $f \models S$, if

- $[x, y] \subseteq \text{dom}(f)$,

- $\text{rang}(f) \subseteq [l, u]$, and

- $f|_{[x,y]} \preceq q$.

**Definition 2.** A $\mathcal{V}$-(influence) scheme $\mathcal{C}$ is a finite set of $\mathcal{V}$-statements. For a scheme $\mathcal{C}$ and $a, b \in \mathcal{V}$, let $\mathcal{C}_{a,b} := \{S \mid S = a \xrightarrow{IqI'} b \in \mathcal{C} \text{ for some } I, q, I'\}$.

We lift the semantics of a single statement to the semantics of an influence scheme. Given a $\mathcal{V}$-influence scheme $\mathcal{C}$ and a $\mathcal{V}$-influence experiment $\mathcal{F}$, we say that $\mathcal{F}$ satisfies $\mathcal{C}$, written $\mathcal{F} \models \mathcal{C}$, if $\mathcal{F}_{a,b} \models S$ for all $S = a \xrightarrow{IqI'} b \in \mathcal{C}$.

*Example 2.* Figure 1 depicts, besides a particular $\mathcal{V}$-influence experiment $\mathcal{F}$ using orange lines as described in Example 1, a $\mathcal{V}$-influence scheme $\mathcal{C}$. Each statement $a \xrightarrow{[x,y]q[l,u]} b \in \mathcal{C}$ is represented by a grey rectangle spanning from $(x, l)$ to $(y, u)$ in the corresponding influence diagram with variable names $a$ and $b$, and behaviour $q$ is indicated by the label inside the rectangle.

Using this visual interpretation, we can verify that $\mathcal{F} \models \mathcal{C}$ holds by inspecting the diagram for each pair of variables (Alt, AP), (AP, Ox), and (Alt, Ox). We
confirm that, for each of these, the corresponding influence is defined on all relevant domains, only takes values within the rectangles, and behaves as indicated by the labels inside the rectangles.

*Hypothesis Validation.* We aim to validate hypotheses such as “does the oxygen level decrease to levels of 10% to 30% at altitudes between 6 and 8 km?” relative to the theory of behaviour of variables described by an influence scheme. Such a hypothesis asserts properties as a *V*-statement does, but it may or may not make a statement on the behaviour of the function in question. Formally, a *hypothesis* is simply a special *V*-statement, typically written as *H*, that may state behaviour $\rightsquigarrow$. Satisfaction of a hypothesis *H* by an influence *F*, written $F \models H$, is defined as it is for *V*-statements.

This provides the model-theoretic machinery for the reasoning problem “does a given hypothesis follows from a scheme?” to be well-defined.

**Definition 3.** A hypothesis *H* follows from a *V*-influence scheme *C*, written *C*models *H*, if for all *V*-influence experiments *F* with *F*models *C* we have *F*models *H*.

*Example 3.* Consider the *V*-influence experiment $\mathcal{F}$ and the *V*-influence scheme *C* shown in Fig. 1. The statement $H = \text{AP} \downarrow_{[6000,8000]} \uparrow_{[10,30]} \text{Ox}$ is a formalisation of the hypothesis given above. It is visualised in Fig. 1 as a red box to distinguish it from the grey boxes representing the scheme.

It is straightforward to see that $\mathcal{F}_{\text{Alt,Ox}} \models H$, and hence $\mathcal{F} \models H$, holds. However, this does not imply that $C \models H$ holds, as there may be *V*-influence experiments $\mathcal{F}'$ with $\mathcal{F}' \models C$ such that $\mathcal{F}'_{\text{Alt,Ox}} \not\models H$, for example when $\mathcal{F}'_{\text{Alt,Ox}}$ takes values in $[40, 50]$ on the domain of $[6000, 8000]$.

We aim to give an algebraic characterisation of logical consequence between schemes and hypotheses, i.e. to provide a sound and complete decision procedure for the following problem SCHEMEENTAILMENT over a given variable set $\mathcal{V}$:

**given:** a *V*-influence scheme *C*, a hypothesis *H*
**decide:** does *C*models *H* hold?

As a syntactic convention, we write $C \cup H$ instead of $C \cup \{H\}$ in the following.

## 3 Indistinguishable Experiments

In general, there are uncountably many influence experiments that satisfy a given influence scheme, given that a statement is a rather coarse representation of uncountably many continuous, real-valued functions. Hence, SCHEMEENTAILMENT cannot be solved by exhaustive search. A promising idea is to formalize logical consequence of schemes and statements into a calculus and to show completeness of this calculus. This works in certain instances, but in general this approach suffers from the complex interactions that the coherence property induces alongside chains in the variable order, sometimes even in a backwards fashion [5]. We therefore follow a different approach: we reduce SCHEMEENTAILMENT to a
<figure><img src="image_69.png" /><figcaption>Fig. 2. An influence scheme that enforces behaviour $\rightsquigarrow$.</figcaption></figure>

corresponding problem in a discrete space. This is achieved by combining sets of influence experiments into finitely many equivalence classes according to a yet-to-be-defined equivalence relation.

A first intuition behind this uses the fact that a scheme (and a hypothesis) may only “talk about” finitely many points, namely those mentioned as the borders of the domain or range of a statement. The exact values of an influence strictly between such boundary points are not important, only their abstract behaviour. This approach will be refined later, but we illustrate the idea first.

*Example 4.* Consider the scheme $C = \{a \stackrel{[1,2]}{\frown} [0,2] \to b\}$ and the hypothesis $a \stackrel{[1,2]}{\to} [0,1] \to b$. It is easy to see that e.g. the influence $\mathcal{F}_{a,b}(x) = 2$ defined on $[0,2]$ refutes $C \models H$. However, we can divide the set of all influences that satisfy $C$ into seven different classes, tabulated below:

<table><thead><tr><th>behaviour on [1, 2]</th><th>image of F<sub>a,b</sub> on [1, 2]</th></tr></thead><tbody><tr><td>constant</td><td>[0, 0], [1, 1], [2, 2], or [i, i] with 0 &lt; i &lt; 1 or 1 &lt; i &lt; 2</td></tr><tr><td>strictly monotonic</td><td>[i, j] with 0 &le; i &lt; j &le; 1, 1 &le; i &lt; j &le; 2 or i &lt; 1 &lt; j</td></tr></tbody></table>

It is not hard to verify that each of these classes can be realized by an actual influence, and that these seven classes partition the set of all influences that satisfy $C$. Moreover, either all influences from a class satisfy $H$, or none does, so this partitioning is a congruence w.r.t. $H$. We conclude that $C \not\models H$, since the influences in at least one of these classes satisfy $C$, but not $H$.

These seven classes are not defined arbitrarily, but following two criteria: (I) the *actual* range of the influence on the interval $[1, 2]$, compared to one of the integers that appears as a bound on the *b*-axis (i.e. 0, 1 or 2), and (II) the *actual* behaviour of the influence on the interval $[1, 2]$.

If $C$ had been $\{a \stackrel{[0,1]}{\frown} [0,1] \to b, a \stackrel{[1,2]}{\to} [0,2] \to b\}$, it would not suffice to look at the behaviour on the interval $[1, 2]$, even though $H$ is restricted to it. In fact, we would have generated 20 equivalence classes since there are five options for the behaviour of an influence on the domain $[1, 2]$ (the five constant options above), and another four for the behaviour on $[0, 1]$ (the four options where the actual range is in $[0, 1]$). Of course, some of them do not form a proper influence (e.g. the function that is constant 0 on $[0, 1]$ and constant 2 on $[1, 2]$). This illustrates that we have to look at the whole scheme in order to ensure that each class is inhabited.
In the presence of a nontrivial chain $a < b < c$ in the variable order, the approach needs to be refined, though.

*Example 5.* Consider the scheme

$$C = \{ a \xrightarrow{[0,1] \parallel [0,1]} b, a \xrightarrow{[1,2] \parallel [0,5]} b, a \xrightarrow{[2,3] \parallel [4,5]} b, b \xrightarrow{[0,1]} [1,1] \to c, \\ b \xrightarrow{[1,2] \parallel [0,1]} c, b \xrightarrow{[2,3]} [1,1] \to c, b \xrightarrow{[3,4] \parallel [0,1]} c, b \xrightarrow{[4,5]} [0,0] \to c \}$$

depicted in Fig. 2 with an influence that satisfies it. Due to the construction of the scheme, the image of $\mathcal{F}_{a,b}$ on $[1, 2]$ must include the entire interval $[1, 4]$. On the other hand, $\mathcal{F}_{b,c}$ must describe a convex pattern on $[1, 4]$, moving upwards from 0 to 1 between 1 and 2, staying constant between 2 and 3, and moving downwards from 1 to 0 between 3 and 4. Hence, the influence $\mathcal{F}_{a,c}$ must describe a similar pattern on $[1, 2]$.

This behaviour in Example 5 produces two problems:

- The behaviour of any $\mathcal{F}_{a,c}$ on $[1, 2]$ can only be described as $\rightsquigarrow$, even though influence schemes cannot have $\rightsquigarrow$ in their statements. Hence, such behaviour can crop up as a logical consequence of seemingly innocuous statements.

- The categorisation of influence schemes alongside the bounds of the scheme described above does not work in the presence of nontrivial variable chains. For example, $C' = C \setminus \{a \xrightarrow{[2,3] \parallel [4,5]} b\}$ does not force the above convex pattern on $\mathcal{F}_{a,c}$. However, such a pattern still satisfies $C'$ whence it must be considered because any influence experiment that satisfies $C$ also satisfies $C'$.

However, the above approach of categorising functions alongside the bounds mentioned in a scheme and a hypothesis does not fail completely. While $\mathcal{F}_{a,c}$ describes the convex pattern within the interval $[1, 2]$, and, hence, has behaviour $\rightsquigarrow$, this does not mean that the behaviour of $\mathcal{F}_{a,c}$ is completely arbitrary. In fact, any influence that satisfies $C$ must describe exactly this behaviour, and for every such influence, there are points $x \le y \in (1, 2)$ that mark beginning, respectively the end of the top constant part of the convex pattern (also depicted in Fig. 2). Where exactly they sit depends on the concrete influence, but they must exist and $1 < x < y < 2$ must be true. Moreover, the influence is monotonic between 1 and $x$, constant between $x$ and $y$, and antitonic between $y$ and 2.

Hence, the idea of categorising influence experiments into finitely many equivalence classes needs to be refined by introducing such undefined, but constrained points of interest, that (i) are derived (heriditarily) from the bounds of the scheme and (ii) partition the influence in question into pieces that resort to behaviour which is stronger than $\rightsquigarrow$ again.

Next, we outline the intuition and essential properties that such equivalence relations should satisfy. However, the precise definition and construction of these equivalence relations, and how to handle the coherence property in the presence of variable chains, are non-trivial and form the core contributions of this work. These are detailed in Sect. 4 and Sect. 5.

The above considerations gives rise to the following, refined idea: given an input to the problem SCHEMEENTAILMENT, i.e. an influence scheme $C$ and a
hypothesis $H$, for each pair of variables $a, b$ with $a < b$, compute an equivalence relation $\sim_{C,H,a,b}$ that satisfies the following properties:

1. (Finiteness) The index of $\sim_{C,H,a,b}$ is finite and the classes are effectively enumerable.

2. (Congruence w.r.t. $C$) If $\mathcal{F}_{a,b} \sim_{C,H,a,b} \mathcal{G}_{a,b}$, then $\mathcal{F}_{a,b} \models C_{a,b}$ if and only if $\mathcal{G}_{a,b} \models C_{a,b}$.

3. (Congruence w.r.t. $H$) $\mathcal{F}_{a,b} \sim_{C,H,a,b} \mathcal{G}_{a,b}$ and $H = a \stackrel{IqI'}{\longmapsto} b$, then $\mathcal{F}_{a,b} \models H$ if and only if $\mathcal{G}_{a,b} \models H$.

4. (Coherence) For all $c \in \mathcal{V}$ with $b < c$, if $\mathcal{F}_{a,b} \sim_{C,H,a,b} \mathcal{G}_{a,b}$ and $\mathcal{F}_{b,c} \sim_{C,H,b,c} \mathcal{G}_{b,c}$, then $\mathcal{F}_{a,c} \sim_{C,H,a,c} \mathcal{G}_{a,c}$.

The first three properties have been discussed above. The last property, Coherence, is a crucial sanity condition that filters out influence classes that do not match each other, i.e. that cannot satisfy the coherence property.

The structure of experiments allows us to lift these relations on influences to a relation on experiments, by defining $\mathcal{F} \sim_{C,H} \mathcal{G}$ if $\mathcal{F}_{a,b} \sim_{C,H,a,b} \mathcal{G}_{a,b}$ for all $a, b \in \mathcal{V}$ with $a < b$. This yields an algorithm to determine whether $C \models H$.

1. For all $a, b \in \mathcal{V}$ with $a < b$ but no $c$ with $a < c < b$, compute the equivalence classes of $\sim_{C,H,a,b}$. Remove all uninhabited (due to discontinuities) classes.

2. Combine the equivalence classes of $\sim_{C,H,a,b}$ for all $a, b \in \mathcal{V}$ with $a < b$ to obtain the equivalence classes of $\sim_{C,H}$.

3. Remove equivalence classes that do not satisfy $C$.

4. Check whether all remaining classes do satisfy $H$ and return **true** if yes, or else return **false** if this fails for some class.

The first and second step work because there are only finitely many equivalence classes of $\sim_{C,H,a,b}$, which can be effectively enumerated. The second step requires the coherence property to be satisfied, which is possible due to the requirement of Coherence above. The third step is possible since all experiments in the same equivalence class are indistinguishable with respect to $C$ (Congruence w.r.t. $C$), hence we must only check for one experiment in each equivalence class whether it satisfies the respective sub-scheme. Finally, the last step works as equivalent experiments are indistinguishable with respect to $H$ (Congruence w.r.t. $H$).

The most challenging requirement on the equivalence relations is Coherence. It involves complex and fine-grained reasoning about the equivalence classes. Hence, in Sect. 4 we focus on schemes defined over *flat* variable orders, i.e. orders where there are no variable chains of the form $a < b < c$, whence Coherence is satisfied vacuously and a formalisation of the informal discussion above suffices. The assumption of flatness is then lifted in Sect. 5.

# 4 Completeness for Flat Schemes

In this section, we assume the underlying variable order to be *flat*, i.e. there are no $a, b, c \in \mathcal{V}$ such that $a < b < c$. Experiments over a flat variable order are more general than just a single influence, as they may contain multiple influences, but these are unrelated by the coherence property.
**Definition 4.** Let $\mathcal{C}$ be a $\mathcal{V}$-influence scheme, let $H$ be a hypothesis, and let $a \in \mathcal{V}$. Then $p$ is an $a$-boundary point if

- there is $S \in \mathcal{C}_{a,b} \cup H$ for some $a < b$ with $S = a \xrightarrow{[x,y]q[l,u]} b$ and $p = x$ or $p = y$, or

- there is $S \in \mathcal{C}_{b,a} \cup H$ for some $b < a$ with $S = b \xrightarrow{[x,y]q[l,u]} a$ and $p = l$ or $p = u$.

We write $\text{bds}_a(\mathcal{C} \cup H)$ for the set of all $a$-boundary points of $\mathcal{C}$ and $H$.

Note that $\text{bds}_a(\mathcal{C} \cup H)$ is naturally ordered via the order of the reals, whence we can refer to the $i$th such point (tacitly assuming that such an $i$th point exists).

Given a $\mathcal{V}$-influence scheme $\mathcal{C}$ and a hypothesis $H$, we consider influences to be equivalent if they behave in the same way w.r.t. all boundary points, formalised as follows.

**Definition 5.** Let $\mathcal{C}$ be a scheme and let $H$ be a hypothesis. Let $f$ be an influence from $a$ to $b$, $[x,y] \subseteq \text{dom}(f)$, $\text{rang}_{[x,y]}(f) = [l,u]$. Then the value range of $f$ is $\text{vrng}_{[x,y]}(f) = [l',u']$ where $l' = \max\{p \in \text{bds}_b(\mathcal{C} \cup H) \mid p \le l\}$ and $u' = \min\{p \in \text{bds}_b(\mathcal{C} \cup H) \mid p \ge u\}$.

Combining this definition with the intuition explained in the previous section, we obtain the following definition of the equivalence of influences.

**Definition 6.** Let $\mathcal{C}$ be a $\mathcal{V}$-influence scheme, $a,b \in \mathcal{V}$ such that $a < b$, $H$ be a hypothesis, $f,g$ be influences from $a$ to $b$.

Then $f$ is equivalent to $g$ w.r.t. $H$ and $\mathcal{C}$, written $f \sim_{\mathcal{C},H,a,b} g$, if for all $x,x'$ that are the $i$th and $i+1$st point in $\text{bds}_a(\mathcal{C} \cup H)$ for some $i$, we have $[x,x'] \not\subseteq \text{dom}(f)$ and $[x,x'] \not\subseteq \text{dom}(g)$, or

1. $[x,x'] \subseteq \text{dom}(f)$ and $[x,x'] \subseteq \text{dom}(g)$,

2. $\text{vrng}_{[x,x']}(f) = \text{vrng}_{[x,x']}(g)$, and

3. $f|_{[x,x')} = g|_{[x,x]}$.

This formalises the above idea that two influences are equivalent if they have (i) the same range w.r.t. the $b$-boundary points on each interval introduced by $a$-boundary points, and (ii) the same actual behaviour, or equivalently are both undefined on such an interval.

It is not hard to verify that $\sim_{\mathcal{C},H,a,b}$ is an equivalence relation. This leaves the requirements collected in Sect. 3 to be shown.

**Lemma 1.** Let $\mathcal{C}$ be a $\mathcal{V}$-influence scheme and $H$ be a hypothesis. Let $a < b$. Then the index of $\sim_{\mathcal{C},H,a,b}$ is finite and the classes are effectively enumerable.

*Proof (Sketch).* Since the $\mathcal{V}$-influence scheme $\mathcal{C}$ is finite, there are only finitely many boundary points for $a$ and $b$. Between consecutive $a$-boundary points, only finitely many value ranges and behaviours are possible. All options can be effectively enumerated, excluding combinations where value ranges within segments are conflicting. $\square$
The two congruence requirements (w.r.t. $\mathcal{C}$ and $H$) are closely related; we
therefore consider them together.

**Lemma 2.** Let $\mathcal{C}$ be a $\mathcal{V}$-influence scheme, $H$ be a hypothesis and $f$ and $g$ be influences from $a$ to $b$ such that $f \sim_{\mathcal{C},H,a,b} g$. For any $S \in \mathcal{C}_{a,b} \cup H$, we have $f \models S$ iff $g \models S$.

*Proof (Sketch).* Each class of $\sim_{C,H,a,b}$ contains more information than any $\mathcal{V}$-statement in $\mathcal{C} \cup H$, and hence, it suffices to combine this information to verify that all influences in a given class satisfy a given $\mathcal{V}$-statement. $\square$

We lift the definition of $\sim_{C,H,a,b}$ to influence experiments in the expected way.

**Definition 7.** Let $\mathcal{C}$ be a flat $\mathcal{V}$-influence scheme and $H$ be a hypothesis. $\mathcal{F}$ and $\mathcal{G}$ are equivalent with respect to $\mathcal{C}$ and $H$, written $\mathcal{F} \sim_{\mathcal{C},H} \mathcal{G}$, if for all $a,b \in \mathcal{V}$ such that $a < b$, it holds that $\mathcal{F}_{a,b} \sim_{\mathcal{C},H,a,b} \mathcal{G}_{a,b}$.

It is straightforward to see that finiteness and the congruences extend from $\sim_{C,H,a,b}$ to $\sim_{C,H}$. Coherence holds trivially. Hence, as described in Sect. 3, decidability of SCHEMEENTAILMENT for flat schemes follows.

**Theorem 1.** SCHEMEENTAILMENT is decidable for flat $\mathcal{V}$-influence schemes in polynomial time.

*Proof (Sketch).* Given a flat $\mathcal{V}$-influence scheme $\mathcal{C}$ and a hypothesis $H$, the equivalence relation $\sim_{C,H}$ has finitely many classes, as follows from Lemma 1 and the finiteness of $\mathcal{V}$. Thus, we can enumerate all equivalence classes, discard those that do not satisfy the $\mathcal{V}$-influence scheme $\mathcal{C}$, and check whether any of the remaining classes satisfy the hypothesis $H$. Both steps are possible by Lemma 2.

Although this naive exhaustive enumeration does not yield a polynomial-
time algorithm, a more refined approach guided by the structure of $H$ permits a
more efficient exploration of the search space. Specifically, for flat schemes, such
a hypothesis-driven procedure ensures polynomial-time decidability. $\square$

It should be noted that this is already known from [5]. However, the approach
outlined above is more general and carries further, to be seen in the next section.

**5 Completeness for General Schemes**

Now we consider schemes over an arbitrary order that is not necessarily flat. When chains of the form $a < b < c$ are allowed, coherence does not hold automatically. This makes reasoning more challenging. Recall from Sect. 3 that the logic of function composition can force influences to exhibit behaviour that can only be described as $\rightsquigarrow$. In Sect. 3, we already saw a potential remedy: to look at more points.

We refine the notion of boundary points twice, first to so-called *turning points*, which formalise the idea that the slope of an influence from *a* to *b* may be so
steep that it crosses several *b*-boundary points between two *a*-boundary points. The points on the *a*-axis where this happens are the turning points. While their exact position is not necessarily the same for two equivalent influences, their existence and relative position are (i.e. influences without such a steep slope may not exhibit such turning points). The notion of turning points works backwards on the variable order: *b*-boundary points (and, in fact, *b*-turning points) induce *a*-turning points, and so forth.

However, refining boundary points into turning points does not suffice. We later refine the concept further into so-called points of interest that also carry information forward alongside the variable order. We then obtain an equivalence relation define analogously to that in Sect. 4, but using points of interest instead of boundary points, which yields the desired decision procedure.

*Turning Points.* Above we said that a turning point is the point on the *a*-axis on which an influence from *a* to *b* crosses a *b*-boundary point (actually, a *b*-turning point). However, that point may not be unique, not even on an interval on which a function is strictly monotonic, since it can remain constant for a time. Hence, we introduce the following notation:

$$- \mathrm{vfst}_{[x,y]}(f, p) = \min\{z \mid x \le z \le y, f(z) = p\}$$

$$- \mathrm{vlst}_{[x,y]}(f, p) = \max\{z \mid x \le z \le y, f(z) = p\}$$

**Definition 8 (Turning Points).** Let $\mathcal{C}$ be a $\mathcal{V}$-influence scheme and be $H$ a hypothesis. Let $\mathcal{F}$ be a $\mathcal{V}$-influence experiment and $a \in \mathcal{V}$. Then $p$ is an *a*-turning point if $p$ is an *a*-boundary point, or

1. there is $b \in \mathrm{Post}(a)$ with $\mathrm{Post}(b) \neq \emptyset$,

2. there are adjacent *a*-boundary-points $x < y$ with $[x, y] \subseteq \mathrm{dom}(\mathcal{F}_{a,b})$,

3. there is a *b*-turning point $t$ with $t \in \mathrm{rang}_{[x,y]}(\mathcal{F}_{a,b})$, and

4. $p = \mathrm{vfst}_{[x,y]}(\mathcal{F}_{a,b}, t)$ or $p = \mathrm{vlst}_{[x,y]}(\mathcal{F}_{a,b}, t)$.

We write $\mathrm{tp}_a(\mathcal{F}, \mathcal{C}, H)$ for the set of *a*-turning points.

The definition matches the intuition above: a turning point is a point on the *a*-axis such that $\mathcal{F}_{a,b}$ reaches an important point on the *b*-axis (i.e. a *b*-turning point, which includes *b*-boundary points) for the first or last time on an interval induced by two adjacent *a*-boundary points.

The definition is inductive in a top-down fashion along the influence order: turning points for a variable *a* are defined based on the turning points of its successors $b \in \mathrm{Post}(a)$. For maximal variables (i.e. those with no successors), the important points on the *b*-axis are simply the *b*-boundary points. For non-maximal variables, the important points are the inductively constructed *b*-turning points.

We illustrate the concept with an example. Consider the $\mathcal{V}$-influence experiment $\mathcal{F}$ depicted in Fig. 3, and assume that $\mathcal{C}$ and $H$ are given s.t. $\mathrm{bds}_c(\mathcal{C} \cup H) = \{0, 1, 2\}$. As $d$ is maximal w.r.t. $<$, by definition, we have $\mathrm{tp}_d(\mathcal{F}, \mathcal{C}, H) = \mathrm{bds}_d(\mathcal{C} \cup H)$, and hence also $\mathrm{tp}_c(\mathcal{F}, \mathcal{C}, H) = \mathrm{bds}_c(\mathcal{C} \cup H)$. The intuition here is that there is no influence in the experiment that can be composed with $\mathcal{F}_{c,d}$, whence it suffices to look at the boundary points of $d$ and $c$.
<figure><img src="image_70.png" /><figcaption>Fig. 3. Example showing the construction of turning points.</figcaption></figure>

Now consider $tp_b(\mathcal{F}, \mathcal{C}, H)$. Since the composition of $\mathcal{F}_{b,c}$ with $\mathcal{F}_{c,d}$ yields $\mathcal{F}_{b,d}$, we have to consider potential subdivisions of the $b$-axis to ensure that the latter function has behaviour stronger than $\rightsquigarrow$ between two $b$-turning points. Hence, such points are introduced on the $b$-axis whenever $\mathcal{F}_{b,c}$ crosses a $c$-turning point, for example at roughly 0.2 and 0.8. The same process is repeated to obtain $tp_a(\mathcal{F}, \mathcal{C}, H)$ (cf. Fig. 3 for details).

Note that, for nonlinear variable orders, e.g. those of the form $a < b < c$ and $a < d < e$, the definition yields $a$-turning points derived from $tp_b(\mathcal{F}, \mathcal{C}, H)$ and from $tp_d(\mathcal{F}, \mathcal{C}, H)$.

*Points of Interest.* The introduction of turning points does not suffice to cover all peculiarities introduced by the presence of function composition, together with the requirement of coherence. Consider Fig. 4. It shows an experiment consisting of $f$ and $g$ (in black and blue), and one consisting of $f$ and $g'$ (in black and red). The influences $g$ and $g'$ are equivalent w.r.t. to the definition from Sect. 4, even with turning points in place of boundary points. However, their compositions are clearly not equivalent under any sensible definition, since one of them is constant and the other is not.

The reason for this problem is that $g$ and $g'$ behave differently on the interval $[0.5, 1.5]$ on the $b$-axis generated by $f(0)$ and $f(1)$. The red function $g'$ is constant there, but the blue function $g$ is not. As a consequence, we extend the concept of turning points into that of points of interest, which are obtained by projecting turning points (actually, points of interest) forward alongside the variable order, just as turning point are projections backwards alongside that order.

<figure><img src="image_71.png" /><figcaption>Fig. 4. Influence composition: $f$ (left), $g$ and $g'$ (middle), and $g \circ f$, $g' \circ f$ (right).</figcaption></figure>
<figure><img src="image_72.png" /><figcaption>**Fig. 5.** Example showing the construction of points of interest.</figcaption></figure>

**Definition 9 (Points of Interest).** Let $\mathcal{C}$ be a $\mathcal{V}$-influence scheme, $H$ be a hypothesis, $\mathcal{F}$ be a $\mathcal{V}$-influence experiment and $b \in \mathcal{V}$. Then $p$ is a $b$-point of interest with respect to $\mathcal{C}$, $H$ and $\mathcal{F}$ if $p$ is a $b$-turning point, or if there is an $a$-point of interest $p'$ s.t. $p = \mathcal{F}_{a,b}(p')$. We write $\text{poi}_b(\mathcal{F}, \mathcal{C}, H)$ for the set of $b$-points of interest.

The definition is inductive in a bottom-up fashion along the influence order: points of interest for a variable $b$ are defined from the turning points of $b$, and also they are propagated forward via the functions $\mathcal{F}_{a,b}$ from points of interest of predecessor variables $a$. This means a point of interest for $b$ is either a $b$-turning point, or the image of an $a$-point of interest under $\mathcal{F}_{a,b}$.

Again, we illustrate the concept by means of an example. Consider the previous example depicted in Fig. 4. The points of interest for $a, b, c$, and $d$ can be computed in a bottom-up fashion. To keep the visualization concise, we base the construction on bds($\mathcal{C} \cup H$) instead of $\text{tp}_a(\mathcal{F}, \mathcal{C}, H)$ for each variable $a \in \mathcal{V}$.

Since $a$ is minimal w.r.t. the variable order, the $a$-points of interest are simply the $a$-boundary points (actually, the $a$-turning points).

We obtain $\text{tp}_b(\mathcal{F}, \mathcal{C}, H)$ as the set of the $\mathcal{F}_{a,b}(x)$ where $x \in \text{tp}_b(\mathcal{F}, \mathcal{C}, H)$. We iterate this for $c$ and $d$, each based on the points of interest of the predecessor variable. Note that, as for the turning points, in non-linear variable orders a variable projects points of interests on all its successors w.r.t the variable order (Fig. 5).

*Equivalence of Experiments.* We now lift the definitions of $\sim_{\mathcal{C},H,a,b}$ and $\sim_{\mathcal{C},H}$, based on boundary points (cf. Definitions 6 and 7) to their natural refinement based on points of interest.

Recall that sets such as $\text{poi}_a(\mathcal{F}, \mathcal{C}, H)$ can be viewed as ordered lists, using the order on the reals. Hence, we can speak of e.g. the $i$th $a$-point of interest (with the tacit assumption that $i$ is such that this point exists). The following definition formalises the idea that two influence experiments have the same structure of points of interest (w.r.t. a scheme and a hypothesis), i.e. the same number of points of interest for each variable, and these points connect to points of interest for other variables in the same manner.

**Definition 10.** Let $\mathcal{C}$ be a $\mathcal{V}$-influence scheme, $H$ be a hypothesis, $\mathcal{F}$ and $\mathcal{G}$ be $\mathcal{V}$-influence experiments. Assume that the following holds for all $a \in \text{Vars}$:
1. We have $|\mathrm{poi}_a(\mathcal{F}, \mathcal{C}, H)| = |\mathrm{poi}_a(\mathcal{G}, \mathcal{C}, H)|$.

2. Let $x$ be the $i$th point in $\mathrm{poi}_a(\mathcal{F}, \mathcal{C}, H)$, let $x'$ be the $i$th point in $\mathrm{poi}_a(\mathcal{G}, \mathcal{C}, H)$.

(a) If $p \in \mathrm{bds}_a(\mathcal{C} \cup H)$ is an $a$-boundary point, then $p = x$ iff $p = x'$.

(b) If $b \in \mathrm{Pre}(a)$, $y$ is the $j$th point in $\mathrm{poi}_b(\mathcal{F}, \mathcal{C}, H)$ and $y'$ is the $j$th point in $\mathrm{poi}_b(\mathcal{G}, \mathcal{C}, H)$, then $x = \mathcal{F}_{b,a}(y)$ iff $x' = \mathcal{F}_{b,a}(y')$.

(c) If $b \in \mathrm{Post}(a)$, $y$ is the $j$th point in $\mathrm{poi}_b(\mathcal{F}, \mathcal{C}, H)$, $y'$ is the $j$th point in $\mathrm{poi}_b(\mathcal{G}, \mathcal{C}, H)$, and if $z_1, z_2$ are the $k$th and $k+1$st points in $\mathrm{tp}_a(\mathcal{F}, \mathcal{C}, H)$ and $z'_1, z'_2$ are the $k$th and $k+1$st points in $\mathrm{tp}_a(\mathcal{G}, \mathcal{C}, H)$, then $x = \mathrm{vfst}_{[z_1, z_2]}(\mathcal{F}_{a,b}, y)$ iff $x' = \mathrm{vfst}_{[z'_1, z'_2]}(\mathcal{G}_{a,b}, y')$, and $x = \mathrm{vlst}_{[z_1, z_2]}(\mathcal{F}_{a,b}, y)$ iff $x' = \mathrm{vlst}_{[z'_1, z'_2]}(\mathcal{G}_{a,b}, y')$.

Then $\mathcal{F}$ and $\mathcal{G}$ are order equivalent w.r.t. $C$ and $H$, written $\equiv_{\mathcal{C},H}^{\le}$.

The intuition here is the following: item 1 says that both experiments have the same number of $a$-points of interest. Item 2 says that corresponding $a$-points of interest match the same boundary points (subitem 2a) that they get mapped to corresponding $b$-points of interest (subitem 2b), and they are induced by the same crossing of turning points on the $b$-axis.

This definition does not force $\mathcal{F}$ and $\mathcal{G}$ to be equivalent in the stricter sense, i.e. they can still have functions with e.g. different actual variable ranges or actual behaviours. However, the desired equivalence is now easy to formalise based on order equivalence.

**Definition 11.** Let $C$ be a $\mathcal{V}$-influence scheme, $H$ be a hypothesis, $\mathcal{F}$ and $\mathcal{G}$ be order-equivalent $\mathcal{V}$-influence experiments, and $a, b \in \mathcal{V}$ with $a < b$. Assume that the following holds for all $x_1, x_2$ that are the $i$th and $i+1$st points in $\mathrm{poi}_a(\mathcal{F}, \mathcal{C}, H)$ and all $x'_1, x'_2$ that are the $i$th and $i+1$st points in $\mathrm{poi}_a(\mathcal{G}, \mathcal{C}, H)$:

1. $[x_1, x_2] \subseteq \mathrm{dom}(\mathcal{F}_{a,b})$ iff $[x'_1, x'_2] \subseteq \mathrm{dom}(\mathcal{G}_{a,b})$.

2. $\mathcal{F}_{a,b}|_{[x_1, x_2]} = \mathcal{G}_{a,b}|_{[x'_1, x'_2]}$.

3. Let $y_1, y_2$ be the $j$th and $k$th points in $\mathrm{poi}_b(\mathcal{F}, \mathcal{C}, H)$ and let $y'_1, y'_2$ be the $j$th and $k$th points in $\mathrm{poi}_b(\mathcal{G}, \mathcal{C}, H)$, where $j \le k$. Then $\mathrm{rang}_{[x_1, x_2]}(\mathcal{F}_{a,b}) = [y_1, y_2]$ iff $\mathrm{rang}_{[x'_1, x'_2]}(\mathcal{G}_{a,b}) = [y'_1, y'_2]$.

Then $\mathcal{F}_{a,b}$ and $\mathcal{G}_{a,b}$ are equivalent w.r.t. $C$, $a$, $b$ and $H$, written $\mathcal{F}_{a,b} \equiv_{\mathcal{C},H,a,b} \mathcal{G}_{a,b}$. $\mathcal{F}$ and $\mathcal{G}$ are equivalent w.r.t. $C$ and $H$, written $\mathcal{F} \equiv_{\mathcal{C},H} \mathcal{G}$, if $\mathcal{F}_{a,b} \equiv_{\mathcal{C},H,a,b} \mathcal{G}_{a,b}$ for all $a < b$.

The intuition here is that $\mathcal{F}_{a,b}$ and $\mathcal{G}_{a,b}$ are defined on the same intervals w.r.t. their $a$-points of interest (item 1), have the same actual behaviour on intervals between corresponding pairs of $a$-points of interest (item 2), and their value ranges on corresponding intervals (w.r.t. $a$-points of interest) are corresponding intervals (w.r.t. $b$-points of interest).

It remains to show that $\equiv_{\mathcal{C},H}$ possesses the properties given in Sect. 3. We first establish the finiteness and congruence properties, which follow by arguments similar to those in Lemma 1 and Lemma 2.
**Lemma 3.** Let $\mathcal{C}$ be a $\mathcal{V}$-influence scheme, $H$ be a hypothesis.

1. The index of $\equiv_{C,H}$ is finite and the equivalence classes can be effectively enumerated.

2. For any $\mathcal{V}$-influence experiments $\mathcal{F}$ and $\mathcal{G}$ such that $\mathcal{F} \equiv_{C,H} \mathcal{G}$ and any $S \in \mathcal{C} \cup H$, it holds that $\mathcal{F} \models S$ if and only if $\mathcal{G} \models S$.

*Proof (Sketch)*. Item 1 follows from the fact that the set of points of interest remains finite and enumerable, yielding only finitely many ways in which experiments can behave between these points. Item 2 relies on the fact that that each equivalence class of $\equiv_{C,H}$ captures strictly more information than any individual $\mathcal{V}$-statement in $\mathcal{C} \cup H$. This allows us to combine the available information in a class and verify whether all $\mathcal{V}$-influence experiments within it satisfy a given $\mathcal{V}$-statement. $\square$

Additionally, we have to show that coherence holds. This step is more involved and requires verifying that the conditions of Definition 11 ensure enough transitivity to guarantee Coherence.

**Lemma 4.** Let $\mathcal{C}$ be a $\mathcal{V}$-influence scheme, $H$ be a hypothesis and $\mathcal{F}$ and $\mathcal{G}$ be $\mathcal{V}$-influence experiments. Then for all $a, b, c \in \mathcal{V}$ such that $a < b < c$, it holds that if $\mathcal{F}_{a,b} \equiv_{C,H,a,b} \mathcal{G}_{a,b}$ and $\mathcal{F}_{b,c} \equiv_{C,H,b,c} \mathcal{G}_{b,c}$ then $\mathcal{F}_{a,c} \equiv_{C,H,a,c} \mathcal{G}_{a,c}$.

*Proof (Sketch)*. From the equivalence classes of $\equiv_{C,H,a,b}$ and $\equiv_{C,H,b,c}$, we know the exact behaviour of $\mathcal{F}_{a,b}$ between $a$-points of interest and of $\mathcal{F}_{b,c}$ between $b$-points of interest. Furthermore, the values of $\mathcal{F}_{a,b}$ on $a$-points of interest are themselves $b$-points of interest.

Thus, the range of $\mathcal{F}_{a,c}$ between consecutive $a$-points of interest is uniquely determined by composing the ranges of $\mathcal{F}_{a,b}$ and $\mathcal{F}_{b,c}$, and likewise, the behaviour of $\mathcal{F}_{a,c}$ between consecutive $a$-points of interest is fully determined by composing the behaviours of $\mathcal{F}_{a,b}$ and $\mathcal{F}_{b,c}$.

Applying the same arguments to $\mathcal{G}$, and by considering that $\mathcal{G}$ and $\mathcal{F}$ behave equally w.r.t. their points of interest, it follows that $\mathcal{F}_{a,c} \equiv_{C,H,a,c} \mathcal{G}_{a,c}$. $\square$

From the previous lemmas, we obtain the desired decidability of SCHEMEENTAILMENT, following the decision procedure outlined in Sect. 3.

**Theorem 2.** SCHEMEENTAILMENT is in coNP.

*Proof (Sketch)*. Given a $\mathcal{V}$-influence scheme $\mathcal{C}$ and a hypothesis $H$, we provide a polynomial-sized witness $\mathcal{P}$ verifying that $\mathcal{C} \not\models H$.

The witness consists of lists of pairs $\mathcal{P}_{a,b}$ for each $a, b \in \mathcal{V}$ with $a < b$, mapping $a$-points of interest to $b$-points of interest. If $(x, y) \in \mathcal{P}_{a,b}$, this imposes $\mathcal{F}_{a,b}(x) = y$, with monotonicity assumed between points.

Verifying that the induced $\mathcal{V}$-influence experiment $\mathcal{F}$ is a counterexample can be done in polynomial time:

- Coherence is checked via Lemma 4.

- Satisfaction of $\mathcal{C}$ and violation of $H$ follow from Lemma 3(2).
It remains to bound the witness size. By construction, the number of points of interest per $a \in \mathcal{V}$ is at most exponential in $|\mathcal{V}|$. Since $\mathcal{V}$ is fixed in the input, the total size of $\mathcal{P}$ remains polynomial. $\square$

# 6 Conclusion

This paper is concerned with a very particular reasoning problem which arises from an attempt to formalise models and tasks occurring in natural sciences classes, especially in designing and conducting experiments, with an overall aim to provide digitalisation support for such learning scenarios. We have extended previous work based on a simple proof system, known as the *Calculus of Influence* (CoI) [5], in the sense that the algebraic approach to the underlying reasoning problem presented here lifts several structural restrictions which need to be imposed on schemes in order for CoI to provide sound and complete reasoning.

The acute reader may have noticed two restrictions on schemes that have been imposed here, and that were not imposed for CoI: here, the domain of scheme statements cannot contain infinities as interval bounds. This is simply done for simplicity. Statements like $\xrightarrow{[0,\infty] \vee [0,1]}$ could be handled by replacing infinities by sufficiently large numbers. Second, we drew a distinction between scheme statements and hypotheses: arbitrary behaviour can only be stated in hypotheses. Technically, schemes with arbitrary behaviour are too weak to categorise their models in terms of equivalences of finite index, since the coherence property could demand an arbitrary amount of turning points. While this restriction slightly weakens this approach mathematically, we argue that from an application point of view arbitrary behaviour in schemes is unnatural anyway. Its main purpose is to allow hypotheses to be formalised even when pupils' knowledge about experiments is only partial, i.e. when they can predict the range of influences for instance, but not necessarily its monotonicity or antitonicity.

Further work is going into two directions: a reasoner for influence needs to be integrated into educational software which allows experiments to be designed and conducted virtually. It remains to be seen what the best practical approaches for solving SCHEMEENTAILMENT are, perhaps based on the use of SMT solvers or an on-the-fly, goal-directed search.

Moreover, the model of influence schemes studied here does not cover arbitrary scenarios in experiments in natural sciences. Many biological or chemical processes are only triggered by the combination of several variables. This happens, for example, in gene transcription which may only occur in the presence of multiple transcription factors, cf. [12]. Chemical reactions often only proceed when a substrate and a co-factor are present, for instance Acetaldehyde requires Ethanol and NAD+, cf. [13]. Also, the use of specific, interpreted variables like time [4] may require specific reasoning principles. All in all, the theory of formal models for reasoning about influence in phenomena studied in natural sciences largely remains to be explored further.
## References

1. Andrews, P.B.: Classical type theory. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 965–1007. North-Holland (2001). https://doi.org/10.1016/B978-044450813-3/50017-5

2. Baader, F., Calvanese, D., McGuinness, D.L., Nardi, D., Patel-Schneider, P.F. (eds.): The Description Logic Handbook: Theory, Implementation, and Applications. Cambridge University Press (2003)

3. Bortolussi, L., Policriti, A.: Hybrid systems and biology. In: International School on Formal Methods for the Design of Computer, Communication and Software Systems, pp. 424–448. Springer (2008)

4. Bruse, F., Kastaun, M., Lange, M., Möller, S.: The calculus of temporal influence. In: Proceedings of 30th International Symposium on Temporal Representation and Reasoning, TIME 2023. LIPICs, vol. 278, pp. 10:1–10:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023). https://doi.org/10.4230/LIPICS.TIME.2023.10

5. Bruse, F., Lange, M., Möller, S.: Formal reasoning about influence in natural sciences experiments. In: Proceedings of 29th International Conference on Computed-Aided Deduction, CADE 2023. LNCS, vol. 14132, pp. 153–169. Springer, Cham (2023)

6. De Ory, I., Romero, L.E., Cantero, D.: Modelling the kinetics of growth of acetobacter aceti in discontinuous culture: influence of the temperature of operation. Appl. Microbiol. Biotechnol. 49(2), 189–193 (1998)

7. Demri, S., Goranko, V., Lange, M.: Temporal Logics in Computer Science. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press (2016). http://www.cambridge.org/coretitle/gb/434611

8. Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press (2000)

9. Harrison, J.: Handbook of Practical Logic and Automated Reasoning. Cambridge University Press (2009)

10. Henzinger, T.A.: The theory of hybrid automata. In: Proceedings of 11th Annual IEEE Symposium on Logic in Computer Science, pp. 278–292. IEEE (1996)

11. Hillmayr, D., Ziernwald, L., Reinhold, F., Hofer, S., Reiss, K.: The potential of digital tools to enhance mathematics and science learning in secondary schools: a context-specific meta-analysis. Comput. Educ. 153, 103897 (2020)

12. Panne, D., Maniatis, T., Harrison, S.C.: Crystal structure of ATF-2/c-Jun and IRF-3 bound to the interferon-beta enhancer. EMBO J. 23, 4384–4393 (2004). https://doi.org/10.1038/sj.emboj.7600453

13. Plapp, B.V.: Conformational changes and catalysis by alcohol dehydrogenase. Arch. Biochem. Biophys. 493(1), 3–12 (2010). https://doi.org/10.1016/j.abb.2009.07.001

14. Robinson, J.A., Voronkov, A. (eds.): Handbook of Automated Reasoning (in 2 volumes). Elsevier and MIT Press (2001)

15. Smullyan, R.M.: First-Order Logic. Springer (1968)

16. Steggles, L.J., Banks, R., Wipat, A.: Modelling and analysing genetic networks: from boolean networks to petri nets. In: Priami, C. (ed.) CMSB 2006. LNCS, vol. 4210, pp. 127–141. Springer, Heidelberg (2006). https://doi.org/10.1007/11885191_9

17. Sumatokhin, S., Petrova, O., Serovayskaya, D., Chistiakov, F.: Digitalization of school biological education: problems and solutions. In: SHS Web of Conferences, vol. 79, p. 01016. EDP Sciences (2020)
18. Theocharopoulou, G., Bobori, C., Vlamos, P.: Formal models of biological systems. In: Proceedings of 2nd World Congress on Genetics, Geriatrics and Neurodegenerative Disease, GeNeDis 2016, Advances in Experimental Medicine and Biology, vol. 987, pp. 325–338. Springer (2017)

**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_73.png" /></figure>
Proof Checking
# Checking Linear Integer Arithmetic Proofs
in Lambdapi

Alessio Coltellacci and Stephan Merz

University of Lorraine, CNRS, Inria, LORIA, Nancy, France

alessio.coltellacci@inria.fr stephan.merz@loria.fr

**Abstract.** Modern SMT solvers can generate proofs of unsatisfiability so that the result can be checked independently. A dependable approach to verify these proofs is to reconstruct them within a proof assistant. In previous work, the SMT checker Carcara was extended to reconstruct SMT proofs in Lambdapi—a proof assistant designed for interoperability, supporting the import and export of proofs for integration with other proof assistants such as Rocq, Lean, or HOL-Light. Whereas that work was limited to SMT theories without arithmetic, we here present an extension that enables the reconstruction of SMT proofs involving linear integer arithmetic.

**Keywords:** SMT · Alethe · integer arithmetic · Lambdapi · normal form · proof by reflection

## 1 Introduction

SMT solvers have become capable of producing proofs of unsatisfiability, enabling independent verification of correctness without relying on the solver's implementation. This development addresses the growing need for trustworthy verification in safety-critical applications and for using SMT solvers as backends of skeptical proof assistants that do not trust the solver. Alethe [2,24] is an established SMT proof format supported by the solvers cvc5 and veriT. In our previous work [12], we extended the Alethe proof checker and elaborator Carcara [1] to reconstruct Alethe SMT proofs within the Lambdapi proof assistant, thereby ensuring their validity. Lambdapi [18] is a proof assistant based on the λΠ-calculus modulo rewriting [13], a logical framework [17] that extends the λ-calculus with dependent types and user-defined rewrite rules. This foundation allows Lambdapi to serve as a framework for formalizing various logical systems. Designed with interoperability in mind, Lambdapi can import and export proofs, facilitating integration with other proof assistants such as Rocq [26], Lean [20], and HOL-Light [9].

However, our prior work was limited to proofs expressed within the logic of Uninterpreted Functions (UF). In the present work, we extend this approach to support the reconstruction of proof steps involving linear integer arithmetic (LIA). In the context of LIA, the SMT solver determines unsatisfiability by analyzing formulas composed of integer variables, linear arithmetic operations,
and logical connectives. This process typically relies on techniques such as Simplex methods adapted for integers and cutting-plane methods to establish the unsatisfiability of linear constraints [11, 14]. Our main contribution is the implementation of an automatic decision procedure to verify these proof steps, using proof by reflection [10, 16].

The remainder of this paper is organized as follows. In Sect. 2, we provide an overview of Lambdapi and present the structure of Alethe proof certificates for linear arithmetic. Then, in Sect. 3, we describe how we leverage Carcara’s elaboration process to reconstruct linear integer arithmetic steps, even when coefficient annotations are missing. Section 4 introduces our encoding of SMT linear arithmetic within Lambdapi, while Sect. 5 presents an automatic decision procedure, based on proof by reflection, to verify these arithmetic steps. An empirical evaluation of our approach is provided in Sect. 6. We review related work in Sect. 7, and we conclude in Sect. 8.

# 2 Background

## 2.1 An Overview of Lambdapi

Lambdapi is an implementation of $\lambda\Pi$ modulo theory ($\lambda\Pi/\equiv$) [18], an extension of the Edinburgh Logical Framework $\lambda\Pi$ [17] that is based on a simply typed $\lambda$-calculus with dependent types. $\lambda\Pi/\equiv$ adds user-defined higher-order rewrite rules. Its syntax is given by

<table><tr><td>Universes</td><td>$u ::= \mathbf{TYPE} | \mathbf{KIND}$</td></tr><tr><td>Terms</td><td>$t, v, A, B, C ::= c | x | u | \Pi x : A, B | \lambda x : A, t | t v$</td></tr><tr><td>Contexts</td><td>$\Gamma ::= \langle\rangle | \Gamma, x : A$</td></tr><tr><td>Signatures</td><td>$\Sigma ::= \langle\rangle | \Sigma, c : C | \Sigma, c := t : C | \Sigma, t \hookrightarrow v$</td></tr></table>

where c is a constant, x is a variable such that the sets of constants and variables are disjoint, and C is a closed term. Universes are constants used to verify if a type is well-formed – more details can be found in [17, §2.1]. $\Pi x : A, B$ is the dependent product (we write $A \to B$ when B does not depend on x), $\lambda x : A, t$ is an abstraction, and $t v$ is an application. A (local) context $\Gamma$ is a finite sequence of variable declarations $x : A$ introducing variables and their types. A signature $\Sigma$ representing the global context is a finite sequence of assumptions $c : C$, indicating that constant c is of type C, definitions $c := t : C$, indicating that c has value t and type C, and rewrite rules $t \hookrightarrow v$ such that $t = c v_1 \dots v_n$ where c is a constant.

The relation $\hookrightarrow_{\beta\Sigma}$ is generated by $\beta$-reduction and by the rewrite rules of $\Sigma$. The relation $\hookrightarrow_{\beta\Sigma}^*$ denotes the reflexive and transitive closure of $\hookrightarrow_{\beta\Sigma}$, and the relation $\equiv_{\beta\Sigma}$ (called conversion) the reflexive, symmetric, and transitive closure of $\hookrightarrow_{\beta\Sigma}$. The relation $\hookrightarrow_{\beta\Sigma}$ must be confluent, i.e., whenever $t \hookrightarrow_{\beta\Sigma}^* v_1$ and $t \hookrightarrow_{\beta\Sigma}^* v_2$, there exists some $w$ such that $v_1 \hookrightarrow_{\beta\Sigma}^* w$ and $v_2 \hookrightarrow_{\beta\Sigma}^* w$, and it must preserve typing, i.e., whenever $\Gamma \vdash_{\Sigma} t : A$ and $t \hookrightarrow_{\beta\Sigma} v$ then $\Gamma \vdash_{\Sigma} v : A$ [5].

A Lambdapi typing judgment $\Gamma \vdash_{\Sigma} t : A$ asserts that term $t$ has type $A$ in the context $\Gamma$ and the signature $\Sigma$. The typing rules of $\lambda\Pi/\equiv$ are those of $\lambda\Pi$ [17,
§2], except for the rule (Conv), given below, that identifies types modulo $\equiv_{\beta\Sigma}$ instead of just modulo $\beta$-reduction.

$$ \frac{\Gamma, \vdash_{\Sigma} B : u \quad \Gamma \vdash_{\Sigma} t : A \quad A \equiv_{\beta\Sigma} B}{\Gamma \vdash_{\Sigma} t : B} \quad (\text{Conv}) $$

In our encoding presented in [12], we employ Tarski-style universes [19] where types are represented by elements of a base type and interpreted via a decoding function. We define the constant **Prop**: **TYPE** for the type of propositions and the decoding function **Prf**<sup>c</sup>: **Prop** → **TYPE** that maps each proposition to **TYPE**. This is necessary because Lambdapi does not support quantification over a variable of type **TYPE**: it is not possible to assign the type $\Pi X$: **TYPE**, ($X \to \text{Prop}$) → $\text{Prop}$ to the universal quantifier $\forall$. To circumvent this, we have the constant **Set**: **TYPE** for the types of object-terms, and a decoding function **El**: **Set** → **TYPE** that embeds **Set** into **TYPE**. This allows us to define the universal quantifier as $\forall$: $\Pi x$: **Set**, ($\text{El } x \to \text{Prop}$) → $\text{Prop}$. To quantify over propositions, we further define a constant $o$: **Set** and add the rewrite rule **El** $o \leftrightarrow \text{Prop}$. This encoding is well-established in the literature on systems formalized in Lambdapi [7].

## 2.2 Alethe Proofs

The Alethe proof trace format [2] for SMT solvers comprises two parts: the trace language based on SMT-LIB and a collection of proof rules. Traces witness proofs of unsatisfiability of a set of constraints. They are sequences $a_1...a_m t_1...t_n$ where the assumptions $a_i$ correspond to the constraints of the original SMT problem being refuted, each $t_i$ is a clause inferred from previous elements of the sequence, and $t_n$ is $\perp$ (the empty clause). In the following, we designate the SMT-LIB problem as the *input problem*.

```
1 (set-logic LIA)
2 (declare-const x Int)
3 (declare-const y Int)
4 (assert (= x 2))
5 (assert (= 0 y))
6 (assert (or (< (+ x y) 1) (< 3 x)))
7 (check-sat)
8 (get-proof)
```

<caption>Listing 1.1. Input problem.</caption>

```
1 (assume a0 (or (< (+ x y) 1) (< 3 x)))
2 (assume a2 (= 0 y))
3 (assume a1 (= x 2))
4 (step t1 (cl (< (+ x y) 1) (< 3 x)) :rule or :premises (a0))
5 (step t2 (cl (not (< 3 x)) (not (= x 2))) :rule la_generic :args (1/1 -1/1))
6 (step t3 (cl (not (< 3 x))) :rule resolution :premises (a1 t2))
7 (step t4 (cl (< (+ x y) 1)) :rule resolution :premises (t1 t3))
8 (step t5 (cl (not (< (+ x y) 1)) (not (= x 2)) (not (= 0 y))))
9 :rule la_generic :args (1/1 1/1 -1/1))
10 (step t6 (cl) :rule resolution :premises (t5 t4 a1 a2))
```

<caption>Listing 1.2. Proof of unsatisfiability of the input problem of listing 1.1.</caption>
We will use the input problem shown in Listing 1.1 with its Alethe proof (found by cvc5) in Listing 1.2 as a running example to introduce Alethe concepts and illustrate our reconstruction of linear arithmetic step in Lambdapi.

*Overview of the Alethe Trace format.* An Alethe proof trace inherits the declarations of the corresponding input problem. All symbols (sorts, functions, assertions, etc.) declared or defined in the input problem remain declared or defined. Furthermore, the syntax for terms, sorts, and annotations uses the syntactic rules defined in SMT-LIB [3, §3] and the SMT signature context defined in [3, §5.1 and §5.2]. In the following we will represent an Alethe step as

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

A step consists of an index $i \in \mathbb{I}$ where $\mathbb{I}$ is a countable set of indices such as a0, t1), and a clause representing the disjunction of literals $l_1, \dots, l_n$. Steps that are not assumptions are justified by a proof rule $\mathcal{R}$ that depends on a possibly empty set of premises $\{p_1, \dots, p_m\} \subseteq \mathbb{I}$ that only contains earlier steps such that the proof forms a directed acyclic graph. A rule might also depend on a list of arguments $a_1, \dots, a_r$ where each argument $a_i$ is either a term or a pair $(x_i, t_i)$ for a variable $x_i$ and a term $t_i$. The interpretation of the arguments is rule-specific. The context $\Gamma$ of a step is a list $c_1, \dots, c_l$ where each element $c_j$ is either a variable or a variable-term tuple denoted $x_j \mapsto t_j$. Therefore, steps with a non-empty context contain variables $x_j$ that appear in $l_i$ and will be substituted by $t_j$. Proof rules $\mathcal{R}$ include theory lemmas and resolution, which corresponds to hyper-resolution on ground first-order clauses.

We now have the key components for explaining the proof in Listing 1.2. The proofs starts with **assume** steps a0, a1, a2 that restate the assertions from the input problem. Step t1 transforms the disjunction a0 into a clause by using the Alethe rule **or**. Steps t2 and t5 are tautologies introduced by the main rule **la_generic** in Linear Real Arithmetic (LRA) logic and also used in LIA logic, where $l_1, l_2, \dots, l_n$ represent linear inequalities. The **Real** terms in LRA and LIA logic are built over the **Real** and **Int** signatures from SMT-LIB with free variables, but containing only linear atoms; that is atoms of the form $d$, ($* d x$), or ($* x d$) where $x$ is a free variable and $d$ is an integer or rational constant. A linear inequality is an expression of the form

$$ \sum_{i=0}^{n} c_i \times t_i + d_1 \bowtie \sum_{i=n+1}^{m} c_i \times t_i + d_2 \quad (1) $$

where $\bowtie \in \{=, <, >, \leq, \geq\}$, $m \ge n$, $c_i, d_1, d_2$ are either **Int** or **Real** constants, and where $c_i$ and $t_i$ have the same sort for all $i$. Checking the validity of the clauses t2 and t5 in Listing 1.2 amounts to checking the unsatisfiability of a system of linear (in)equations e.g. $x < 3$ and $x = 2$ in t2. Coefficients for each
<table><caption>**Table 1.** Linear arithmetic rules in Alethe supported in our encoding.</caption><thead><tr><td>Rule</td><td>Description</td></tr></thead><tbody><tr><td>la generic</td><td>Tautologous disjunction of linear inequalities</td></tr><tr><td>lia generic</td><td>Tautologous disjunction of linear integer inequalities</td></tr><tr><td>la disequality</td><td>t<sub>1</sub> &asymp; t<sub>2</sub> &or; &not;(t<sub>1</sub> &ge; t<sub>2</sub>) &or; &not;(t<sub>2</sub> &ge; t<sub>1</sub>)</td></tr><tr><td>la totality</td><td>t<sub>1</sub> &ge; t<sub>2</sub> &or; t<sub>2</sub> &ge; t<sub>1</sub></td></tr><tr><td>la mult pos</td><td>t<sub>1</sub> &gt; 0 &and; (t<sub>2</sub> &boxtimes; t<sub>3</sub>) &rarr; t<sub>1</sub> * t<sub>2</sub> &boxtimes; t<sub>1</sub> * t<sub>3</sub> and &boxtimes; &isin; {&lt;, &gt;, &ge;, &le;, &asymp;}</td></tr><tr><td>la mult neg</td><td>t<sub>1</sub> &lt; 0 &and; (t<sub>2</sub> &boxtimes; t<sub>3</sub>) &rarr; t<sub>1</sub> * t<sub>2</sub> &boxtimes;<sub>inv</sub> t<sub>1</sub> * t<sub>3</sub></td></tr><tr><td>la rw eq</td><td>(t &asymp; u) &asymp; (t &ge; u &and; u &ge; t)</td></tr><tr><td>comp simplify</td><td>Simplification of arithmetic comparisons</td></tr><tr><td>arith-int-eq-elim</td><td>(t &asymp; s) &rarr; t &ge; s &and; t &le; s</td></tr><tr><td>arith-refl-geq</td><td>t &ge; t &rarr; &top;</td></tr><tr><td>arith-refl-lt</td><td>t &lt; t &rarr; &bottom;</td></tr><tr><td>arith-refl-leq</td><td>t &le; t &rarr; &top;</td></tr><tr><td>arith-elim-leq</td><td>t &le; s &rarr; s &ge; t</td></tr><tr><td>arith-elim-gt</td><td>t &gt; s &rarr; &not;(t &le; s)</td></tr><tr><td>arith-leq-norm</td><td>t &le; s &rarr; &not;(t &ge; s + 1)</td></tr><tr><td>arith-geq-norm1</td><td>t &ge; s &rarr; (t &minus; s) &ge; 0</td></tr><tr><td>arith-geq-norm2</td><td>t &ge; s &rarr; &minus;t &le; &minus;s</td></tr><tr><td>arith-geq-tighten</td><td>&not;(t &ge; s) &rarr; s &ge; t + 1</td></tr><tr><td>arith-poly-norm</td><td>polynomial normalization</td></tr><tr><td>evaluate</td><td>evaluate constant terms</td></tr></tbody></table>

inequality are passed as arguments e.g. $(\frac{1}{t}, \frac{1}{t})$ in t2. Steps t3 and t4 apply the **resolution** rule to the premises a1, t2 (respectively t1 and t3). Finally, the step t6 concludes the proof by generating the empty clause $\bot$, denoted as (c1) in Listing 1.2. Notice that the contexts $\Gamma$ of each step are all empty in this proof.

*Linear Arithmetic in Alethe.* Proofs for linear arithmetic steps use a number of rules listed in Table 1, such as `la_totality` that asserts totality of the ordering $\leq$. Besides arithmetical tautologies, the table also contains simplification rules, indicated with the symbol $\rightarrow$. Following our encoding of Alethe in Lambdapi as described in [12], the linear arithmetic rules `la_disequality`, `la_totality`, and `la_mult_*` are implemented as lemmas. We do not support the remaining arithmetic simplification rules, including the `la_tautology` rule from Alethe. This omission is primarily due to the fact that cvc5 extends Alethe with the RARE simplification rules [21], which it uses in place of the original ones. Consequently, we support the RARE rules prefixed by `arith-*`, as listed in Table 1, and we have selectively implemented those that appear in the proof traces of the benchmarks discussed in Sect. 6. In addition, support for the
evaluate rule is provided through the work described in Sect. 4, and support for arith-poly-norm is realized through the normalization approach explained in Sect. 5.

A different approach is taken for the rules la generic and lia generic , as they describe an algorithm. While the la generic rule is primarily intended for LRA logic, it is also applied in LIA proofs when all variables in the (in)equalities are of integer sort. A step of the rule la generic represents a tautological clause of linear inequalities. It can be checked by showing that the conjunction of the negated inequalities is unsatisfiable. After the application of some strengthening rules, the resulting conjunction is unsatisfiable, even if Int variables are assumed to be Real variables. Although the rule may introduce rational coefficients, they often reduce to integers—as shown in List. 1.2, where the coefficients are ( 1 $_{1}$, 1 $_{1}$). Cases where coefficients cannot be reduced to integers are rare in practice, however, we reduce them to integers by clearing denomina- tors with their least common denominator. Let ϕ$_{1}$, . . . , ϕ$_{n}$ be linear inequalities or their negations, but different from s$_{1}$ ≈ s$_{2}$ and a$_{1}$, . . . , a$_{n}$ rational numbers, then an la generic step has the general form

$$
i. \triangleright \varphi_1, \dots, \varphi_n \quad \mathbf{la\_generic} [a_1, \dots, a_n]
$$

The constants a_i are of sort Real. To check the unsatisfiability of the con-
junction ¬ϕ_1 ∧ ... ∧ ¬ϕ_n, one performs the following steps for each literal.

1. If $\varphi_i$ is of the form $s_1 \ge s_2$ or $\neg(s_1 < s_2)$, then let $\psi_i = s_2 > s_1$. If $\varphi_i$ is of the form $s_1 > s_2$ or $\neg(s_1 \le s_2)$, then let $\psi_i = s_2 \ge s_1$. If $\varphi_i$ is of the form $s_1 < s_2$ or $\neg(s_1 \ge s_2)$, then let $\psi_i = s_1 \ge s_2$. If $\varphi_i$ is of the form $\neg(s_1 \approx s_2)$, then let $\psi_i = s_1 \approx s_2$. This step produces a positive literal that is equivalent to $\neg\varphi_i$ and that only contains the operators $>$, $\ge$, and $\approx$.

2. Replace $\psi_i = \sum_{j=0}^{k_i} c_j^i \times t_j^i + d_1^i \bowtie \sum_{j=k_i+1}^{m_i} c_j^i \times t_j^i + d_2^i$ by the literal $(\sum_{j=0}^{k_i} c_j^i \times t_j^i) - (\sum_{j=k_i+1}^{m_i} c_j^i \times t_j^i) \bowtie d_2^i - d_1^i$.

3. Now $\psi_i$ has the form $s_1^i \bowtie d^i$. If all variables in $s_1^i$ are integer-sorted then replace $s_1^i > d^i$ by $s_1^i \ge \lfloor d^i \rfloor + 1$, respectively, replace $s_1^i \ge d^i$ by $s_1^i \ge \lfloor d^i \rfloor + 1$ if $d$ is not an integer.

4. If all variables of $\psi_i$ are integer-sorted and the coefficients $a_1 \dots a_n$ are in $\mathbb{Q}$, then $a_i := -a_i \times \text{lcd}(a_1 \dots a_n)$ where $\text{lcd}$ is the least common denominator of $\{a_1, \dots, a_n\}$.

5. If $\bowtie$ is $\approx$, then replace $\psi_i$ by $\sum_{j=0}^{m_i} a_i \times c_j^i \times t_j^i = a_i \times d^i$, otherwise replace $\psi_i$ by $\sum_{j=0}^{m_i} |a_i| \times c_j^i \times t_j^i \bowtie |a_i| \times d^i$.

6. Finally, the sum of the resulting literals is trivially contradictory,

$$
\sum_{i=1}^{n} \sum_{j=1}^{m_i} c_j^i * t_j^i \bowtie \sum_{i=1}^{n} d^i
$$
The operator $\triangleright$ is = if all operators are =, > if all are either $\approx$ or > (but at least one operator is different from $\approx$), and $\ge$ otherwise. Finally, the sum on the left-hand side is 0 and the right-hand side is > 0 (or $\ge$ 0 if $\triangleright$ is >).

The above algorithm is adapted from the Alethe specification [2], except that we clarified step 1: the subsequent steps in the original algorithm are designed for > and $\ge$ and do not clearly address how to handle < and $\le$. Additionally, we added step 4 in order to ensure that our construction is independent of $\mathbb{Q}$.

*Example 1.* Consider the following `la_generic` step in the logic `QF_UFLIA` with the uninterpreted function symbol (`f Int`):

$$ \begin{array}{l} 1 \quad (\mathit{step} \ t11 \ (\mathit{cl} \ (\mathit{not} \ (\leq \ f \ 0)) \ (\leq \ (+ \ 1 \ (\ast \ 4 \ f)) \ 1)) \\ 2 \quad :\mathit{rule} \ \mathit{la\_generic} \ :\mathit{args} \ (1/1 \ 1/4)) \end{array} $$

The algorithm then performs the following steps:

$$ -f \geq 0, 4 \times f > 0 \qquad (\text{Steps 1 and 2}) $$

$$ -f \geq 0, 4 \times f \geq 1 \qquad (\text{Step 3}) $$

$$ \text{Replace arguments } [\frac{1}{4}, \frac{1}{4}] \text{ by } [4, 1] \text{ due to clearing denominators} \qquad (\text{Step 4}) $$

$$ |4| \times (-f) \geq |4| \times 0, |1| \times 4 \times f \geq |1| \times 1 \qquad (\text{Step 5}) $$

$$ -4 \times f + 4 \times f \geq 1 \qquad (\text{Step 6}) $$

Which simplifies to the contradiction $0 \ge 1$.

*Remark 1.* The operator `to_real` is used in the LIA theory to embed integers into the reals. As a result, a proof for a problem formulated in LIA may involve reasoning over real numbers. Since our approach does not support the Real theory, we do not attempt to reconstruct such proofs and instead let the translation process fail in this case.

**Quantifiers in Linear Arithmetic.** The Alethe format defines rules for quantifier instantiation, Skolemization, substitution, and other manipulations of bound variables. For instance, the rule `forall_inst` is used to express quantifier instantiation. It produces a unit clause with a formula of the form $(\neg\forall\bar{x}, \varphi) \lor (\varphi[\bar{t}])$, where $\varphi$ is a term containing the free variables $\bar{x}$, and each term $t$ is a ground term of the same sort as the corresponding variable $x$. Accordingly, an Alethe proof will first instantiate the quantifier to produce a ground term, enabling subsequent arithmetic steps such as those involving `la_generic` or `lia_generic` to operate solely on ground terms.

## 3 Elaborating lia_generic Steps

The rule `lia_generic` is similar to `la_generic`, but the SMT solver does not provide the coefficients, i.e. $[a_1 \dots a_r]$ is empty. We decided to leverage the
elaboration process of lia_generic performed by Carcara, as doing otherwise would require implementing Fourier-Motzkin elimination for integers, as done in [4,22], hence reimplementing work that was already done by the solver.

Carcara considers lia_generic steps as holes in the proof, given that “their checking is as hard as solving” [1, §3.2]. To address this, Carcara invokes an external SMT solver, such as cvc5, or any tool capable of reading SMT-LIB input and producing Alethe proofs, and attempts to generate an Alethe proof that avoid using lia_generic. Suppose the resulting proof still includes a lia_generic step. In that case, Carcara repeats the process for up to three iterations, merging the final results if a complete proof without any lia_generic steps is eventually found. The proof is then imported and validated, replacing the original step.

*Example 2 (Sketch of lia_generic elaboration).* Consider a step S (Listing 1.3) concluding the clause $\neg l_1 \lor \dots \neg l_n$ where all $l_i$ are inequalities and proved by lia_generic rule.

1 (step S (cl (not l1) ... (not ln)) :rule lia_generic)

<caption>**Listing 1.3.** Elaborated proof</caption>

Carcara will generate an SMT-LIB problem asserting $l_1, \dots, l_n$ and invoke the solver cvc5 on it, expecting an Alethe proof of the unsatisfiability of $l_1 \land \dots \land l_n$ that does not use lia_generic. Carcara will check this subproof and then replace the original step by a proof of the form shown in Listing 1.4.

1 (anchor :step S.t_m+1)
2 (assume S.h_1 l1)
3 ...
4 (assume S.h_n ln)
5 ...
6 (step S.t_m (cl false) :rule ...)
7 (step t.t_m+1 (cl (not l1) ... (not ln) false) :rule subproof)
8 (step t.t_m+2 (cl (not false)) :rule false)
9 (step S (cl (not l1) ... (not ln))
:rule resolution :premises (S.t_m+1 S.t_m+2))
10

<caption>**Listing 1.4.** Elaboration of lia_generic</caption>

In Listing 1.4, steps S.h_1 until S.t_m are imported from the cvc5 proof. As a result the lia_generic step S in the original proof (Listing 1.3) will have been replaced by a detailed justification whose correctness can be independently established by Carcara.

# 4 Encoding of Linear Integer Arithmetic in Lambdapi

The definition of integers in Lambdapi that we use appears in Fig. 1. It follows a common encoding found in many other theories, including the one adopted in the Rocq standard library [26]. First, the type $\mathbb{P}$ is an inductive type representing strictly positive integers in binary form. Starting from 1 (represented by the constructor $H$), one can add a new least significant digit via the constructor $0$ (digit 0) or the constructor $I$ (digit 1). The type $\mathbb{Z}$ represents integers in
<figure><img src="image_75.png" /><figcaption>Fig. 1. Type definitions for binary positive number, integers, comparison and Booleans.</figcaption></figure>

<figure><img src="image_76.png" /><figcaption>Fig. 2. Definitions for operators over $\mathbb{Z}$.</figcaption></figure>

binary form. An integer is either zero (with constructor `Z0`) or a strictly positive number `Zpos` (coded as a $\mathbb{P}$) or a strictly negative number `Zneg`. We make use of Lambdapi's **builtin** mechanism to enable decimal notation for numeric values, allowing us to write, e.g., 2 instead of `ZPos(0H)`. We also introduce enumeration types `Comp` and $\mathbb{B}$ representing comparison operators and Booleans.

In order to enable quantification over elements of these types, we introduce constants such as `int`: `Set` that represent codes for these types along with a rule for rewriting codes to their corresponding types, for example `E1 int` $\leftrightarrow$ $\mathbb{Z}$. Figure 2 introduces operations on these types, including addition (`+`) and comparison (`$\doteq$`) over $\mathbb{Z}$. The auxiliary operations `add`, `sub`, and `cmp` implement addi-
tion, subtraction, and comparison for binary positive numbers; their definitions are not shown here for space restrictions. We also define the operations of multiplication (*) and subtraction (−) over $Z$. We will refer to the rewriting rules defining these operations as $\rightarrow_Z$ and $\rightarrow_P$ (for operations on $Z$ and $P$) in the following sections. The confluence of these rewriting rules has been proven using CSI [27]. We leverage these rewriting rules to perform the constant folding required by the `evaluate` rule, enabling the final proof step to be discharged by reflexivity.

Finally, we define inequality operators for $Z$ as binary predicates by reducing them to the decidable comparison $\doteq$. They reduce to $\top$, $\bot$ (or negated) by applying rules of $\rightarrow_Z$ and $\rightarrow_P$. For example, $1 < 2 \leftrightarrow \mathit{istrue}(\mathit{isLt}(1 \doteq 2)) \leftrightarrow \mathit{istrue}(\mathit{isLt}(L_t)) \leftrightarrow \mathit{istrue}(\mathit{true}) \leftrightarrow \top$.

We use this encoding of integer operations for extending our existing embedding of Alethe proofs in Lambdapi [12]. In particular, the SMT sort `Int` is mapped to `El int`, and the arithmetic operations of SMT to their counterparts in the Lambdapi encoding. The following section describes how we leverage this representation of integers in Lambdapi to simulate the algorithm presented in Sect. 2.2 for checking applications of the rule `la generic`.

# 5 Reconstruction of Linear Arithmetic for LIA Logic

Proof by reflection [10] is a technique for writing certified procedures for automated reasoning. It reduces the validity of a logical statement to a symbolic computation. Let $P: Z \rightarrow \mathit{Prop}$ be a predicate over a data type $Z$ and $f: Z \rightarrow \mathit{bool}$ be a function such that the following theorem holds:

$$f\_correct: \forall z: Z, (f z = \mathit{true}) \rightarrow (P z)$$

If $f z$ reduces to `true`, then the proof term $f\_correct z$ (`refl bool true`) with `refl`: $\Pi A: \mathit{Set}$, $\Pi x: \mathit{El A}$, $\mathit{Prf}^c(x = x)$, constitutes a proof of predicate $(P z)$. In step 6 of checking an application of rule `la generic`, the primary challenge lies in reasoning modulo associativity and commutativity when manipulating expressions over $Z$. The key idea is to provide a normalization function that transforms a $Z$ expression into a canonical form.

## 5.1 Representation

The procedure is based on an algebraic group structure, denoted as $G$ defined in Fig. 3, which represents linear polynomials. The base type for its elements is $G$: `TYPE`. The unary operator `cst` injects constants from $Z$ into $G$. The term `var c x` is intended for representing expressions $c \times x$ that appear as constituents of linear inequalities, where $c$ is an integer coefficient and $x$ a $Z$ term, in particular a variable. The constructor `mul` represents the multiplication of an element of $G$ by a constant. The constructor `opp` corresponds to unary minus. Lastly, the constructor $\oplus$ represents the addition of two elements of $G$.
<figure><img src="image_77.png" /><figcaption>Fig. 3. Definition of $\mathcal{G}$ Algebra and its reification ($\Uparrow$) and denotation ($\Downarrow$) functions.</figcaption></figure>

Lambdapi provides modifiers for supporting associative and commutative operations, ensuring that terms are systematically transformed into a canonical form w.r.t. a builtin ordering relation [6,8]. We declare the operator $\oplus$ as associative commutative, ensuring that expressions involving sums of elements of $\mathcal{G}$ are systematically canonicalized.

## 5.2 Associative Commutative Normalization

The transformation to canonical form implemented in Lambdapi ensures that sum expressions of the form

$$ (\mathbf{var} c_1 x_1) \oplus (\mathbf{cst} k_1) \oplus (\mathbf{var} c_2 x_2) \oplus \dots \oplus (\mathbf{cst} k_m) \oplus \dots \oplus (\mathbf{var} c_n x_n) $$

will be normalized such that any pair of terms $(\mathbf{var} c x)$ and $(\mathbf{var} d x)$ involving the same variable $x$ are placed next to each other, and all $(\mathbf{cst} k)$ will be placed at the left before the first variable $(\mathbf{var} c x)$. We will use the rewriting rules shown in Fig. 4 for reducing $\mathcal{G}$ expressions. Notably, the resulting normal forms do not contain the constructors `mul` and `opp`, as the associated rewrite rules eliminate them in favor of `var`, `add` and `cst`.

**Definition 4.** The $\le$ builtin total order on $\mathcal{G}$-terms is defined as follows: Terms are ordered such that $\mathbf{cst}(c_1) \le \mathbf{cst}(c_2) < (\mathbf{var} c x)$ for any constants $c_1 \le c_2$ and any variable term $(\mathbf{var} c x)$. For variable terms, $(\mathbf{var} c x) \le (\mathbf{var} d x)$ if either $x < y$, or $x = y$ and $c \le d$. Let $\rightarrow^{AC}$ be the relation mapping every term $t$ to its unique AC-canonical form denoted $[t]$.

Two terms $t$ and $u$ are AC-equivalent (written $t \simeq_{AC} u$) iff their AC-canonical forms are equal.
$$ (\mathbf{var} c_1 x) \oplus (\mathbf{var} c_2 x) \hookrightarrow (\mathbf{var} (c_1 + c_2) x) \qquad (2) $$

$$ (\mathbf{var} c_1 x) \oplus ((\mathbf{var} c_2 x) \oplus y) \hookrightarrow (\mathbf{var} (c_1 + c_2) x) \oplus y \qquad (3) $$

$$ (\mathbf{cst} c_1) \oplus (\mathbf{cst} c_2) \hookrightarrow (\mathbf{cst} (c_1 + c_2)) \qquad (4) $$

$$ (\mathbf{cst} c_1) \oplus ((\mathbf{cst} c_2) \oplus y) \hookrightarrow (\mathbf{cst} (c_1 + c_2)) \oplus y \qquad (5) $$

$$ (\mathbf{cst} 0) \oplus x \hookrightarrow x \qquad (6) $$

$$ x \oplus (\mathbf{cst} 0) \hookrightarrow x \qquad (7) $$

$$ \mathbf{opp} (\mathbf{var} c x) \hookrightarrow (\mathbf{var} (-c) x) \qquad (8) $$

$$ \mathbf{opp} (\mathbf{cst} c) \hookrightarrow (\mathbf{cst} (-c)) \qquad (9) $$

$$ \mathbf{opp} (\mathbf{opp} x) \hookrightarrow x \qquad (10) $$

$$ \mathbf{opp} (x \oplus y) \hookrightarrow (\mathbf{opp} x) \oplus (\mathbf{opp} y) \qquad (11) $$

$$ \mathbf{opp} (\mathbf{mul} k x) \hookrightarrow \mathbf{mul} (-k) x \qquad (12) $$

$$ \mathbf{mul} k (\mathbf{var} c x) \hookrightarrow (\mathbf{var} (k * c) x) \qquad (13) $$

$$ \mathbf{mul} k (\mathbf{opp} x) \hookrightarrow \mathbf{mul} (-k) x \qquad (14) $$

$$ \mathbf{mul} k (x \oplus y) \hookrightarrow (\mathbf{mul} k x) \oplus (\mathbf{mul} k y) \qquad (15) $$

$$ \mathbf{mul} k (\mathbf{cst} c) \hookrightarrow (\mathbf{cst} (k * c)) \qquad (16) $$

$$ \mathbf{mul} c_1 (\mathbf{mul} c_2 x) \hookrightarrow \mathbf{mul} (c_1 * c_2) x \qquad (17) $$

<caption>**Fig. 4.** Rewrite system on canonical forms.</caption>

**Definition 5.** The relation $\rightarrow_{\Sigma}^{AC}$ is defined as $\hookrightarrow_{\Sigma} \rightarrow^{AC}$, where $\Sigma$ contains the rewrite rules of Figs. 2 and 4.

An $\rightarrow_{\Sigma}^{AC}$ step is a standard $\hookrightarrow_{\Sigma}$ step with syntactic matching followed by AC-canonicalization. We now prove that the relation $\rightarrow_{\Sigma}^{AC}$ terminates and is confluent.

**Lemma 6.** The relation $\rightarrow_{\Sigma/AC} = \simeq_{AC} \hookrightarrow_{\Sigma} \simeq_{AC}$ of matching modulo AC, which contains $\rightarrow_{\Sigma}^{AC}$, terminates.

*Proof.* AProVE [15] automatically proves the termination of $\rightarrow_{\Sigma/AC}$. $\square$

**Lemma 7.** $\rightarrow_{\Sigma}^{AC}$ is locally confluent on AC-canonical terms.

*Proof.* We show that every critical pair is joinable using $\rightarrow_{\Sigma}^{AC}$ and confluence of $\rightarrow_{\Sigma}$ and $\rightarrow_{\mathbb{P}}$. $\square$

We compare two $\mathbb{Z}$-terms $t_1$ and $t_2$ wrt $\rightarrow_{\Sigma}^{AC}$ by reifying them into their corresponding $\mathbb{G}$-terms, denoted $[g_1]$ and $[g_2]$, using the reification function $\upharpoonright$, and normalizing them using $\rightarrow^{AC}$. Following the reduction rules specified in Fig. 4, we can then compare their corresponding $\mathbb{Z}$-terms by applying the denotation function $\downharpoonright$. To validate this procedure, it is necessary to establish the correctness
of the following diagram, formally expressed by Theorem 8.

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

**Theorem 8 (Correctness of normalization).** For all $\mathbb{G}$-terms $t$, we have $(\downarrow[t]) = (\downarrow t)$ where $[t]$ is the AC-canonical form of $t$ with respect to $\xrightarrow{\Sigma^{AC}}$.

*Proof.* The proof proceeds by induction on $t$, and the key case is the one where $t = t_1 \oplus t_2$. We have to show that $\downarrow[t_1 \oplus t_2] = (\downarrow t_1) + (\downarrow t_2)$. By the induction hypothesis, we have $\downarrow[t_1] = \downarrow t_1$ and $\downarrow[t_2] = \downarrow t_2$. Hence,

$$ (\downarrow t_1) + (\downarrow t_2) = (\downarrow [t_1]) + (\downarrow [t_2]) = \downarrow ([t_1] \oplus [t_2]) $$

It remains to show that $\downarrow([t_1] \oplus [t_2]) = \downarrow[t_1 \oplus t_2]$. Now, $[t_1]$, $[t_2]$, and $[t_1 \oplus t_2]$ are terms built solely from `cst`, `var`, and $\oplus$ since the remaining operators have been eliminated by applying the rules in Fig. 4, and the terms on both sides of the equation contain the same multisets of subterms. The two terms are therefore identified by AC-canonicalization. $\square$

We make use of Lemma 9 to embed $\mathbb{Z}$-terms into $\mathbb{G}$ for normalization and subsequent comparison. In addition, we leverage this normalization process to support the `arith-poly-norm` rule.

**Lemma 9 (Conversion).** For all $x: \mathbb{Z}$, we have $x = (\downarrow(\uparrow x))$.

*Proof.* By induction on $x$. We consider the three cases: $x = \mathbb{ZPos}(n)$, $x = \mathbb{ZNeg}(n)$, and $x = \mathbb{Z0}$. In each case, $\uparrow(x)$ yields the corresponding constant (cst $x$), and by definition of the denotation function, $x = \downarrow((cst x))$. Hence, $x = (\downarrow(\uparrow x))$ in all cases. $\square$

```
1   opaque symbol t2: Prf* ((¬ (3 < x) ∨c ¬ (x = 2)) ∨ ■) {
2     apply ∨c i1;
3   rewrite Zinv_lt_eq;
4   rewrite Z_diff_gt_Z0_eq (∼ 3) (∼ x);
5   rewrite Z_diff_eq_Z0_eq (x) 2;
6   rewrite Zgt_le_succ_r_eq ((∼ 3) - (∼ x)) 0;
7   rewrite Zmult_ge_compat_eq 1 ((∼ 3) - (∼ x)) ((0 + 1));
8   rewrite Zmult_eq_compat_eq (∼ 1) (x - 2) 0;
9   rewrite imp_eq_or; apply ⇒c i; assume H0; apply ¬c i; assume H1;
10  set H0' := (1 * ((∼ 3) - (∼ x))); set H0r := (1 * (0 + 1));
11  set H1' := ((∼ 1) * (x - 2)); set H1r := ((∼ 1) * 0);
12  have H1': Prf<sup>c</sup> (H1' ≥ H1r) { refine Z_eq_implies_ge H1 }; remove H1;
13  have contra : Prf<sup>c</sup> ((↓(↑(H0' + H1')) ≥ (↓(↑(H0r' + H1r')))){
14    rewrite ∨_⊥; rewrite ∨_⊥;
15    apply (Zsum_geq_s H0' H0r' H1' H1r' H0 H1');
16  };
17  apply (⇒<sup>c</sup> e' contra); apply ⊢<sup>c</sup> i;
18};
```

<caption>Listing 1.5. Lambdapi proof of Listing 1.2</caption>
<table><caption>**Table 2.** Benchmark results.</caption><thead><tr><th>Logic</th><th>Benchmark</th><th>Samples</th><th>Proofs</th><th>Elaborate</th><th>Translate</th><th>Check</th></tr></thead><tbody><tr><td rowspan="4">LIA</td><td>tptp</td><td>36</td><td>36 - 0 - 0</td><td>36 - 0</td><td>36 - 0 - 0</td><td>28 - 8 - 0</td></tr><tr><td>Ultimate</td><td>153</td><td>120 - 0 - 33</td><td>73 - 47</td><td>68 - 5 - 0</td><td>50 - 18 - 0</td></tr><tr><td>Svcomp'19</td><td>27</td><td>27 - 0 - 0</td><td>25 - 2</td><td>0 - 25 - 0</td><td>0</td></tr><tr><td>psyco</td><td>50</td><td>48 - 0 - 2</td><td>48 - 0</td><td>43 - 0 - 5</td><td>0 - 37 - 6</td></tr><tr><td rowspan="3">QFLIA</td><td>SMPT</td><td>1568</td><td>1529 - 39 - 0</td><td>1497 - 32</td><td>1476 - 0 - 21</td><td>804 - 638 - 34</td></tr><tr><td>rings</td><td>294</td><td>70 - 1 - 223</td><td>49 - 21</td><td>49 - 0 - 0</td><td>7 - 0 - 42</td></tr><tr><td>CAV2009</td><td>85</td><td>85 - 0 - 0</td><td>19 - 66</td><td>19 - 0 - 0</td><td>19 - 0 - 0</td></tr><tr><td rowspan="2">UFLIA</td><td>sledgeh</td><td>1521</td><td>1343 - 0 - 178</td><td>1278 - 65</td><td>1258 - 13 - 7</td><td>711 - 467 - 80</td></tr><tr><td>tokeneer</td><td>1732</td><td>1732 - 0 - 0</td><td>1689 - 43</td><td>1689 - 0 - 0</td><td>1482 - 197 - 10</td></tr></tbody></table>

We present in Listing 1.5 the translation of Step t2 from Listing 1.2 using our Carcara module. The `rewrite Zinv_lt_eq` step at line 3 performs the normalization from Step 1, rewriting $\neg(3 < x)$ as $\neg(\sim 3 > \sim x)$. The lemmas $Z_diff_gt_Z0$ and $Z_diff_eq_Z0_eq$ (lines 4–5) implement Step 2. Since the goal involves a > inequality, Step 3 applies with the lemma `Zgt_le_r_eq` (line 6). The coefficients $[\frac{1}{1}, -\frac{1}{1}]$ from Step 4 are trivially cast to $\mathbb{Z}$ and applied in lines 7–8. To express all inequalities uniformly, remaining equalities are rewritten as $\ge$ using $Z_eq_implies_ge$ (line 12). Finally, Step 6 derives the contradiction by summing inequalities from lines 13 to 17.

# 6 Evaluation

Our benchmark suite shown in Table 2 is composed of files from the SMT-LIB benchmarks<fnref n="1" />. The suite includes a total of 5,466 samples drawn from 9 benchmark categories spanning three SMT-LIB logics: LIA, QFLIA, and UFLIA that correspond to those covered by our method. Within the logics QFLIA and UFLIA, we prioritized benchmarks with the most significant number of available samples. Table 2 provides a detailed breakdown of the benchmarks and the corresponding results. The *Logic* column indicates the SMT theory used, while the *Benchmark* column lists abbreviated benchmark names. The column *Samples* describes the number of problems available with status *unsat*. Each of the columns *Proofs*, *Translate*, and *Check* reports a triple in the format *success - error - timeout*, representing respectively the number of successful executions, failed attempts, and timeouts. The *Proofs* column reports the number of proofs generated by cvc5² that do not contain the `to_real` cast operator. The *Elaborate* column shows a pair of values: the number of proofs that were successfully elaborated by Carcara, and the number that failed. Only proofs successfully elaborated by Carcara are considered for translation. The *Translate* column gives

<footnote n="1">¹ https://smtlib.cs.uiowa.edu/benchmarks.shtml.</footnote>

<footnote n="2">² cvc5 version 1.2.1-dev.144.38fcc340e5 [git 38fcc340e5 on branch main].</footnote>
<table><caption>**Table 3.** Lambdapi checking times in milliseconds.</caption><thead><tr><th>Bench</th><th>Min</th><th>Q1</th><th>Mean</th><th>Q3</th><th>Max</th></tr></thead><tbody><tr><td>tptp</td><td>240</td><td>262</td><td>263</td><td>267</td><td>336</td></tr><tr><td>Ultimate</td><td>82</td><td>96</td><td>100</td><td>111</td><td>346</td></tr><tr><td>SMPT</td><td>52</td><td>55</td><td>55</td><td>56</td><td>293</td></tr><tr><td>rings</td><td>670</td><td>704</td><td>773</td><td>826</td><td>1197</td></tr><tr><td>CAV2009</td><td>54</td><td>296</td><td>403</td><td>498</td><td>683</td></tr><tr><td>sledgeh</td><td>53</td><td>166</td><td>354</td><td>552</td><td>1594</td></tr><tr><td>tokeneer</td><td>55</td><td>60</td><td>61</td><td>248</td><td>753</td></tr></tbody></table>

the number of proof traces successfully translated into Lambdapi proofs, while the *Check* column indicates the number of these translated proofs that were successfully type-checked by Lambdapi.

We enforced a timeout of 30 s for cvc5 to find a proof and 30 s for the translation step with Carcara. No timeout was imposed during the elaboration step, as the runtime is negligible. A timeout of 20 s was set for Lambdapi when type-checking the final proofs to ensure that proof verification remains as fast as possible.<fnref n="3" />

All nine benchmarks demonstrated consistently reliable proof generation, with few or no timeouts, except for the *rings* benchmark. The elaboration phase was generally robust, except in the *Ultimate* benchmark, where an error in the elaborator caused failures. For LIA, performance in the translation and checking stages was mixed. In particular, for *Svcomp'19* and *psyco*, no or few proofs could be translated or verified, mainly due to currently unsupported simplification rules involving the *ite* operator. The QFLIA benchmarks exhibited more reliable proof checking in *SMPT* and *CAV2009*, while only a small number of proofs from the *rings* benchmark were successfully checked. The errors encountered during the elaboration of the *CAV2009* come from a bug in the elaborator. Since the samples in this benchmark are derived from a common base problem while increasing in size, the bug propagated across all samples that depend on the same base instance. The limited success with checking proofs in the *rings* category is due to the presence of *la_generic* terms with hundreds of uninterpreted variables; the current normalization mechanism, described in Sect. 5.2, relies on a built-in term ordering that is not sufficiently efficient in this setting. Benchmarks under UFLIA performed better throughout the pipeline. Most proofs were successfully generated and elaborated, and a large portion were translated and verified by Lambdapi, particularly in the *tokeneer* dataset. The higher number of errors in *SMPT* and *sledgeh* is primarily due to unsupported RARE rules related to the *QF UF* logic, as well as unhandled cases in the *evaluate* rule for LIA and *QF UF*.

<footnote n="3">³ All benchmarks were executed in parallel using GNU parallel [25] with an Apple silicon M2.</footnote>
Table 3 reports the Lambdapi proof-checking times in milliseconds, presenting the minimum, first quartile (Q1), mean, third quartile (Q3), and maximum durations for each benchmark. In most cases, the checking time remains below one second.

# 7 Related Work

The reconstruction for Alethe proofs produced by the veriT solver has been implemented within Isabelle/HOL [23] to enhance the reconstruction success rate compared to Z3. Concerning linear arithmetic reasoning, they also follow the algorithm described in Sect. 2.2, relying on Isabelle’s simplifier (which supports reasoning modulo associativity and commutativity) for normalizing expressions.

Besson [4] introduces a modular framework for integrating SMT solvers with the Rocq proof assistant, emphasizing the generation and efficient verification of proof certificates directly within Coq. His approach enables fast, reflexive proof checking using Nelson-Oppen-style theory combination, and it supports both Linear Integer Arithmetic (LIA) and Linear Real Arithmetic (LRA) logics. To efficiently generate Farkas certificates for LA, the technique relies on the Simplex algorithm, while for LIA, a variant of the Omega test [22] is adopted. The technique has been evaluated on SMT-LIB 2 benchmarks using the Z3 solver.

Compared to these approaches, which demonstrate stronger scalability in handling larger and more complex systems of inequalities, our method does not yet scale as well, in particular for cases that require significant arithmetic simplification. As shown in Sect. 6, performance degrades on benchmarks such as *rings*, where large instances of rule *la_generic* are generated. Nevertheless, our framework offers the advantage of supporting proof export from Lambdapi to other systems. This interoperability enables the reuse of valid SMT proofs in external environments such as Rocq.

# 8 Conclusion

We presented an extension of Carcara’s [1]<fnref n="4" /> translation module [12] for reconstructing arithmetic reasoning steps in Alethe proof traces involving linear arithmetic reasoning in the foundational proof assistant Lambdapi [18]. The translation module enables the export of an Alethe proof, together with its input problem, parsed and elaborated by Carcara, into a Lambdapi file that can be independently verified using the Lambdapi compiler and the Lambdapi library included in Carcara, which encodes Alethe logic. Building on this module, our extension introduces support for exporting arithmetic proof steps and extends the Lambdapi Alethe library to incorporate integer arithmetic proof rules. Our method includes a ring solver inspired by the computational reflection techniques described in [10,16].

<footnote n="4">⁴ https://github.com/NotBad4U/carcara/tree/lambdapi-translate.</footnote>
We have shown that this allows us to reconstruct several thousand SMT
proofs that originate from the SMT-lib Benchmarks. To the best of our knowl-
edge, this is the first work to automatically solve arithmetic goals in Lambdapi.
Nonetheless, the current implementation does not yet scale well in arithmetic-
heavy cases. As future work, we plan to improve Lambdapi's built-in normaliza-
tion mechanism to better handle such cases. We also intend to extend our work to
support rational and real arithmetic, enabling verification of broader fragments
of linear arithmetic (LRA) theories. This will in particular require an encoding
of rational and real arithmetic in Lambdapi and their normalization function,
based on the *gcd* operator, as a basis for implementing proof by reflection.

References

1. Andreotti, B., Lachnitt, H., Barbosa, H.: CARCARA: an efficient proof checker and elaborator for SMT proofs in the Alethe format. In: Sankaranarayanan, S., Sharygina, N. (eds.) TACAS 2023. LNCS, vol. 13993, pp. 367–386. Springer, Cham (2023). https://doi.org/10.1007/978-3-031-30823-9_19

2. Barbosa, H., Fleury, M., Fontaine, P., Schurr, H.J.: The Alethe proof format an evolving specification and reference (2024). https://verit.gitlabpages.uliege.be/alethe/specification.pdf

3. Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB standard: version 2.7. Technical report, Department of Computer Science, The University of Iowa (2017–2024). https://smt-lib.org/papers/smt-lib-reference-v2.7-r2025-07-07.pdf

4. Besson, F.: Fast reflexive arithmetic tactics the linear case and beyond. In: Altenkirch, T., McBride, C. (eds.) TYPES 2006. LNCS, vol. 4502, pp. 48–62. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-74464-1_4

5. Blanqui, F.: Type safety of rewrite rules in dependent types. In: 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), vol. 167, pp. 13:1–13:14 (2020)

6. Blanqui, F.: Encoding type universes without using matching modulo associativity and commutativity. In: Felty, A.P. (ed.) 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), vol. 228, pp. 24:1–24:14 (2022)

7. Blanqui, F., Dowek, G., Grienenberger, E., Hondet, G., Thiré, F.: Some axioms for mathematics. In: 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), vol. 195, pp. 20:1–20:19. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl (2021)

8. Blanqui, F., Hardin, T., Weis, P.: On the implementation of construction functions for non-free concrete data types. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 95–109. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-71316-6_8

9. Blanqui, F.: Translating HOL-light proofs to Coq. In: Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning. EPiC Series in Computing, vol. 100, pp. 1–18 (2024)

10. Boutin, S.: Using reflection to build efficient and certified decision procedures. In: Abadi, M., Ito, T. (eds.) TACS 1997. LNCS, vol. 1281, pp. 515–529. Springer, Heidelberg (1997). https://doi.org/10.1007/BFb0014565
11. Bromberger, M., Sturm, T., Weidenbach, C.: A complete and terminating approach to linear integer solving. J. Symb. Comput. **100**, 102–136 (2020). https://doi.org/10.1016/J.JSC.2019.07.021

12. Coltellacci, A., Merz, S., Dowek, G.: Reconstruction of SMT proofs with Lambdapi. In: Proceedings of the 22nd International Workshop on Satisfiability Modulo Theories Co-located with the 36th International Conference on Computer Aided Verification (CAV 2024). CEUR Workshop Proceedings, vol. 3725, pp. 13–23. CEUR-WS.org, Montreal (2024)

13. Cousineau, D., Dowek, G.: Embedding pure type systems in the lambda-pi-calculus modulo. In: Della Rocca, S.R. (ed.) TLCA 2007. LNCS, vol. 4583, pp. 102–117. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-73228-0_9

14. Dutertre, B., de Moura, L.: Integrating simplex with DPLL(T). Technical report CSL-06-01, SRI International (2006). https://yices.csl.sri.com/papers/sri-csl-06-01.pdf

15. Giesl, J., et al.: Proving termination of programs automatically with AProVE. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS (LNAI), vol. 8562, pp. 184–191. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08587-6_13

16. Grégoire, B., Mahboubi, A.: Proving equalities in a commutative ring done right in Coq. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol. 3603, pp. 98–113. Springer, Heidelberg (2005). https://doi.org/10.1007/11541868_7

17. Harper, R., Honsell, F., Plotkin, G.D.: A framework for defining logics. J. ACM **40**, 143–184 (1993). https://apisemanticscholar.org/CorpusID:13375103

18. Hondet, G., Blanqui, F.: The new rewriting engine of Dedukti. In: 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), vol. 167, pp. 35:1–35:16. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl (2020)

19. Martin-Löf, P.: Intuitionistic type theory (1980)

20. 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

21. Nötzli, A., Barbosa, H., Niemetz, A., Preiner, M., Reynolds, A., Barrett, C., Tinelli, C.: Reconstructing fine-grained proofs of rewrites using a domain-specific language. In: FMCAD 2022, pp. 65–74 (2022). https://doi.org/10.34727/2022/isbn.978-3-85448-053-2_12

22. Pugh, W.: The Omega test: a fast and practical integer programming algorithm for dependence analysis. In: Proceedings of the 1991 ACM/IEEE Conference on Supercomputing, pp. 4–13 (1991)

23. Schurr, H.-J., Fleury, M., Desharnais, M.: Reliable reconstruction of fine-grained proofs in a proof assistant. In: Platzer, A., Sutcliffe, G. (eds.) CADE 2021. LNCS (LNAI), vol. 12699, pp. 450–467. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-79876-5_26

24. Schurr, H.J., Fleury, M., Barbosa, H., Fontaine, P.: Alethe: towards a generic SMT proof format (extended abstract). In: Electronic Proceedings in Theoretical Computer Science, vol. 336, pp. 49–54 (2021)

25. Tange, O.: GNU parallel 20250322 (2025). https://doi.org/10.5281/zenodo.15071920. GNU Parallel is a general parallelizer to run multiple serial command line programs in parallel without changing them

26. The Rocq Development Team: The Rocq reference manual – release 9.0.0 (2025). https://rocq-prover.org/doc/V9.0.0/refman/index.html
27. Zankl, H., Felgenhauer, B., Middeldorp, A.: CSI – a confluence tool. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS (LNAI), vol. 6803, pp. 499–505. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22438-6_38

**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_79.png" /></figure>
# Certifying rlive: A New Proof Strategy for Liveness Model Checking

Giulia Sindoni(✉)D, Alberto Griggio(✉)D, and Stefano Tonetta(✉)D

Fondazione Bruno Kessler, Trento, Italy

`{gsindoni,griggio,tonettas}@fbk.eu`

**Abstract.** SAT-based model checking has become a prominent approach to the verification of temporal properties. However, while invariant model checking can produce simple proofs based on induction, proof generation for SAT-based model checking of liveness properties is much more complex.

In this paper, we focus on a recently developed algorithm, called rlive, which has been proved quite effective in practice. rlive tries to find a counterexample with a series of reachability checks, while iteratively blocking shoals, i.e., set of states that cannot be extended with fair paths. Despite the complexity of the algorithm, we show that the shoals are sufficient to generate a proof in a deductive system for temporal properties. We implement the approach in an existing certifying model checking framework based on the PVS theorem prover, and we experimentally evaluate it on liveness verification problems from the hardware model checking competition, generating proofs using the nuXmv model checker and checking them with PVS.

## 1 Introduction

Applying formal methods as a tool for certifying high-assurance and safety-critical systems demands for verification tools that are capable of providing a high level of confidence in their outcomes.

A model checker generally offers a straightforward “yes” or “no” answer when addressing a verification problem. When the answer is “no” the model checker provides a counterexample as supporting evidence. No such evidence is usually given when the answer is “yes”. Moreover, the growing complexity of model checkers themselves has made it increasingly important to obtain certificates from their process. The idea of certifying model checking [19] is to generate certificates as a byproduct of the verification. These certificates, often in the form of deductive proofs, serve to build trust in the verification results by providing additional evidence of correctness.

In this paper we consider problem of certifying the liveness checking problem, denoted $M = FGq$ where $FGq$ intuitively means that, in any satisfying trace, $q$ eventually holds in all the future states. More specifically, we focus on rlive [30], a new SAT-based model-checking algorithm for the verification of liveness properties of finite-state symbolic transition systems, which has been proved quite
effective in practice. rlive tries to find a counterexample with a series of reachability checks, while iteratively blocking a set of shoals, i.e. set of states that cannot reach a $\neg q$-state infinitely often.

We show that, despite the complexity of this algorithm, the shoals are sufficient to generate certifying proofs for the liveness property in a deductive system. The shoals are easily provided by the model checker, in the case where this has verified that the model satisfies the liveness property.

Our starting point is the approach presented in [15], describing a method for the generation of liveness checking certificates using the *k*-liveness algorithm [9]. The key idea of *k*-liveness is it prove that a liveness property holds, by bounding how many times *q* can be false. For any valid liveness property in a finite-state transition system, there exists a bound *k* such that *q* can become false at most *k* times in any trace. The algorithm incrementally searches for this bound (*k* = 0, 1, 2, ...), using a SAT-based safety checker to verify each bound until one succeeds. In this paper, we adapt and generalise the certification procedure for *k*-liveness of [15] to make it applicable also to rlive. We then extend our previous work of [28], where we presented a theorem prover based certification framework for invariant properties, to handle liveness proofs.

More specifically, we make the following contributions:

1. The formalisation of new temporal deductive rule capturing rlive. We formally prove the correctness and completeness of the rule. This rule is a generalisation of the temporal rule for *k*-liveness presented in [15]. The correctness result is proved within a deductive proof system developed in the PVS specification language [26], so that it can be used within an automated proof strategy.

2. The development of a proof strategy for certifying the success of the model checking answer “yes”, when the model checker has used rlive to show that the model satisfies the liveness property. This strategy only takes as input the set of shoals, which are created during the model checking stage.

We experimentally evaluate our approach on liveness verification problems from the hardware model checking competition, generating proofs using the nuXmv model checker [7] and checking them with PVS.

**Outline.** The rest of the paper is organised as follows. Section 2 provides an overview of related work. Section 3 introduces notation and background notions. Section 4 describes our contribution at formalising rlive as a temporal deductive rule and at generating proofs for certifying liveness checking results using rlive. Section 5 reports an evaluation of the prototype implementation of the proof strategy on a standard set of benchmarks for liveness checking. Section 6 concludes the paper.

## 2 Related Work

This work builds upon the concepts first presented in [15], where it was shown how to exploit the *k*-liveness algorithm to extend proof generation capabilities
for invariant checking to cover full linear-temporal logic (LTL) properties, with
little overhead for the model checker. The work shows how *k*-liveness can be
formalised as a temporal deductive rule and its correctness proved within a
complete axiomatic system for LTL from [13]. However, in that case no theorem
prover was used to check the proof generated by the model checker.

In [28] the authors fill this gap by presenting a novel approach for certifying
model checking results exploiting a theorem prover, namely PVS, and a theory of
temporal deductive rules that can support various kinds of transformations and
simplifications of the original model, such as 2-phase abstraction and temporal
decomposition. This work was however restricted in that it can only handle the
proof of invariant properties.

The present work builds upon the theorem-prover based approach from [28],
by showing how to certify model checking results for liveness properties, specifi-
cally when the model checker uses the newly introduced *rlive* algorithm to prove
the property at issue. Even though *rlive* looks as a very different algorithm from
*k*-liveness, the proof of the first turns out to be a generalisation of the latter
presented in [15].

A different approach to certification is presented in [31], where a formal
framework designed to certify model checking results based on *k*-induction is
described. The core of this certification process is the creation of a witness circuit
which simulates the original circuit, and which includes an inductive invariant
that serves as a proof certificate. This approach is extended further in [4] and [12].
The framework is however limited to the certification of invariants, and doesn't
consider liveness or general LTL properties.

A relevant approach to certifying the correctness of liveness properties specif-
ically is presented in [16]. The authors present a variant of the liveness-to-safety
algorithm [1], and transform the liveness property into a safety property using a
reduction. Then they get a proof for that safety property. However, this reduction
has to be trusted as correct, and the proof does not target the original system,
but the result of the reduction. In our work, we produce a temporal proof of
the fact that the original system satisfies the property, so that only the theorem
prover performing the proof, and not the model checking algorithms used, has
to be trusted.

Other approaches concerning the generation of proofs from model checking
results include [22,23], [17] and [10], but they are mainly theoretical, and no
implementation is available, to the best of our knowledge. In contrast, our cer-
tification procedure has been implemented within a theorem prover framework,
and specifically targets the *rlive* algorithm.

3 Background and Preliminaries

We operate within the framework of Boolean (propositional) logic, using the
standard concepts of satisfiability, validity, interpretations, and models. We use
lowercase Latin letters *x*, *v* (possibly with subscripts or primes) to denote propo-
sitional variables. Similarly, uppercase Latin letters *X*, *V* represent sets of vari-
ables. Uppercase Latin letters *I*, *T*, as well as lowercase Latin and Greek letters
$q, \phi, \psi$, are used to denote formulae, while uppercase Greek letters $\Gamma$ and $\Delta$ and $\Pi$ represent sets of formulae.

## 3.1 Transitions Systems

We take into account systems modeled by state transition structures, implicitly represented by propositional formulae. A transition system $\mathcal{M}$ is a triple $(X, \mathcal{I}, T)$, where $X$ is a set of (propositional) state variables, $\mathcal{I}(X)$ is a formula representing the initial states, and $T(X, X')$ is a formula representing the system's transition relation. The states of $\mathcal{M}$ are (complete) assignments to the variables in $X$. We denote by $\Sigma_X$ the set of states. A state $s \in \Sigma_X$ is a model for a propositional formula $\psi$, denote by $s \models \psi(X)$, if substituting the values of $s$ into $\psi$, the formula $\psi$ evaluate to True. Next states, i.e., those reached after a transition, are represented as assignments to primed state variables $X'$. A path of $\mathcal{M}$ is an infinite sequence of states $s_0, s_1, \dots$ such that $s_0 \models \mathcal{I}$, and for all $i \ge 0$, $s_i, s'_{i+1} \models T$. Given a path $\pi := s_0, s_1, \dots$ we denote with $\pi[i]$ the state $s_i$.

## 3.2 Linear Temporal Logic

Linear Temporal Logic (LTL) was introduced by Pnueli [24] for the specification and verification of reactive systems. Formulae of LTL are constructed from a set of propositional variables $X$ using the usual logical connectives ($\neg$, $\wedge$, $\vee$) and some temporal operators $X$ ("next"), $F$ ("eventually"), $G$ ("always") and $U$ ("until"). LTL formulae are interpreted in terms of paths, i.e., sequences of states of a transition system. Their semantics is also extended to states and whole transition systems.

Given a transition system $\mathcal{M} = (X, \mathcal{I}, T)$, a path $\pi := s_0, s_1, \dots$ in $\mathcal{M}$, an index $i$ and a formula $\psi$ over $X$, we define $\pi, i \models \psi$, i.e. that $\pi$ satisfies $\psi$ in $i$, as follows:

- $\pi, i \models \top$ and $\pi, i \not\models \bot$.

- For each $p \in X$, $\pi, i \models p$ iff $\pi[i] \models p$.

- $\pi, i \models \neg \psi$ iff $\pi, i \not\models \psi$.

- $\pi, i \models \psi_1 \wedge \psi_2$ iff $\pi, i \models \psi_1$ and $\pi, i \models \psi_2$.

- $\pi, i \models \psi_1 \vee \psi_2$ iff $\pi, i \models \psi_1$ or $\pi \models \psi_2$.

- $\pi, i \models \mathbf{X}\psi$ iff $\pi, i+1 \models \psi$.

- $\pi, i \models \mathbf{F}\psi$ iff $\pi, j \models \psi$ for some $j \ge i$.

- $\pi, i \models \mathbf{G}\psi$ iff $\pi, j \models \psi$ for every $j \ge i$.

- $\pi, i \models \psi_1 \mathbf{U}\psi_2$ iff $\pi, j \models \psi_2$ for some $j \ge i$ and $\pi, k \models \psi_1$ for every $i \le k < j$.

Finally, $\pi \models \psi$ iff $\pi, 0 \models \psi$. Given a propositional formula $q$ over $X$, we call the *liveness checking problem*, denoted by $\mathcal{M} \models \mathbf{FG}q$, the problem to check $\pi \models \mathbf{FG}q$ for all paths $\pi$ of $\mathcal{M}$. $\mathbf{FG}q$ intuitively means that, in any path of $\mathcal{M}$, $q$ eventually holds in all the future states. Therefore the condition $\neg q$ can only be visited a finite number of times. Dually, a counterexample of $\mathbf{FG}q$ is an infinite path where $\neg q$ is visited an infinite number of times, i.e. there is
a trace satisfying $GF\neg q$. Since we are working in the finite-state case, such a counterexample must be a lasso-shaped path, i.e. an infinite sequence of states consisting of a finite prefix leading to a cycle that repeats forever. The general model checking problem, denoted by $M \models \phi$ where $\phi$ is an LTL formula, can be reduced to the liveness checking problem $M \times A_{\neg\phi} \models FGq$ following the standard automata-theoretic approach [29], where $\neg q$ is the Buchi acceptance condition of $A_{\neg\phi}$.

## 3.3 Liveness Checking with rlive

rlive is a recent algorithm for verifying liveness properties in finite-state symbolic transition systems [30]. It can be seen as a variant of k-liveness [9] that explores the state-space in a depth-first search manner. Like other approaches, rlive reduces the liveness checking to a sequence of safety checks. Algorithm 1 describes how rlive is implemented using a generic invariant-checking engine. The key innovation is that rlive builds counterexamples to FGq incrementally through a recursive, depth-first search process, rather than directly searching for lasso-shaped counterexamples. When looking for counterexamples, rlive first finds a path from the initial states to a $\neg q$-state, i.e. a state that satisfies $\neg q$. This happens in the first iteration of the while-loop at line 4, Algorithm 1, where $\neg C$ and $\neg C'^1$ both evaluate to $\top$. The state s, line 5, is the first $\neg q$-state met. Notice that if such a state is not reachable, then $Gq$ is proved and so is $FGq$. Then it searches for additional $\neg q$-states from the successors of each discovered $\neg q$-state (line 9). During this process, either of the following outcomes occurs:

1. a previously visited $\neg q$-state is met again, creating a lasso-shaped counterexample that violates the liveness property (lines 11-12), or

2. the search reaches a point where no more $\neg q$-states can be reached. In this case, rlive obtains an inductive invariant, the *shoal*, from the safety checker, which describes the set of states from which $\neg q$ can be visited a finite number of times only (lines 15-16). Clearly, no state in the shoal belongs to a counterexample trace.

Hence, the shoals are used to restrict future searches by blocking parts of the system state space. The algorithms excludes the states in $C$ from the transition system by adding the constraint $\neg C \wedge \neg C'$ to $T$ (lines 4 and 9). Additionally, the states to be searched are no longer simply $\neg q$-states, but states in $T^{-1}(\neg C) \cap \neg q$ (lines 4 and 9), i.e. $\neg q$-states that also have successors outside the shoal $C$, to exclude $\neg q$-states that are proved not to be part of the counterexample. This procedure continues until either all the reachable $\neg q$-states are eliminated, proving the property (line 18), or a lasso-shaped counterexample is found (lines 11-12).

<footnote n="1">¹ We remark that for a formula $A$, the primed notation $A'$ represents the set of states that are immediate successors to states satisfying $A$. This is semantically equivalent to the LTL next operator $X$ introduced in Sect. 3.2.</footnote>
<table><caption>**Algorithm 1:** rlive algorithm [30].</caption><thead><tr><th></th><th></th></tr></thead><tbody><tr><td>1</td><td>Procedure rlive(X, I, T, FGq) begin</td></tr><tr><td>2</td><td>C := ⊥</td></tr><tr><td>3</td><td>B := empty stack of states</td></tr><tr><td>4</td><td>while check-invariant(X, I, T ∧ (¬C ∧ ¬C'), T<sup>-1</sup>(¬C) → q) is Unsafe do</td></tr><tr><td>5</td><td>s := final state of get-counterexample()</td></tr><tr><td>6</td><td>B.push(s)</td></tr><tr><td>7</td><td>while B is not empty do</td></tr><tr><td>8</td><td>s := B.top()</td></tr><tr><td>9</td><td>if check-invariant(X, T(s), T ∧ (¬C ∧ ¬C'), T<sup>-1</sup>(¬C) → q) is Unsafe then</td></tr><tr><td>10</td><td>t := final state of get-counterexample()</td></tr><tr><td>11</td><td>if t ∈ B then</td></tr><tr><td>12</td><td>return Unsafe</td></tr><tr><td>13</td><td>B.push(t)</td></tr><tr><td>14</td><td>else</td></tr><tr><td>15</td><td>inv := get-inductive-invariant()</td></tr><tr><td>16</td><td>C := C ∨ inv</td></tr><tr><td>17</td><td>B.pop()</td></tr><tr><td>18</td><td>return Safe</td></tr></tbody></table>

## 3.4 Theorem Proving in PVS

The Prototype Verification System (PVS) [20] is a specification language integrated with a theorem prover. The PVS theorem prover is interactive, but it also supports strategies development [21] and a batch mode [18], so that proofs can be run automatically. PVS uses a sequent-style [14] proof representation. A PVS sequent is an object of the form $A_1, A_2, A_3, ... \vdash B_1, B_2, B_3, ...$, where formulae $A_i$ make the antecedent and formulae $B_j$ make the consequent. The sequent above asserts that “if all the A's are true, then at least one of the B's is true”. Hence, the sequent means the same as: $(A_1 \land A_2 \land A_3 \dots) \rightarrow (B_1 \lor B_2 \lor B_3 \dots)$.

The prover builds a proof tree that starts with $\vdash A$, where A is the theorem to be established. A proof is accomplished when all the leaves are recognised as true: this occurs if any antecedent is the same as any consequent ($C, \Gamma \vdash C, \Delta$), if any antecedent is false (*False*, $\Gamma \vdash \Delta$), or if any consequent is true (*True*, $\Delta$). Other sequents can be recognised as true using more powerful inferences [26].

## 3.5 A Shallow Embedding of LTL into PVS

In [28] we present a formalisation of LTL into PVS, following a shallow embedding approach [5, 25].

In the PVS theory `shallow_ltl` we declare the type `trace` as all mappings from natural numbers to states. An *LTL formula* is a function that takes a trace and a natural number, and returns a boolean PVS type (*True* or *False*), which is the truth-value of the formula at point on the trace. A *state* is an object of any type, and it is an explicit parameter of `shallow_ltl`.
```
shallow_ltl(State: TYPE+): THEORY
BEGIN
Trace: TYPE = ARRAY[nat -> State]
ltlformula: TYPE = [Trace -> [nat -> bool]]
```

Examples of definition of propositional and LTL operators within our theory<fnref n="2" /> follow, where *P* is an LTL formula.

```
NOT(P)(trace: Trace)(t: nat): bool = NOT P(trace)(t);
NEXT(P)(trace: Trace)(t: nat): bool = P(trace)(t+1);
GLOBALLY(P)(trace: Trace)(t: nat): bool = FORALL (t0: nat): t0 >= t IMPLIES
P(trace)(t0);
```

An LTL formula *P* is valid if it is true at the initial state of any trace. A stronger notion of validity, called *global validity*, is when the formula is true at any state of any trace.

```
|=(trace:Trace, t:nat, P): bool = P(trace)(t)
valid(P): bool = FORALL (trace: Trace): |=(trace, 0, P)
valid_all(P): bool = FORALL (trace: Trace): FORALL (t: nat): |=(trace, t, P)
```

The full theory `shallow_ltl` can be found in a dedicated repository [27].

# 4 Certifying Liveness Properties Using rlive

Consider the liveness checking problem $\mathcal{M} \models \mathbf{FG}q$, where $\mathcal{M} = (X, \mathcal{I}, T)$ and $q$ is a propositional formula over $X$. With an abuse of notation, we consider $T$ also an LTL formula, identifying $x'$ with $\mathbf{X}(x)$ for every variable $x \in X$. In order to prove $\mathcal{M} \models \mathbf{FG}q$, we provide a proof of $(\mathcal{I} \wedge \mathbf{GT}) \rightarrow \mathbf{FG}q$, following the same approach as in [15].

## 4.1 A New Temporal Deductive Rule for Liveness

In order to prove $(\mathcal{I} \wedge \mathbf{GT}) \rightarrow \mathbf{FG}q$, we use the following inference rule denoted with RL

$$ \frac{P_1 \quad P_0 \quad Pk_1 \quad Pp_1 \quad \dots \quad Pk_n \quad Pp_n}{\mathcal{I} \wedge \mathbf{G}(T) \rightarrow \mathbf{FG}q} \quad \text{RL} $$

The premises of the rule RL are:

$$ P_1 := (\mathcal{I} \wedge \mathbf{GT} \wedge \mathbf{G} \neg C) \rightarrow \mathbf{G}q $$

$$ P_0 := \mathbf{G}(C_0 \leftrightarrow \bot) $$

$$ Pk_1 := \mathbf{G}((C_0 \lor C_1) \land T \rightarrow \mathbf{X}(C_0 \lor C_1)) $$

$$ Pp_1 := \mathbf{G}((C_0 \lor C_1) \land T \land \neg q \rightarrow \mathbf{X}(C_0)) $$

...

$$ Pk_n := \mathbf{G}((C_0 \lor \dots \lor C_n) \land T \rightarrow \mathbf{X}(C_0 \lor \dots \lor C_n)) $$

<footnote n="2">² PVS allows overloading of built-in symbols. In the definition above the first `NOT` is our defined LTL operator, which creates an LTL formula and whose semantics is defined via the boolean PVS operator `NOT`.</footnote>
$$Pp_n := \mathbf{G}((C_0 \lor \dots \lor C_n) \land T \land \neg q \rightarrow \mathbf{X}(C_0 \lor \dots \lor C_{n-1}))$$

where $C := C_0 \lor C_1 \lor \dots \lor C_n$.

Intuitively, $P_i$ means that any trace of $\mathcal{M}$ satisfies that either a state in the shoal will be met eventually, or $q$ is an invariant - being the formula $(\mathcal{I} \land \mathbf{GT} \land \mathbf{G} \neg C) \rightarrow \mathbf{G}q$ equivalent to $(\mathcal{I} \land \mathbf{GT}) \rightarrow (\mathbf{FC} \lor \mathbf{G}q)$. If the latter is the case, then $\mathbf{FG}q$ holds and the liveness property is therefore verified. Thus we need to cover the case where a shoal state is met eventually ($\mathbf{FC}$).

We consider the additional premises of RL, $P_0$, $Pk_1$, $Pp_1$, ..., $Pk_n$, $Pp_n$. $P_0$ simply states that the shoal is initially empty. Each premise $Pk_i$ ($1 \le i \le n$) states that the invariant $C_0 \lor \dots \lor C_i$ incrementally built is inductive. Each premise $Pp_i$ ($1 \le i \le n$) states that if we are in a state where $C_0 \lor \dots \lor C_i$ and $\neg q$ both hold, following the transition $T$, the next state will belong to at least one shoal that was added to $C$ before $C_i$ itself, i.e. to $C_0 \lor \dots \lor C_{i-1}$. This means that once in the shoal, we do not exit it, and that the search space can be incrementally restricted, as long as we keep visiting a $\neg q$-state. Notice that $Pk_1$ is equivalent to $\mathbf{G}(C_1 \land T \land \neg q \rightarrow \bot)$: states in $C_1$ cannot reach $\neg q$-states at all. $C_1$ represents the first non-empty set of states added to $C$ by the algorithm.

A formal proof of the fact that rlive contains the information necessary to prove premises $P_i$, and $Pk_i$, $Pp_i$ for $1 \le i \le n$ is given in Sect. 4.3.

**RL as a Generalisation of k-liveness Rule.** In the temporal proof for k-liveness from [15] we have formulae $\alpha_0, \dots, \alpha_{k+1}$, that keep count of the number of times the fairness condition $\neg q$ is reached. Assuming by contradiction that we will keep reaching $\neg q$, eventually $\alpha_{k+1}$ is reached. This final formula expresses a contradiction as $\neg q$ can be visited at most $k$ times by the k-liveness algorithm [9]. Thus, any path starting from $\mathcal{I}$ can visit $\neg q$ finitely many times only (concluding $\mathbf{FG}q$).

RL generalises this k-liveness rule, in the sense that it can be used to build proofs for k-liveness, but the premises are more relaxed to cover more general proofs. In particular, given the $\alpha$'s conditions from k-liveness, RL can be used to perform a k-liveness proof as in [15].

Given $n = k+1$, we can establish this mapping: each k-liveness condition $\alpha_i$ for $0 \le i \le k+1$ maps to $C_{k-i+1}$, so specifically $\alpha_{k+1}$ maps to $C_0$, both formulae expressing a contradiction, $\alpha_k$ maps to $C_1$ and so on through the sequence up $\alpha_1$ mapping to $C_k$ and $\alpha_0$ mapping to $C_{k+1}$. $C = C_0 \lor \dots \lor C_n = \alpha_{k+1} \lor \dots \lor \alpha_0$. Given this mapping, we can prove that if the premise $P_i$ of k-liveness holds, which states that $\mathcal{I} \rightarrow \mathbf{F}(\alpha_0)$, than the corresponding $P_i$ of RL holds too, as $\alpha_0$ implies $C$ using the mapping above. Moreover it is possible to prove by induction that, given this mapping, if each $Pk_i$ and $Pp_i$ premises from k-liveness hold, then so do the corresponding premises for RL.

Thus, RL can be used in alternative to the rule defined in [15] for k-liveness, but the premises are more relaxed to accommodate the proof of rlive. In particular, it provides a more general first premise $P_i$, and weaker premises $Pk_i$ than the corresponding premises of k-liveness. In the k-liveness rule, $P_i := \mathcal{I} \rightarrow \mathbf{F}(\alpha_0)$, i.e., from the initial state we can reach $\alpha_0$ and start counting. In RL we need
to consider the alternative possibility that the shoal stays empty (FC is false), thus concluding Gq. The Pki premises from RL allows to transition from a Ci to any shoal with a lower index, whilst in the k-liveness rule a state from αi is required to either remain in αi (when q holds) or transition to the immediate successor condition αi+1.

## 4.2 Correctness of the Rule

Let us denote the set of formulae {$P_{k_1}, P_{k_2}, \dots, P_{k_n}, P_{n+1}$} simply with Π. The full formalisation and proof of correctness of RL has been done in PVS in our theory lemmas_shallow_ltl [27], in the form of a validity statement: for all formulae I, T, q and C we proved that valid((P<sub>1</sub> ∧ P<sub>0</sub> ∧ Π) → (I ∧ GT → FGq)). The schema of the proof is as follows, and we refer to [27] for the fine-grained proof.

$$ \frac{\frac{P_i}{(I \wedge GT) \rightarrow (\neg G \neg C \vee Gq)} \qquad [I \wedge GT]}{(I \wedge GT) \rightarrow (FC \vee Gq) \qquad FC \vee Gq} $$

If Gq is the case:

$$ \frac{\frac{Gq}{FGq}}{(I \wedge GT) \rightarrow FGq} $$

Let us now consider the second possibility: FC.

$$ \text{RLB} \quad \frac{\substack{\mathbf{FC} \\ \Pi} \quad [\mathcal{I} \wedge \mathbf{GT}] \quad [\mathbf{GF} \neg q]}{\mathbf{FC}_0} \quad \frac{P_0}{\mathbf{G} \neg C_0} \quad \frac{\substack{\perp \\ \neg \mathbf{GF} \neg q}}{\mathbf{FG} q} \quad [(\mathcal{I} \wedge \mathbf{GT}) \rightarrow \mathbf{FG} q] $$

Notice that the main step to prove the correctness of RL is the following deduction rule

$$ \text{RLB} \quad \frac{\mathbf{FC} \quad \Pi \quad \mathcal{I} \wedge \mathbf{GT} \quad \mathbf{GF} \neg q}{\mathbf{FC}_0} $$

This rule states that if we are on a trace where the shoal C is eventually entered, and where ¬q holds infinitely often then, considering the additional premises Π of RL, we are bound to enter the last shoal C₀. As shown in the proof sketch above, the assumption of the fact that ¬q holds infinitely often is used to perform a proof by contradiction, and it is negated when the contradiction is reached. Also RLB has been formalised and proved in PVS within our theory lemmas_shallow_ltl [27]. The proof RLB uses the KLB rule from [15], which is the main step for the deduction of their temporal rule for k-liveness. This is because, as explained earlier, RL is a generalisation of this rule.
## 4.3 Completeness for rlive

In this section, we show that the rule is complete to provide a proof for the property proved by rlive, in the sense that rlive can be easily extended to generate the premises of the rule.

The $C_i$ are the inductive invariants that are generated by performing a series of invariant checks on variations of the original transition system. Thus, initially $C := C_0$ is empty ($C_0 = \perp$, from line 2 of Algorithm 1). New shoals are added in disjunction and at the $i$-th iteration $C = C_{\le i} := C_0 \lor \dots \lor C_i$ (lines 15-16). At each iteration (lines 8-17), rlive proves that the new $C_{i+1}$ shoal is an inductive invariant for the modified transition $T \land \neg C_{\le i} \land \neg C'_{\le i}$ and that it implies the invariant $T \land \neg C'_{\le i} \to q$ (line 9). We can prove that this is sufficient to prove the premises $P_{k_n}$ and $P_{p_n}$ from Sect. 4.2.

**Theorem 1.** Assume that for all $i$, $0 \le i < n$, the following holds:

$$ \models (C_{i+1} \land T \land \neg C_{\le i} \land \neg C'_{\le i}) \rightarrow C'_{i+1} \quad (1) $$

$$ C_{i+1} \land \neg q \land T \land \neg C'_{\le i} \models \perp \quad (2) $$

Then for all $i$, $0 \le i < n$, the following implications are valid:

$$ ((C_{\le i} \lor C_{i+1}) \land T) \rightarrow (C'_{\le i} \lor C'_{i+1}) \quad (3) $$

$$ ((C_{\le i} \lor C_{i+1}) \land T \land \neg q) \rightarrow C'_{\le i} \quad (4) $$

*Proof.* We prove (3) by induction on $i$. Since $C_{\le i} = \perp$ in case $i=0$, the base case of (3), what we want to prove says that $(C_1 \land T) \to (C'_1)$, which is exactly the assumption (1) with $i=0$.

Let us consider the step case of the induction. By inductive hypothesis we know that $(C_{\le i} \land T) \to (C'_{\le i})$. By (1), we have that $\neg C_{\le i} \land C_{i+1} \land T \to C'_{\le i+1}$. From these two, we can deduce that the same holds for $((C_{\le i} \lor C_{i+1}) \land T) \to (C'_{\le i} \lor C'_{i+1})$, that is 3.

We now prove (4). From (3), we have that $((C_{\le i}) \land T) \to (C'_{\le i})$. From (2), we deduce that $(C_{i+1} \land T \land \neg q) \to C'_{\le i}$. From these two, we can deduce that $((C_{\le i} \lor C_{i+1}) \land T \land \neg q) \to C'_{\le i}$, that is (4). $\square$

Similarly, we can prove that the information provided by the algorithm rlive is sufficient to prove the initial premise $P_i$. The idea is that $C$ represents the final shoals returned by the rlive algorithm and the algorithm proves that $P_i$ holds. The last invariant check at line 4 of Algorithm 1 returns an invariant, let us call it $\psi$, that is inductive for the modified transition $T \land \neg C \land \neg C'$, and such is that it implies the invariant $T \land \neg C' \to q$.

**Theorem 2.** Assume that the following holds:

$$ \models \psi \rightarrow (T \land \neg C' \rightarrow q) \quad (5) $$

$$ \models \mathcal{I} \land \mathbf{G}(T \land \neg C) \rightarrow \mathbf{G}\psi \quad (6) $$

Then the following implication is valid:

$$ \mathcal{I} \land \mathbf{G}(T \land \neg C) \rightarrow \mathbf{G}q \quad (7) $$
## 4.5 A Proof Strategy for Liveness Checking

Given a model $\mathcal{M} = \langle X, \mathcal{I}, T \rangle$, a liveness property $q$ and a formula $C$ representing the shoal, which is provided by the model checking stage, a proof strategy for certifying liveness results utilises the temporal deductive rule RL (as presented above) as a proven lemma, and then proceeds to discharge each of its premises $P_1, P_0$ and $\Pi$.

The strategy takes the sequence of formulae $C_0, \dots, C_n$, whose disjunction makes the shoal, as explicit parameters. The model checker provides an additional parameter formula, let us call it $\psi$. As we will see later, this is the inductive invariant that will be used to accomplish the proof of the premise $P_1$.

The proof tree starts with the goal: $\vdash valid(\mathcal{I} \wedge GT \rightarrow FGq)$. The strategy splits in two branches: **Branch 1**, where the premise $P_1$ is added to the set of assumptions, and **Branch 2** where $P_1$ is added to the set of conclusions, to be proved. In practice we make use of the PVS rule **Case** which allows us to assume a formula and subsequently prove this formula to be true [26].

**Branch 1** in turns splits into two branches: **Branch 1.1** where the remaining premises $P_0$ and $\Pi$'s are added to the set of assumptions, and **Branch 1.2** where $P_0$ and $\Pi$'s are added to the set of conclusions, to be proved.

On **Branch 1.1 RL** is added to the set of assumptions as a proven lemma, with appropriate substitution for the formulae representing the shoal $C, \mathcal{I}, T$ and the liveness property $q$ within the RL premises $P_1, P_0$ and $\Pi$. The sequent at the leaf of **Branch 1.1** has this form:

$$ \begin{array}{rl} -1 & valid(P_1 \wedge P_0 \wedge \Pi \rightarrow (\mathcal{I} \wedge GT \rightarrow FGq)) \\ -2 & valid(P_1) \\ -3 & valid(P_0 \wedge \Pi) \\ 1 & valid(\mathcal{I} \wedge GT \rightarrow FGq) \end{array} $$

which is clearly provable after expanding the definition of “valid” and some simple symbolic manipulation. This concludes the proof of **Branch 1.1**.

The strategy turns then to **Branch 1.2**, where the premises $P_0, Pk_1, Pp_1, \dots, Pk_n, Pp_n$ have to be discharged. After expanding the definition of the **Globally** operator **G**, which is the main operator of each of these premises, they can all be discharged by rewriting $\mathcal{I}, T, q$ and each $C_i$ for $0 \le i \le n$ with the appropriate formulae from the theory at issue, and by using the PVS SAT solver Yices to prove the propositional implications at the resulting leaves. This completes the proof of **Branch 1.2**.

The strategy turns to **Branch 2**, where premise $P_1$ has to be discharged. We remind the reader that $P_1 := \mathcal{I} \wedge GT \wedge G \neg C \rightarrow Gq$. This is an invariant claim equivalent to $\mathcal{I} \wedge G(T \wedge \neg C) \rightarrow Gq$. $P_1$ expresses that the formula $q$ is an invariant for the model $\mathcal{M} = \langle X, \mathcal{I}, \hat{T} \rangle$ with $\hat{T} := T \wedge \neg C \wedge \neg C'$. Since formula $q$ is not necessarily inductive w.r.t. $\mathcal{M}$, we need an invariant formula $\psi$, that is inductive and that will imply the proof of the invariant claim in $P_1$. The
model checker is able to produce such an inductive invariant as the result of the invariant check contained within the *rlive* algorithm, as described in Sect. 4.3. (line 4 of Algorithm 1). It then passes this as a parameter for the proof strategy, together with the shoal formula *C*. In order to prove $P_1$, the proof strategy applies a subroutine for proving invariants using inductive invariants. This subroutine strategy takes the formula $\psi$ as parameter and carries out a proof of $P_1$. This strategy is an adaptation of the strategy for proving invariant presented in [28]. This completes the proof of **Branch 2**.

Our PVS implementation of this strategy can be found at [27], together with a full example of a proof using this strategy.

# 5 Experimental Evaluation

In this section, we present the experimental evaluation of our proposed methodology, assessing the effectiveness, efficiency, and robustness of our approach through a series of comprehensive tests run on publicly available benchmarks sets. We describe the experimental setup, including the hardware and software configurations, the datasets used, and the specific metrics considered for the evaluation. We also provide a detailed analysis of the results obtained.

**Setup.** We have implemented our proof generation and certification procedure on top the model checking tool nuXmv [7]. The tool takes as input a model in Aiger [2] format, and produces the inductive invariants making the shoal and the inductive invariant $\psi$ described in Sect. 4.5, as Aiger combinational circuits expressed over the state variables of the model.

We then apply a simple Python script to translate the input model and the generated invariants into a PVS theory. We make the script available (together with the rest of the our toolchain) at [27]. The Python script is relatively simple, and it can be verified through standard software verification methodologies. This was adapted from our work from [28] to include generation of theories for liveness checking. The overhead of this translation stage (namely, stage 2 of the certification process described in Sect. 4.4) is negligible, and therefore not included in the results evaluation where we only compare the model checking stage and the proof generation stage.

**Benchmark Set.** For our evaluation, we have collected a total of 53 distinct problem instances from different families, stemming from previous Hardware Model Checking Competitions (HWMCC) [3]. These 53 instances are the safe instances that could be successfully proved by nuXmv in the time limit of 1200 s. All benchmarks, certificates, and run logs have been made available for reference [27].

**Results.** The nuXmv runs were carried out on a computer cluster, on a queue consisting of 4 nodes with identical hardware specifications. Each node is
equipped with an Intel Xeon CPU 6226R processor operating at 2.9 GHz, with 32 CPU cores and 16 GB of memory. These jobs were managed by SLURM with a memory limit of 4 GB and a wall-time limit of 1200 seconds per experimental run.

PVS experiments were conducted using PVS8.0³ on the set of benchmarks described above, on the same cluster and in the same setup mentioned above, with a memory limit of 8 GB and a wall-time limit of 3600 s per run.

The results demonstrate the effectiveness of the prototype implementation, integrating our rlive proof strategy described in Sect. 4.5 within the existing certifying model checking framework based on PVS [28]: of the 53 total test cases, 41 in total were successfully proved by PVS within the allotted time and memory constraints, whilst remaining 12 cases exceeded the available memory resources.

<figure><img src="image_80.png" /><figcaption>**Fig. 1.** Comparison between model checking verification and PVS certification times, considering overall certification times (a) and just SAT solver times (b).</figcaption></figure>

Figure 1 presents preliminary results comparing model checking instances verification times, i.e. the time taken by the model checker to verify that an instance model satisfies a liveness property using the rlive algorithm (this is stage 1 of the certification process described in Sect. 4.4), against the certification times of PVS, i.e. the time taken by PVS to prove the corresponding theorem (this is stage 3 of the certification process described in Sect. 4.4). Figure 1a accounts for all the PVS certification contributions whereas Fig. 1b focuses on just Yices SAT solver times. Figure 1a shows that almost all data points lie significantly above the diagonal dashed line indicating that PVS total proof time is consistently

<footnote n="3">³ We modified the PVS Makefile configuration to increase resource allocations. The SBCL_SPACE_SIZE parameter was increased from 6 GB to 30 GB, and SBCL_STACK_SIZE was increased from 8 MB to 32 MB.</footnote>
higher than the model checking verification time for the same problems. Figure 1b shows that Yices times are generally closer to the diagonal line, suggesting that the proof-obligation discharging part of the proof is more efficient than the rest of the steps performed in the PVS proofs.

<figure><img src="image_81.png" /><figcaption>Fig. 2. Times breakdown for PVS-based runs.</figcaption></figure>

To better understand the reasons behind this gap, we further analysed the breakdown of execution times for different operations within PVS. Figure 2 illustrates the total certification time divided into three components: *type-checking time*, the time spent verifying semantic constraints, determining expression types, and resolving names, *proof-checking time*, the time spent executing the actual steps of the proof strategy and *SAT-solving time*, the time of the proof-checking time spent on calls to the SAT solver Yices. Our analysis reveals that PVS performance bottlenecks occur primarily within proof steps other than the Yices solver component. When processing theories with numerous shoals formulae, PVS spends disproportionate time on fundamental logical operations, such as logical operators’ expansion. For *n* shoals, expanding basic LTL operators like ‘AND’ requires approximately *n* separate expansion operations, each triggering cascading expansions of nested ‘OR’ operations. These operations, as well as operations of installing and rewriting definitions, involve substantial hidden costs. PVS performs additional typechecking and book-keeping during these operations. This explains the significant gap between Yices processing time and proof time observed in our performance analysis.

While our analysis indicate scaling limitations in the current prototype implementation, it is important to emphasise that the primary contribution of this work is the theoretical foundation and correctness of our proof strategy for *rlive*. The prototype serves its intended purpose: demonstrating that the strategy is sound and functional by successfully certifying the tested benchmarks. The PVS based framework could be implemented using alternative certification tools or
optimised versions of PVS tailored to this problem domain. As proposed in [28],
future work will address these scaling concerns.

6 Conclusions and Future Work

In this paper we have considered rlive [30], a new SAT-based model-checking
algorithm for the verification of liveness properties of finite-state symbolic tran-
sition systems. We have shown that, despite the complexity of the algorithm, the
shoals provided by the model checker are sufficient to generate proof certificates
in a deductive system for temporal properties, and that even though rlive and
k-liveness seem two very different algorithms, in terms of temporal rules the first
can be seen a generalisation of the second, as it is presented in [15]. We have
formalised the rule for rlive, proved its correctness and completeness, and devel-
oped a proof strategy that uses this rule to certify liveness checking results. We
have implemented our strategy as a prototype in an existing certifying model
checking framework [28] based on PVS, and tested the implementation on a set
of benchmarks from the hardware model checking competition.

We see several directions for future work, such as extending the certifying
model checking approach to other liveness checking algorithms such as liveness-
to-safety [1] and FAIR [6]. It would also be interesting to investigate the possibil-
ity of a proof strategy that encompasses all these liveness checking algorithms.
We would also like to generalise the current proof strategy for rlive to account
for multiple fairness constraints, as it is done for k-liveness in [15], since our app-
roach is currently limited to a single fairness condition (namely ¬q). Since proofs
are easily composed, it is a very feasible next step to consider the generation of
proofs that combine multiple transformation techniques with liveness proofs, as
it is done in [15] for k-liveness. Some of these transformations, such as temporal
decomposition and phase abstraction, are already certifiable using the theorem
prover based approach from [28]. We would also like to consider generalisations
to the infinite-state transition system and SMT (Satisfiability Modulo Theories)
based model checking, since rlive has recently been generalised to handle this
type of transition systems [8].

**Acknowledgments.** The authors acknowledge the support of the PNRR project FAIR - Future AI Research (PE00000013), under the NRRP MUR program funded by the Next Generation EU and in particular the activity of technology transfer "nuXmv - Towards Market Readiness".

References

1. Biere, A., Artho, C., Schuppan, V.: Liveness checking as safety checking. Electron. Notes Theor. Comput. Sci. **66**(2), 160–177 (2002)

2. Biere, A., Heljanko, K., Wieringa, S.: AIGER 1.9 and beyond. Technical Report 11/2, Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr. 69, 4040 Linz, Austria (2011)
3. Biere, A., Jussila, T.: The Model Checking Competition Web Page, http://fmv.jku.at/hwmcc

4. Biere, A., Yu, E., Froleyks, N.: Stratified certification for k-induction. In: Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design–FMCAD 2022, vol. 3, p. 59. TU Wien Academic Press (2022)

5. Boulton, R.J., et al.: Experience with embedding hardware description languages in HOL. In: TPCD, vol. 10, pp. 129–156 (1992)

6. Bradley, A.R., Somenzi, F., Hassan, Z., Zhang, Y.: An incremental approach to model checking progress properties. In: 2011 Formal Methods in Computer-Aided Design (FMCAD), pp. 144–153. IEEE (2011)

7. Cavada, R., et al.: The NUXMV Symbolic Model Checker. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 334–342. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08867-9_22

8. Cimatti, A., Griggio, A., Johannsen, C., Rozier, K.Y., Tonetta, S.: Infinite state liveness checking with rlive. In: Proceedings of the 37th International Conference on Computer Aided Verification (CAV 2025) (2025). To be published

9. Claessen, K., Sörensson, N.: A liveness checking algorithm that counts. In: 2012 Formal Methods in Computer-Aided Design (FMCAD), pp. 52–59. IEEE (2012)

10. Dax, C., Hofmann, M., Lange. M.: A proof system for the linear time μ-calculus. In: FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science: 26th International Conference, Kolkata, India, December 13-15, 2006. Proceedings 26, pp. 273–284. Springer (2006)

11. Dutertre, B., De Moura, L.: The yices smt solver. Tool paper at http://yices.csl.sri.com/tool-paper.pdf, 2(2), 1–2 (2006)

12. Froleyks, N., Yu, E., Biere, A., Heljanko, K.: Certifying phase abstraction. In: International Joint Conference on Automated Reasoning, pp. 284–303. Springer (2024)

13. Gabbay, D., Pnueli, A., Shelah, S., Stavi, J.: On the temporal analysis of fairness. In: Proceedings of the 7th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp. 163–173 (1980)

14. Gentzen, G.: Untersuchungen über das logische schließen. i. Mathematische zeitschrift, 35 (1935)

15. Griggio, A., Roveri, M., Tonetta, S.: Certifying proofs for sat-based model checking. Formal Methods Syst. Des. 57(2), 178–210 (2021)

16. Kuismin, T., Heljanko, K.: Increasing confidence in liveness model checking results with proofs. In: Haifa Verification Conference, pp. 32–43. Springer (2013)

17. Kupferman, O., Vardi, M.Y.: From complementation to certification. Theor. Comput. Sci. 345(1), 83–100 (2005)

18. Munoz, C.A.: Batch proving and proof scripting in PVS. Technical report, National Institute of Aerospace (2007)

19. Namjoshi, K.S.: Certifying model checkers. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 2–13. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-44585-4_2

20. Owre, S., Rushby, J.M., Shankar, N.: PVS: a prototype verification system. In: International Conference on Automated Deduction, pp. 748–752. Springer, 1992

21. Owre, S., Shankar, N.: Writing PVS proof strategies. In: Design and Application of Strategies/Tactics in Higher Order Logics (STRATA 2003), number CP-2003-212448 in NASA Conference Publication, pp. 1–15 (2003)

22. Peled, D., Pnueli, A., Zuck, L.: From falsification to verification. In: International Conference on Foundations of Software Technology and Theoretical Computer Science, pp. 292–304. Springer (2001)
23. Peled, D., Zuck, L.: From model checking to a temporal proof. In: International SPIN workshop on model checking of software, pp. 1–14. Springer (2001)

24. Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium On Foundations of Computer Science (sfcs 1977), pp. 46–57. IEEE (1977)

25. Rushby, J.: PVS embeddings of propositional and quantified modal logic. arXiv preprint arXiv:2205.06391 (2022)

26. Shankar, N., Owre, S., Rushby, J.M., Stringer-Calvert, D.W.J.: PVS prover guide. Comput. Sci. Lab. SRI Int. Menlo Park, CA 1, 11–12 (2001)

27. Sindoni, G., Griggio, A., Tonetta, S.: Certifying-rlive-25. https://gitlab.fbk.eu/gsindoni/Certifying_Rlive_25. Accessed 15 May 2025

28. Sindoni, G., et al.: Giulia Sindoni, et al.: A theorem prover based approach for sat-based model checking certification. In: Automated Deduction-CADE- 35: 30th International Conference on Automated Deduction, Stuttgart, Germany, 2025, Proceedings 30 (2025). To be published

29. Vardi, M.Y.: An automata-theoretic approach to linear temporal logic. In: Logics for concurrency: structure versus automata, pp. 238–266 (2005)

30. Xia, Y., Cimatti, A., Griggio, A., Li, J.: Avoiding the shoals-a new approach to liveness checking. In: International Conference on Computer Aided Verification, pp. 234–254. Springer (2024)

31. Yu, E., Biere, A., Heljanko, K.: Progress in Certifying Hardware Model Checking Results. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12760, pp. 363–386. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-81688-9_17

**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_82.png" /></figure>