# Checking Linear Integer Arithmetic Proofs in Lambdapi

Alessio Coltellacci, Stephan Merz

► To cite this version:

Alessio Coltellacci, Stephan Merz. Checking Linear Integer Arithmetic Proofs in Lambdapi. FroCoS 2025 - 15th International Symposium Frontiers of Combining Systems, Sep 2025, Reykjavik, Iceland. pp.367-385, 10.1007/978-3-032-04167-8 . hal-05328609

HAL Id: hal-05328609

https://inria.hal.science/hal-05328609v1

Submitted on 23 Oct 2025

**HAL** is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

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

Distributed under a Creative Commons Attribution 4.0 International License
Checking Linear Integer Arithmetic Proofs
in Lambdapi

Alessio Coltellacci¹[0009-0005-3580-2075] and Stephan Merz¹[0000-0003-0974-1844]

University of Lorraine, CNRS, Inria, LORIA, Nancy

**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 [24, 2] 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 [14, 11]. 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 \leftrightarrow 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 $\leftrightarrow$ v such that $t = c v_1 \dots v_n$ where c is a constant.

The relation $\leftrightarrow_{\beta\Sigma}$ is generated by $\beta$-reduction and by the rewrite rules of $\Sigma$. The relation $\leftrightarrow_{\beta\Sigma}$ denotes the reflexive and transitive closure of $\leftrightarrow_{\beta\Sigma}$, and the relation $\equiv_{\beta\Sigma}$ (called conversion) the reflexive, symmetric, and transitive closure of $\leftrightarrow_{\beta\Sigma}$. The relation $\leftrightarrow_{\beta\Sigma}$ must be confluent, i.e., whenever $t \leftrightarrow_{\beta\Sigma} v_1$ and $t \leftrightarrow_{\beta\Sigma} v_2$, there exists some w such that $v_1 \leftrightarrow_{\beta\Sigma} w$ and $v_2 \leftrightarrow_{\beta\Sigma} w$, and it must preserve typing, i.e., whenever $\Gamma \vdash t : A$ and $t \leftrightarrow_{\beta\Sigma} v$ then $\Gamma \vdash v : A$ [5].
A Lambdapi typing judgment $Γ \vdash_Σ t : A$ asserts that term $t$ has type $A$ in the context $Γ$ and the signature $Σ$. The typing rules of $λΠ/≡$ are those of $λΠ$ [17, §2], except for the rule (Conv), given below, that identifies types modulo $≡_{βΣ}$ instead of just modulo $β$-reduction.

$$ \frac{Γ, \vdash_Σ B : u \quad Γ \vdash_Σ t : A \quad A ≡_{βΣ} B}{Γ \vdash_Σ 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`: `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 $ΠX : TYPE$, $(X \to Prop) \to Prop$ to the universal quantifier $∀$. 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 $∀ : Πx : Set, (El x \to Prop) \to Prop$. To quantify over propositions, we further define a constant `o`: `Set` and add the rewrite rule `El o ↪→ 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 $⊥$ (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 List. 1.1 with its Alethe proof (found by cvc5) in List. 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_2.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 \qquad (1) $$

where $\bowtie \in \{=, <, >, \leq, \geq\}$, $m \geq 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 List. 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 inequality are passed as arguments e.g. $(\frac{1}{1}, \frac{1}{1})$ in t2. Steps t3 and t4 apply the
<table><caption>**Table 1.** Linear arithmetic rules in Alethe supported in our encoding.</caption><thead><tr><th>Rule</th><th>Description</th></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> &approx; t<sub>2</sub> &or; ~(&gt;t<sub>1</sub> &ge; t<sub>2</sub>) &or; ~(&gt;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> &not;| t<sub>3</sub>) &rarr; t<sub>1</sub> * t<sub>2</sub> &not;| t<sub>1</sub> * t<sub>3</sub> and &not;| &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> &not;| t<sub>3</sub>) &rarr; t<sub>1</sub> * t<sub>2</sub> &not;|<sub>inv</sub> t<sub>1</sub> * t<sub>3</sub></td></tr><tr><td>la rw eq</td><td>(t &asymp; u) &approx; (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; ~(&gt;t &le; s)</td></tr><tr><td>arith-leq-norm</td><td>t &le; s &rarr; ~(&gt;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>~(&gt;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>

**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 List. 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 Tab. 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 $(\frac{1}{1}, \frac{1}{1})$. Cases where coefficients cannot be reduced to integers are rare in practice, however, we reduce them to integers by clearing denominators with their least common denominator. Let $\varphi_1, \dots, \varphi_n$ be linear inequalities or their negations, but different from $s_1 \approx s_2$ and $a_1, \dots, a_n$ rational numbers, then an la_generic step has the general form

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

The constants $a_i$ are of sort Real. To check the unsatisfiability of the conjunction $\neg \varphi_1 \land \dots \land \neg \varphi_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 $s_1 \le s_2$ or $\neg (s_1 > s_2)$, then let $\psi_i = s_1 > 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 \triangleright \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) \triangleright d_2^i - d_1^i$.

3. Now $\psi_i$ has the form $s_1^i \triangleright 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 $\triangleright$ 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 \triangleright |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 \triangleright \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):
1
2
```
RULES
    (step t11 (cl (not (<= f 0)) (<= (+ 1 (* 4 f)) 1))
     :rule la_generic :args (1/1 1/4))
```

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 \geq 1$.

*Remark 2.* 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 `(? \forall \bar{x}, \varphi) \lor (\varphi[\bar{f}])`, 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...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.
<figure><img src="image_3.png" /><figcaption>Fig. 1. Type definitions for binary positive number, integers, comparison and Booleans.</figcaption></figure>

*Example 3 (Sketch of lia_generic elaboration).* Consider a step *S* (List. 1.3) concluding the clause *¬l*₁ *∩* ... *∩* *l*ₙ where all *l*ᵢ are inequalities and proved by lia_generic rule.

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

**Listing 1.3.** Elaborated proof

Carcara will generate an SMT-LIB problem asserting *l*₁, ..., *l*ₙ and invoke the solver cvc5 on it, expecting an Alethe proof of the unsatisfiability of *l*₁ ∧ ... ∧ *l*ₙ 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 List. 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

**Listing 1.4.** Elaboration of lia_generic

In List. 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 (List. 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_4.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(OH)`. 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 `El int` $\leftrightarrow$ $\mathbb{Z}$. Figure 2 introduces operations on these types, including addition (`+`) and comparison (`=`) over $\mathbb{Z}$. The auxiliary operations `add`, `sub`, and `cmp` implement addition, 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 $\mathbb{Z}$. We will refer to the rewriting rules defining these operations as $\rightarrow_{\mathbb{Z}}$ and $\rightarrow_{\mathbb{P}}$ (for operations on $\mathbb{Z}$ and $\mathbb{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 $\mathbb{Z}$ as binary predicates by reducing them to the decidable comparison $\doteq$. They reduce to $\top$, $\bot$ (or negated) by applying rules of $\to_{\mathbb{Z}}$ and $\to_{\mathbb{P}}$. For example, $1 < 2 \leftrightarrow \mathit{istrue}(\mathit{isLt}(1 \doteq 2)) \leftrightarrow \mathit{istrue}(\mathit{isLt}(\mathit{Lt})) \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 \to \mathbf{Prop}$ be a predicate over a data type $Z$ and $f: Z \to \mathbf{bool}$ be a function such that the following theorem holds:

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

If $f z$ reduces to `true`, then the proof term $f\_correct z$ (`refl bool true`) with `refl`: $\Pi A: \mathbf{Set}, \Pi x: \mathbf{El A}, \mathbf{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 $\mathbb{Z}$. The key idea is to provide a normalization function that transforms a $\mathbb{Z}$ expression into a canonical form.

## 5.1 Representation

The procedure is based on an algebraic group structure, denoted as $\mathbb{G}$ defined in Fig. 3, which represents linear polynomials. The base type for its elements is $\mathbb{G}: \mathbf{TYPE}$. The unary operator `cst` injects constants from $\mathbb{Z}$ into $\mathbb{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 $\mathbb{Z}$ term, in particular a variable. The constructor `mul` represents the multiplication of an element of $\mathbb{G}$ by a constant. The constructor `opp` corresponds to unary minus. Lastly, the constructor $\oplus$ represents the addition of two elements of $\mathbb{G}$.

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 $\mathbb{G}$ are systematically canonicalized.
<figure><img src="image_5.png" /><figcaption>Fig. 3. Definition of $\mathbb{G}$ Algebra and its reification ($\Uparrow$) and denotation ($\Downarrow$) functions.</figcaption></figure>

## 5.2 Associative Commutative Normalization

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

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

will be normalized such that any pair of terms $(\mathit{var} c x)$ and $(\mathit{var} d x)$ involving the same variable $x$ are placed next to each other, and all $(\mathit{cst} k)$ will be placed at the left before the first variable $(\mathit{var} c x)$. We will use the rewriting rules shown in Fig. 4 for reducing $\mathbb{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 $\leq$ builtin total order on $\mathbb{G}$-terms is defined as follows: Terms are ordered such that $cst(c_1) \leq CST(c_2) < (\mathit{var} c x)$ for any constants $c_1 \leq c_2$ and any variable term $(\mathit{var} c x)$. For variable terms, $(\mathit{var} c x) \leq (\mathit{var} d y)$ if either $x < y$, or $x = y$ and $c \leq 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.

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

An $\rightarrow^{AC}_{\Sigma}$ step is a standard $\leftrightarrow_{\Sigma}$ step with syntactic matching followed by AC-canonicalization. We now prove that the relation $\rightarrow^{AC}_{\Sigma}$ terminates and is confluent.
$$ (\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>

**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_Z$ and $\rightarrow_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 $\uparrow$, 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 $\downarrow$. To validate this procedure, it is necessary to establish the correctness of the following diagram, formally expressed by Thm. 8.

<figure><img src="image_6.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 $\to^{AC}_{\Sigma}$.

*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 Lem. 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$

```
opaque symbol t2: Prf* ((\neg (3 < x) \vee^c \neg (x = 2)) \vee \Box) {
    apply \vee^c_{i1};
    rewrite Zinv_lt_eq;
    rewrite Z_diff_gt_Z0_eq (~3) (~x);
    rewrite Z_diff_eq_Z0_eq (x) 2;
    rewrite Zgt_le_succ_r_eq ((~3) - (~x)) 0;
    rewrite Zmult_ge_compat_eq 1 ((~3) - (~x)) ((0 + 1));
    rewrite Zmult_eq_compat_eq (~1) (x - 2) 0;
    rewrite imp_eq_or; apply \Rightarrow^c_i; assume H0; apply \Rightarrow^c_i; assume H1;
    set H01 := (1 * ((~3) - (~x))); set H0r := (1 * (0 + 1));
    set H11 := ((~1) * (x - 2)); set H1r := ((~1) * 0);
    have H1': Prf^c (H11' \ge H1r') { refine Z_eq_implies_ge H1 }; remove H1;
    have contra : Prf^c ((\downarrow (\uparrow (H01' + H11'))) \ge (\downarrow (\uparrow (H0r' + H1r')))) {
        rewrite \downarrow_{\uparrow}; rewrite \downarrow_{\downarrow};
        apply (Zsumgeq_s H01' H0r' H11' H1r' H0 H1');
    };
    apply (\Rightarrow^c_e' contra); apply \top^c_i;
};
```

<caption>**Listing 1.5.** Lambdapi proof of List. 1.2</caption>

We present in List. 1.5 the translation of Step t2 from List. 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_succ_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.
<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>

# 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 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 seconds for cvc5 to find a proof and 30 seconds for the translation step with Carcara. No timeout was imposed during the elaboration step, as the runtime is negligible. A timeout of 20 seconds 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

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

<footnote n="3">³ All benchmarks were executed in parallel using GNU parallel [25] with an Apple silicon M2.</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>

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.

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

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 knowledge, 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 normalization 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: Tools and Algorithms for

<footnote n="4">⁴ https://github.com/NotBad4U/carcara/tree/lambdapi-translate</footnote>
the Construction and Analysis of Systems: 29th International Conference, TACAS 2023. p. 367–386. Springer-Verlag, Cham (2023)

2. Barbosa, H., Fleury, M., Fontaine, P., Schurr, H.J.: The Alethe Proof Format An Evolving Specification and Reference (Mar 2024), https://verit.gitlabpages.uliege.be/alethe/specification.pdf

3. Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB Standard: Version 2.7. Tech. rep., 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.) Intl. Workshop Types for Proofs and Programs (TYPES 2006). pp. 48–62. LNCS, Springer, Berlin, Heidelberg (2006)

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, Germany (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.) Programming Languages and Systems. pp. 95–109. Springer Berlin Heidelberg, Berlin, Heidelberg (2007)

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.) Theoretical Aspects of Computer Software. pp. 515–529. Springer Berlin Heidelberg, Berlin, Heidelberg (1997)

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: Proc. 22nd Intl. Wsh. Satisfiability Modulo Theories co-located with the 36th Intl. Conf. Computer Aided Verification (CAV 2024). CEUR Workshop Proceedings, vol. 3725, pp. 13–23. CEUR-WS.org, Montreal, Canada (2024)

13. Cousineau, D., Dowek, G.: Embedding pure type systems in the Lambda-Pi-Calculus Modulo. In: Typed Lambda Calculi and Applications. pp. 102–117. Springer, Berlin, Heidelberg (2007)

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

15. Giesl, J., Brockschmidt, M., Emmes, F., Frohn, F., Fuhs, C., Otto, C., Plücker, M., Schneider-Kamp, P., Ströder, T., Swiderski, S., Thiemann, R.: Proving termination of programs automatically with AProVE. In: Automated Reasoning. pp. 184–191. Springer International Publishing, Cham (2014)
16. Grégoire, B., Mahboubi, A.: Proving equalities in a commutative ring done right in Coq. In: Hurd, J., Melham, T. (eds.) Theorem Proving in Higher Order Logics. pp. 98–113. Springer Berlin Heidelberg, Berlin, Heidelberg (2005)

17. Harper, R., Honsell, F., Plotkin, G.D.: A framework for defining logics. J. ACM **40**, 143–184 (1993), https://api.semanticscholar.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, Germany (2020)

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

20. de Moura, L., Ullrich, S.: The Lean 4 theorem prover and programming language. In: Automated Deduction – CADE 28: 28th International Conference on Automated Deduction, Virtual Event, July 12–15, 2021, Proceedings. p. 625–635. Springer-Verlag, Berlin, Heidelberg (2021)

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: Automated Deduction – CADE 28. pp. 450–467. Springer International Publishing, Cham (2021)

24. Schurr, H.J., Fleury, M., Barbosa, H., Fontaine, P.: Alethe: Towards a generic SMT proof format (extended abstract). Electronic Proceedings in Theoretical Computer Science **336**, 49–54 (07 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. https://rocq-prover.org/doc/V9.0.0/refman/index.html (2025)

27. Zankl, H., Felgenhauer, B., Middeldorp, A.: CSI - A confluence tool. In: Bjørner, N.S., Sofronie-Stokkermans, V. (eds.) 23rd Intl. Conf. Automated Deduction (CADE-23). LNCS, vol. 6803, pp. 499–505. Springer, Wroclaw, Poland (2011)