diff --git a/spec/Makefile b/spec/Makefile
index e5e28ca4fd78707b01e8d37fa02173b8dd1b30ad..31b2d9c6ab2e072dcf548264c7e1fd64780e0e93 100644
--- a/spec/Makefile
+++ b/spec/Makefile
@@ -1,3 +1,6 @@
+backport:
+ latexmk -pdf -pvc -interaction=nonstopmode -shell-escape -lualatex spec
+
comments:
latexmk -pdf -shell-escape doc
diff --git a/spec/alethe_rules.tex b/spec/alethe_rules.tex
new file mode 100644
index 0000000000000000000000000000000000000000..b637ace8eb7aaa54408f39d49b5e48a8f4393a4b
--- /dev/null
+++ b/spec/alethe_rules.tex
@@ -0,0 +1,2042 @@
+\environment Typesetting
+\environment ThesisData
+
+\startcomponent AletheRules
+
+\starttitle[
+ title={The Alethe Proof Rules},
+ reference=apx:rules
+]
+\chapterannot{This section is based on an informally published reference
+of the Alethe proof format.
+It was originally written by me for the work in
+\in{Section}[sec:reconstruction]. Later\\ Haniel Barbosa,\\ Mathias Fleury, \\
+Pascal Fontaine contributed.
+}
+
+This appendix provides a list of all proof rules supported by
+Alethe. To make this long list more accessible, this section
+first lists multiple classes of proof rules. The classes are not
+mutually exclusive: for example, the \proofRule{la_generic} rule is
+both a linear arithmetic rule and introduces a tautology.
+The number in brackets is the position of the rule in the overall list
+of proof rules.
+\in{Table}[rule-tab:special] lists rules that serve a special purpose.
+\in{Table}[rule-tab:tautologies] lists all rules that introduce
+tautologies. That is, regular rules that do not use premises.
+
+The subsequent section, starting at \at{page}[sec:alethe:rules-list], defines
+all rules and provides example proofs for complicated rules.
+The index of proof rules at \at{page}[sec:alethe:rules-index] can be used
+to quickly find the definition of rules.
+
+\subject[sec:alethe:rules-overview]{Classifications of the Rules}
+
+\placetable[here][rule-tab:special]{Special rules.}{
+\setupTABLE[r][each][frame=off,style=\addff{table}]
+\setupTABLE[r][1][bottomframe=on,rulewidth=1pt]
+\setupTABLE[c][1][width=12em]
+\bTABLE[width=broad]
+ \bTR\bTD Rule \eTD\bTD Description \eTD\eTR
+ \bTR\bTD \ruleref{assume} \eTD\bTD Repetition of an input assumption. \eTD\eTR
+ \bTR\bTD \ruleref{hole} \eTD\bTD Placeholder for rules not defined here. \eTD\eTR
+ \bTR\bTD \ruleref{subproof} \eTD\bTD Concludes a subproof and discharges local assumptions. \eTD\eTR
+\eTABLE
+}
+
+\placetable[here][rule-tab:resolution]{Resolution and related rules.}{
+\setupTABLE[r][each][frame=off,style=\addff{table}]
+\setupTABLE[r][1][bottomframe=on,rulewidth=1pt]
+\setupTABLE[c][1][width=12em]
+\bTABLE[width=broad]
+ \bTR\bTD Rule \eTD\bTD Description \eTD\eTR
+ \bTR\bTD \ruleref{resolution} \eTD\bTD Chain resolution of two or more clauses. \eTD\eTR
+ \bTR\bTD \ruleref{th_resolution} \eTD\bTD As \proofRule{resolution}, but used by theory solvers. \eTD\eTR
+ \bTR\bTD \ruleref{tautology} \eTD\bTD Simplification of tautological clauses to $\top$. \eTD\eTR
+ \bTR\bTD \ruleref{contraction} \eTD\bTD Removal of duplicated literals. \eTD\eTR
+ \eTABLE
+}
+
+\page
+\placetable[here,split][rule-tab:tautologies]{Rules introducing tautologies.}{
+\setupTABLE[r][each][frame=off,style=\addff{table}]
+\setupTABLE[c][1][width=12em]
+\setupTABLE[r][1][bottomframe=on,rulewidth=1pt]
+\bTABLE[width=broad,split=repeat]
+\bTABLEhead
+\bTR\bTD Rule \eTD\bTD Conclusion \eTD\eTR
+\eTABLEhead
+\bTABLEbody
+\bTR\bTD \ruleref{true} \eTD\bTD $\top$ \eTD\eTR
+\bTR\bTD \ruleref{false} \eTD\bTD $\neg\bot$ \eTD\eTR
+\bTR\bTD \ruleref{not_not} \eTD\bTD $\neg(\neg\neg\varphi), \varphi$ \eTD\eTR
+\bTR\bTD \ruleref{la_generic} \eTD\bTD Tautologous disjunction of linear inequalities. \eTD\eTR
+\bTR\bTD \ruleref{lia_generic} \eTD\bTD Tautologous disjunction of linear integer inequalities. \eTD\eTR
+\bTR\bTD \ruleref{la_disequality} \eTD\bTD $t_1 ≈ t_2 \lor \neg (t_1 \leq t_2) \lor \neg (t_2 \leq t_1)$ \eTD\eTR
+\bTR\bTD \ruleref{la_totality} \eTD\bTD $t_1 \leq t_2 \lor t_2 \leq t_1$ \eTD\eTR
+\bTR\bTD \ruleref{la_tautology} \eTD\bTD A trivial linear tautology. \eTD\eTR
+\bTR\bTD \ruleref{forall_inst} \eTD\bTD Quantifier instantiation. \eTD\eTR
+\bTR\bTD \ruleref{refl} \eTD\bTD Reflexivity after applying the context. \eTD\eTR
+\bTR\bTD \ruleref{eq_reflexive} \eTD\bTD $t ≈ t$ without context. \eTD\eTR
+\bTR\bTD \ruleref{eq_transitive} \eTD\bTD $\neg (t_1 ≈ t_2) , \dots , \neg (t_{n-1} ≈ t_n) , t_1 ≈ t_n$ \eTD\eTR
+\bTR\bTD \ruleref{eq_congruent} \eTD\bTD $\neg (t_1 ≈ u_1) , \dots , \neg (t_n ≈ u_n) , f(t_1, \dots, t_n) ≈ f(u_1, \dots, u_n)$ \eTD\eTR
+\bTR\bTD \ruleref{eq_congruent_pred} \eTD\bTD $\neg (t_1 ≈ u_1) , \dots , \neg (t_n ≈ u_n) , P(t_1, \dots, t_n) ≈ P(u_1, \dots, u_n)$ \eTD\eTR
+\bTR\bTD \ruleref{qnt_cnf} \eTD\bTD Clausification of a quantified formula. \eTD\eTR
+\bTR\bTD \ruleref{and_pos} \eTD\bTD $\neg (\varphi_1 \land \dots \land \varphi_n) , \varphi_k $ \eTD\eTR
+\bTR\bTD \ruleref{and_neg} \eTD\bTD $ (\varphi_1 \land \dots \land \varphi_n), \neg\varphi_1 , \dots , \neg\varphi_n $ \eTD\eTR
+\bTR\bTD \ruleref{or_pos} \eTD\bTD $ \neg (\varphi_1 \lor \dots \lor \varphi_n) , \varphi_1 , \dots , \varphi_n $ \eTD\eTR
+\bTR\bTD \ruleref{or_neg} \eTD\bTD $ (\varphi_1 \lor \dots \lor \varphi_n) , \neg \varphi_k $ \eTD\eTR
+\bTR\bTD \ruleref{xor_pos1} \eTD\bTD $ \neg (\varphi_1 \,\lsymb{xor}\, \varphi_2) , \varphi_1 , \varphi_2 $ \eTD\eTR
+\bTR\bTD \ruleref{xor_pos2} \eTD\bTD $ \neg (\varphi_1 \,\lsymb{xor}\, \varphi_2), \neg \varphi_1, \neg \varphi_2 $ \eTD\eTR
+\bTR\bTD \ruleref{xor_neg1} \eTD\bTD $ \varphi_1 \,\lsymb{xor}\, \varphi_2, \varphi_1 , \neg \varphi_2 $ \eTD\eTR
+\bTR\bTD \ruleref{xor_neg2} \eTD\bTD $ \varphi_1 \,\lsymb{xor}\, \varphi_2, \neg \varphi_1 , \varphi_2 $ \eTD\eTR
+\bTR\bTD \ruleref{implies_pos} \eTD\bTD $ \neg (\varphi_1 \rightarrow \varphi_2), \neg \varphi_1 , \varphi_2 $ \eTD\eTR
+\bTR\bTD \ruleref{implies_neg1} \eTD\bTD $ \varphi_1 \rightarrow \varphi_2, \varphi_1 $ \eTD\eTR
+\bTR\bTD \ruleref{implies_neg2} \eTD\bTD $ \varphi_1 \rightarrow \varphi_2, \neg \varphi_2 $ \eTD\eTR
+\bTR\bTD \ruleref{equiv_pos1} \eTD\bTD $\neg (\varphi_1 ≈ \varphi_2) , \varphi_1 , \neg \varphi_2$ \eTD\eTR
+\bTR\bTD \ruleref{equiv_pos2} \eTD\bTD $\neg (\varphi_1 ≈ \varphi_2) , \neg \varphi_1 , \varphi_2$ \eTD\eTR
+\bTR\bTD \ruleref{equiv_neg1} \eTD\bTD $\varphi_1 ≈ \varphi_2 , \neg \varphi_1 , \neg \varphi_2$ \eTD\eTR
+\bTR\bTD \ruleref{equiv_neg2} \eTD\bTD $\varphi_1 ≈ \varphi_2 , \varphi_1 , \varphi_2$ \eTD\eTR
+\bTR\bTD \ruleref{ite_pos1} \eTD\bTD $\neg (\lsymb{ite} \varphi_1\;\varphi_2\;\varphi_3) , \varphi_1 , \varphi_3$ \eTD\eTR
+\bTR\bTD \ruleref{ite_pos2} \eTD\bTD $\neg (\lsymb{ite} \varphi_1\;\varphi_2\;\varphi_3) , \neg \varphi_1 , \varphi_2$ \eTD\eTR
+\bTR\bTD \ruleref{ite_neg1} \eTD\bTD $\lsymb{ite} \varphi_1\;\varphi_2\;\varphi_3 , \varphi_1 , \neg \varphi_3$ \eTD\eTR
+\bTR\bTD \ruleref{ite_neg2} \eTD\bTD $\lsymb{ite} \varphi_1\;\varphi_2\;\varphi_3 , \neg \varphi_1 , \neg \varphi_2$ \eTD\eTR
+\bTR\bTD \ruleref{connective_def} \eTD\bTD Definition of the Boolean connectives. \eTD\eTR
+\bTR\bTD \ruleref{and_simplify} \eTD\bTD Simplification of a conjunction. \eTD\eTR
+\bTR\bTD \ruleref{or_simplify} \eTD\bTD Simplification of a disjunction. \eTD\eTR
+\bTR\bTD \ruleref{not_simplify} \eTD\bTD Simplification of a Boolean negation. \eTD\eTR
+\bTR\bTD \ruleref{implies_simplify} \eTD\bTD Simplification of an implication. \eTD\eTR
+\bTR\bTD \ruleref{equiv_simplify} \eTD\bTD Simplification of an equivalence. \eTD\eTR
+\bTR\bTD \ruleref{bool_simplify} \eTD\bTD Simplification of combined Boolean connectives. \eTD\eTR
+\bTR\bTD \ruleref{ac_simp} \eTD\bTD Flattening of nested $\lor$ or $\land$. \eTD\eTR
+\bTR\bTD \ruleref{ite_simplify} \eTD\bTD Simplification of if-then-else. \eTD\eTR
+\bTR\bTD \ruleref{qnt_simplify} \eTD\bTD Simplification of constant quantified formulas. \eTD\eTR
+\bTR\bTD \ruleref{qnt_join} \eTD\bTD Joining of consecutive quantifiers. \eTD\eTR
+\bTR\bTD \ruleref{qnt_rm_unused} \eTD\bTD Removal of unused quantified variables. \eTD\eTR
+\bTR\bTD \ruleref{eq_simplify} \eTD\bTD Simplification of equality. \eTD\eTR
+\bTR\bTD \ruleref{div_simplify} \eTD\bTD Simplification of division. \eTD\eTR
+\bTR\bTD \ruleref{prod_simplify} \eTD\bTD Simplification of products. \eTD\eTR
+\bTR\bTD \ruleref{unary_minus_simplify} \eTD\bTD Simplification of the unary minus. \eTD\eTR
+\bTR\bTD \ruleref{minus_simplify} \eTD\bTD Simplification of subtractions. \eTD\eTR
+\bTR\bTD \ruleref{sum_simplify} \eTD\bTD Simplification of sums. \eTD\eTR
+\bTR\bTD \ruleref{comp_simplify} \eTD\bTD Simplification of arithmetic comparisons. \eTD\eTR
+\bTR\bTD \ruleref{distinct_elim} \eTD\bTD Elimination of the distinction predicate. \eTD\eTR
+\bTR\bTD \ruleref{la_rw_eq} \eTD\bTD $(t ≈ u) ≈ (t \leq u \land u \leq t)$ \eTD\eTR
+\bTR\bTD \ruleref{nary_elim} \eTD\bTD Replace $n$-ary operators with binary application. \eTD\eTR
+\eTABLEbody
+\eTABLE
+}
+
+\placetable[here,split][rule-tab:la-tauts]{Linear arithmetic rules.}{
+\setupTABLE[r][each][frame=off,style=\addff{table}]
+\setupTABLE[c][1][width=12em]
+\setupTABLE[r][1][bottomframe=on,rulewidth=1pt]
+\bTABLE[width=broad,split=repeat]
+\bTABLEhead\bTR\bTD Rule \eTD\bTD Conclusion \eTD\eTR\eTABLEhead
+\bTABLEbody
+\bTR\bTD\ruleref{la_generic} \eTD\bTD Tautologous disjunction of linear inequalities. \eTD\eTR
+\bTR\bTD\ruleref{lia_generic} \eTD\bTD Tautologous disjunction of linear integer inequalities. \eTD\eTR
+\bTR\bTD\ruleref{la_disequality} \eTD\bTD $t_1 ≈ t_2 \lor \neg (t_1 \leq t_2) \lor \neg (t_2 \leq t_1)$ \eTD\eTR
+\bTR\bTD\ruleref{la_totality} \eTD\bTD $t_1 \leq t_2 \lor t_2 \leq t_1$ \eTD\eTR
+\bTR\bTD\ruleref{la_tautology} \eTD\bTD A trivial linear tautology. \eTD\eTR
+\bTR\bTD\ruleref{la_rw_eq} \eTD\bTD $(t ≈ u) ≈ (t \leq u \land u \leq t)$ \eTD\eTR
+\bTR\bTD\ruleref{div_simplify} \eTD\bTD Simplification of division. \eTD\eTR
+\bTR\bTD\ruleref{prod_simplify} \eTD\bTD Simplification of products. \eTD\eTR
+\bTR\bTD\ruleref{unary_minus_simplify} \eTD\bTD Simplification of the unary minus. \eTD\eTR
+\bTR\bTD\ruleref{minus_simplify} \eTD\bTD Simplification of subtractions. \eTD\eTR
+\bTR\bTD\ruleref{sum_simplify} \eTD\bTD Simplification of sums. \eTD\eTR
+\bTR\bTD\ruleref{comp_simplify} \eTD\bTD Simplification of arithmetic comparisons. \eTD\eTR
+\eTABLEbody\eTABLE}
+
+\page
+\placetable[here,split][rule-tab:quants]{Quantifier handling.}{
+\setupTABLE[r][each][frame=off,style=\addff{table}]
+\setupTABLE[c][1][width=12em]
+\setupTABLE[r][1][bottomframe=on,rulewidth=1pt]
+\bTABLE[width=broad,split=repeat]
+\bTABLEhead\bTR\bTD Rule \eTD\bTD Conclusion \eTD\eTR\eTABLEhead
+\bTABLEbody
+\bTR\bTD\ruleref{forall_inst} \eTD\bTD Instantiation of a universal variable. \eTD\eTR
+\bTR\bTD\ruleref{bind} \eTD\bTD Renaming of bound variables. \eTD\eTR
+\bTR\bTD\ruleref{sko_ex} \eTD\bTD Skolemization of existential variables. \eTD\eTR
+\bTR\bTD\ruleref{sko_forall} \eTD\bTD Skolemization of universal variables. \eTD\eTR
+\bTR\bTD\ruleref{qnt_cnf} \eTD\bTD Clausification of quantified formulas. \eTD\eTR
+\bTR\bTD\ruleref{qnt_simplify} \eTD\bTD Simplification of constant quantified formulas. \eTD\eTR
+\bTR\bTD\ruleref{onepoint} \eTD\bTD The one-point rule. \eTD\eTR
+\bTR\bTD\ruleref{qnt_join} \eTD\bTD Joining of consecutive quantifiers. \eTD\eTR
+\bTR\bTD\ruleref{qnt_rm_unused} \eTD\bTD Removal of unused quantified variables. \eTD\eTR
+\eTABLEbody\eTABLE}
+
+
+\placetable[here,split][rule-tab:skos]{Skolemization rules.}{
+\setupTABLE[r][each][frame=off,style=\addff{table}]
+\setupTABLE[c][1][width=12em]
+\setupTABLE[r][1][bottomframe=on,rulewidth=1pt]
+\bTABLE[width=broad,split=repeat]
+\bTABLEhead\bTR\bTD Rule \eTD\bTD Conclusion \eTD\eTR\eTABLEhead
+\bTABLEbody
+\bTR\bTD\ruleref{sko_ex} \eTD\bTD Skolemization of existential variables. \eTD\eTR
+\bTR\bTD\ruleref{sko_forall} \eTD\bTD Skolemization of universal variables. \eTD\eTR
+\eTABLEbody\eTABLE}
+
+
+\placetable[here,split][rule-tab:clausification]{Clausification rules. These rules can be used to perform propositional
+clausification.}{
+\setupTABLE[r][each][frame=off,style=\addff{table}]
+\setupTABLE[c][1][width=12em]
+\setupTABLE[r][1][bottomframe=on,rulewidth=1pt]
+\bTABLE[width=broad,split=repeat]
+\bTABLEhead\bTR\bTD Rule \eTD\bTD Conclusion \eTD\eTR\eTABLEhead
+\bTABLEbody
+\bTR\bTD\ruleref{and} \eTD\bTD And elimination. \eTD\eTR
+\bTR\bTD\ruleref{not_or} \eTD\bTD Elimination of a negated disjunction. \eTD\eTR
+\bTR\bTD\ruleref{or} \eTD\bTD Disjunction to clause. \eTD\eTR
+\bTR\bTD\ruleref{not_and} \eTD\bTD Distribution of negation over a conjunction. \eTD\eTR
+\bTR\bTD\ruleref{xor1} \eTD\bTD From $\,\lsymb{xor}\, \varphi_1 \varphi_2$ to $\varphi_1, \varphi_2$. \eTD\eTR
+\bTR\bTD\ruleref{xor2} \eTD\bTD From $\,\lsymb{xor}\, \varphi_1 \varphi_2$ to $\neg\varphi_1, \neg\varphi_2$. \eTD\eTR
+\bTR\bTD\ruleref{not_xor1} \eTD\bTD From $\neg(\,\lsymb{xor}\, \varphi_1 \varphi_2)$ to $\varphi_1, \neg\varphi_2$. \eTD\eTR
+\bTR\bTD\ruleref{not_xor2} \eTD\bTD From $\neg(\,\lsymb{xor}\, \varphi_1 \varphi_2)$ to $\neg\varphi_1, \varphi_2$. \eTD\eTR
+\bTR\bTD\ruleref{implies} \eTD\bTD From $ \varphi_1\rightarrow\varphi_2 $ to $\neg\varphi_1 , \varphi_2 $. \eTD\eTR
+\bTR\bTD\ruleref{not_implies1} \eTD\bTD From $\neg (\varphi_1\rightarrow\varphi_2)$ to $\varphi_1$. \eTD\eTR
+\bTR\bTD\ruleref{not_implies2} \eTD\bTD From $\neg (\varphi_1\rightarrow\varphi_2)$ to $\neg\varphi_2$. \eTD\eTR
+\bTR\bTD\ruleref{equiv1} \eTD\bTD From $ \varphi_1≈\varphi_2$ to $\neg\varphi_1 , \varphi_2$. \eTD\eTR
+\bTR\bTD\ruleref{equiv2} \eTD\bTD From $ \varphi_1≈\varphi_2$ to $\varphi_1 , \neg\varphi_2$. \eTD\eTR
+\bTR\bTD\ruleref{not_equiv1} \eTD\bTD From $\neg(\varphi_1≈\varphi_2)$ to $\varphi_1 , \varphi_2$. \eTD\eTR
+\bTR\bTD\ruleref{not_equiv2} \eTD\bTD From $\neg(\varphi_1≈\varphi_2)$ to $\neg\varphi_1 , \neg\varphi_2$. \eTD\eTR
+\bTR\bTD\ruleref{and_pos} \eTD\bTD $\neg (\varphi_1 \land \dots \land \varphi_n), \varphi_k$\eTD\eTR
+\bTR\bTD\ruleref{and_neg} \eTD\bTD $(\varphi_1 \land \dots \land \varphi_n), \neg\varphi_1, \dots , \neg\varphi_n $ \eTD\eTR
+\bTR\bTD\ruleref{or_pos} \eTD\bTD $\neg (\varphi_1 \lor \dots \lor \varphi_n) , \varphi_1 , \dots
+ , \varphi_n $ \eTD\eTR
+\bTR\bTD\ruleref{or_neg} \eTD\bTD
+$ (\varphi_1 \lor \dots \lor \varphi_n) , \neg \varphi_k $\eTD\eTR
+\bTR\bTD\ruleref{xor_pos1} \eTD\bTD
+$ \neg (\varphi_1 \,\lsymb{xor}\, \varphi_2) , \varphi_1 , \varphi_2 $ \eTD\eTR
+\bTR\bTD\ruleref{xor_pos2} \eTD\bTD
+$ \neg (\varphi_1 \,\lsymb{xor}\, \varphi_2)
+, \neg \varphi_1, \neg \varphi_2 $ \eTD\eTR
+\bTR\bTD\ruleref{xor_neg1} \eTD\bTD
+$ \varphi_1 \,\lsymb{xor}\, \varphi_2, \varphi_1 , \neg \varphi_2 $ \eTD\eTR
+\bTR\bTD\ruleref{xor_neg2} \eTD\bTD
+$ \varphi_1 \,\lsymb{xor}\, \varphi_2, \neg \varphi_1 , \varphi_2 $ \eTD\eTR
+\bTR\bTD\ruleref{implies_pos} \eTD\bTD
+$ \neg (\varphi_1 \rightarrow \varphi_2), \neg \varphi_1 , \varphi_2 $ \eTD\eTR
+\bTR\bTD\ruleref{implies_neg1} \eTD\bTD
+$ \varphi_1 \rightarrow \varphi_2, \varphi_1 $ \eTD\eTR
+\bTR\bTD\ruleref{implies_neg2} \eTD\bTD
+$ \varphi_1 \rightarrow \varphi_2, \neg \varphi_2 $ \eTD\eTR
+\bTR\bTD\ruleref{equiv_pos1} \eTD\bTD
+$\neg (\varphi_1 ≈ \varphi_2) , \varphi_1 , \neg \varphi_2$ \eTD\eTR
+\bTR\bTD\ruleref{equiv_pos2} \eTD\bTD
+$\neg (\varphi_1 ≈ \varphi_2) , \neg \varphi_1 , \varphi_2$ \eTD\eTR
+\bTR\bTD\ruleref{equiv_neg1} \eTD\bTD
+$\varphi_1 ≈ \varphi_2 , \neg \varphi_1 , \neg \varphi_2$ \eTD\eTR
+\bTR\bTD\ruleref{equiv_neg2} \eTD\bTD
+$\varphi_1 ≈ \varphi_2 , \varphi_1 , \varphi_2$ \eTD\eTR
+\bTR\bTD\ruleref{let} \eTD\bTD Elimination of the $\lsymb{let}$ operator. \eTD\eTR
+\bTR\bTD\ruleref{distinct_elim} \eTD\bTD Elimination of the $\lsymb{distinct}$ operator. \eTD\eTR
+\bTR\bTD\ruleref{nary_elim} \eTD\bTD Elimination of n-ary application of operators. \eTD\eTR
+\eTABLEbody\eTABLE}
+
+\page
+\placetable[here,split][rule-tab:simplification]{Simplification rules. These rules represent typical operator-level
+simplifications.}{
+\setupTABLE[r][each][frame=off,style=\addff{table}]
+\setupTABLE[c][1][width=12em]
+\setupTABLE[r][1][bottomframe=on,rulewidth=1pt]
+\bTABLE[width=broad,split=repeat]
+\bTABLEhead\bTR\bTD Rule \eTD\bTD Conclusion \eTD\eTR\eTABLEhead
+\bTABLEbody
+\bTR\bTD\ruleref{connective_def} \eTD\bTD Definition of the Boolean connectives. \eTD\eTR
+\bTR\bTD\ruleref{and_simplify} \eTD\bTD Simplification of a conjunction. \eTD\eTR
+\bTR\bTD\ruleref{or_simplify} \eTD\bTD Simplification of a disjunction. \eTD\eTR
+\bTR\bTD\ruleref{not_simplify} \eTD\bTD Simplification of a Boolean negation. \eTD\eTR
+\bTR\bTD\ruleref{implies_simplify} \eTD\bTD Simplification of an implication. \eTD\eTR
+\bTR\bTD\ruleref{equiv_simplify} \eTD\bTD Simplification of an equivalence. \eTD\eTR
+\bTR\bTD\ruleref{bool_simplify} \eTD\bTD Simplification of combined Boolean connectives. \eTD\eTR
+\bTR\bTD\ruleref{ac_simp} \eTD\bTD Simplification of nested disjunctions and conjunctions. \eTD\eTR
+\bTR\bTD\ruleref{ite_simplify} \eTD\bTD Simplification of if-then-else. \eTD\eTR
+\bTR\bTD\ruleref{qnt_simplify} \eTD\bTD Simplification of constant quantified formulas. \eTD\eTR
+\bTR\bTD\ruleref{onepoint} \eTD\bTD The one-point rule. \eTD\eTR
+\bTR\bTD\ruleref{qnt_join} \eTD\bTD Joining of consecutive quantifiers. \eTD\eTR
+\bTR\bTD\ruleref{qnt_rm_unused} \eTD\bTD Removal of unused quantified variables. \eTD\eTR
+\bTR\bTD\ruleref{eq_simplify} \eTD\bTD Simplification of equalities. \eTD\eTR
+\bTR\bTD\ruleref{div_simplify} \eTD\bTD Simplification of division. \eTD\eTR
+\bTR\bTD\ruleref{prod_simplify} \eTD\bTD Simplification of products. \eTD\eTR
+\bTR\bTD\ruleref{unary_minus_simplify} \eTD\bTD Simplification of the unary minus. \eTD\eTR
+\bTR\bTD\ruleref{minus_simplify} \eTD\bTD Simplification of subtractions. \eTD\eTR
+\bTR\bTD\ruleref{sum_simplify} \eTD\bTD Simplification of sums. \eTD\eTR
+\bTR\bTD\ruleref{comp_simplify} \eTD\bTD Simplification of arithmetic comparisons. \eTD\eTR
+\bTR\bTD\ruleref{qnt_simplify} \eTD\bTD Simplification of constant quantified formulas. \eTD\eTR
+\eTABLEbody\eTABLE}
+\stopsection
+
+\page
+\subject[sec:alethe:rules-list]{Rule List}
+
+\startRuleDescription{assume}
+\startAletheS
+\setupTABLE[c][3][width=27em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD
+$\varphi$ \eTD\bTD \currule \eTD\eTR
+\stopAlethe
+
+ where $\varphi$ corresponds up to the orientation of equalities
+ to a formula asserted in the input problem.
+ \starttightpara{Remark.}
+ This rule can not be used by the
+ \inlineAlethe{(step }\dots\inlineAlethe{)} command. Instead it corresponds to the dedicated
+ \inlineAlethe{(assume }\dots\inlineAlethe{)} command.
+
+ \stoptightpara
+\stopRuleDescription
+
+\startRuleDescription{hole}
+\startAlethe
+\setupTABLE[c][3][width=15.3em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD
+$\varphi$ \eTD\bTD (\currule\; p_1, \dots, p_n)\, [a_1, \dots, a_n] \eTD\eTR
+\stopAlethe
+
+\noindent
+where $\varphi$ is any well-formed formula.
+
+This rule can be used to express holes in the proof. It can be used by
+solvers as a placeholder for proof steps that are not yet expressed
+by the proof rules in this document. A proof checker {\em must not}
+accept a proof as valid that contains this rule even if the checker can
+somehow check this rule. However, it is possible for checkers to have
+a dedicated status for proofs that contain this rule and are otherwise
+valid. Any other tool can accept or reject proofs that contain this rule.
+
+The premises and arguments are arbitrary, but must follow the syntax
+for premises and arguments.
+
+\stopRuleDescription
+
+\startRuleDescription{true}
+\startAlethe
+\setupTABLE[c][3][width=27.5em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD
+$\top$ \eTD\bTD \currule \eTD\eTR
+\stopAlethe
+\stopRuleDescription
+
+\startRuleDescription{false}
+\startAlethe
+\setupTABLE[c][3][width=27.5em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD
+$\bot$ \eTD\bTD \currule \eTD\eTR
+\stopAlethe
+\stopRuleDescription
+
+\startRuleDescription{not_not}
+
+\startAlethe
+\setupTABLE[c][3][width=27.5em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD
+$\neg (\neg \neg \varphi)$, $\varphi$ \eTD\bTD \currule \eTD\eTR
+\stopAlethe
+
+\tightpara{Remark.} This rule is useful to remove double negations from a
+clause by resolving a clause with the double negation on $\varphi$.
+\stopRuleDescription
+
+\page
+\startRuleDescription{th_resolution}
+This rule is the resolution of two or more clauses.
+\startAlethe
+\setupTABLE[c][3][width=20.1em]
+\bTR\bTD $i_1$.\eTD\bTD \ctxsep \eTD\bTD $l^1_1$, \dots, $l^1_{k^1}$ \eTD\bTD ($\ruleType{...}$) \eTD\eTR
+\aletheLine
+\bTR\bTD $i_n$.\eTD\bTD \ctxsep \eTD\bTD $l^n_1$, \dots, $l^n_{k^n}$ \eTD\bTD $ (\ruleType{...}$) \eTD\eTR
+\bTR\bTD $j$.\eTD\bTD \ctxsep \eTD\bTD $l^{r_1}_{s_1}$, \dots, $l^{r_m}_{s_m}$ \eTD\bTD ($\currule\;i_1,\dots, i_n)$ \eTD\eTR
+\stopAlethe
+
+\noindent
+where $l^{r_1}_{s_1} , \dots , l^{r_m}_{s_m}$ are from $l^{i}_{j}$ and
+are the result of a chain of predicate resolution steps on the clauses of
+$i_1$ to $i_n$. It is possible that $m = 0$, i.e. that
+the result is the empty clause. When performing resolution steps, the
+rule implicitly merges repeated negations at the start of the formulas
+$l^{i}_{j}$. For example, the formulas $\neg\neg\neg P$ and $\neg\neg P$
+can serve as pivots during resolution. The first formula is interpreted as
+$\neg P$ and the second as just $P$ for the purpose of performing resolution
+steps.
+
+This rule is only used when the resolution step is not emitted by the SAT solver.
+See the equivalent \proofRule{resolution} rule for the rule emitted by the
+SAT solver.
+
+\tightpara{Remark.} The definition given here is very general. The motivation
+for this to ensure the definition covers all possible resolution steps generated
+by the existing proof generation code in veriT. It will be restricted after
+a full review of the code. As a consequence of this checking this rule is
+theoretically NP-complete. In practice, however, the \currule-steps
+produced by {\verit} are simple. Experience with reconstructing the step in
+{\isabelle} shows that checking can done by naive decision procedures. The
+vast majority of \currule-steps are binary resolution steps.
+\stopRuleDescription
+
+\startRuleDescription{resolution}
+This rule is equivalent to the \proofRule{th_resolution} rule, but it is
+emitted by the SAT solver instead of theory reasoners. The differentiation
+serves only informational purpose.
+
+\stopRuleDescription
+
+\startRuleDescription{tautology}
+
+\startAlethe
+\setupTABLE[c][3][width=25em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD
+$l_1$, \dots, $l_k$, \dots, $l_m$, \dots, $l_n$ \eTD\bTD (\dots) \eTD\eTR
+\bTR\bTD $j$.\eTD\bTD \ctxsep \eTD\bTD
+$\top$ \eTD\bTD (\currule\; $i$) \eTD\eTR
+\stopAlethe
+
+\noindent
+ and $l_k$, $l_m$ are such that
+ \startformula\startalign
+ \NC l_k \NC= \underbrace{\neg \dots \neg}_o \varphi \NR
+ \NC l_m \NC= \underbrace{\neg \dots \neg}_p \varphi
+ \stopalign\stopformula
+ and one of $o, p$\/ is odd and the other even. Either can be $0$.
+\stopRuleDescription
+
+\startRuleDescription{contraction}
+\startAlethe
+\setupTABLE[c][3][width=24.4em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD
+$l_1$, \dots, $l_n$ \eTD\bTD (\dots) \eTD\eTR
+\bTR\bTD $j$.\eTD\bTD \ctxsep \eTD\bTD
+$l_{k_1}$, \dots, $l_{k_m}$ \eTD\bTD (\currule\; $i$) \eTD\eTR
+\stopAlethe
+
+\noindent
+ where $m \leq n$ and $k_1 \dots k_m$ is a monotonic map to $1 \dots n$
+ such that $l_{k_1} \dots l_{k_m}$ are pairwise distinct and
+ $\{l_1, \dots, l_n\} = \{l_{k_1}, \dots, l_{k_m}\}$.
+ Hence, this rule removes duplicated literals.
+\stopRuleDescription
+
+
+\startRuleDescription{subproof}
+The \currule{} rule completes a subproof and discharges local
+assumptions. Every subproof starts with some \proofRule{assume} steps. The
+last step of the subproof is the conclusion.
+
+\startAlethe
+\bTR\bTD $i_1$.\eTD\bTD[leftframe=on] \ctxsep \eTD\bTD $\varphi_1$ \eTD\bTD $\proofRule{assume}$ \eTD\eTR
+\aletheLineB
+\bTR\bTD $i_n$.\eTD\bTD[leftframe=on] \ctxsep \eTD\bTD $\varphi_n$ \eTD\bTD $\proofRule{assume}$ \eTD\eTR
+\aletheLineB
+\bTR[bottomframe=on]\bTD[bottomframe=off] $j$.\eTD\bTD[leftframe=on] \ctxsep \eTD\bTD $\psi$ \eTD\bTD (\dots) \eTD\eTR
+\bTR\bTD k.\eTD\bTD \ctxsep \eTD\bTD $\neg\varphi_1$,\dots, $\neg\varphi_n$, $\psi$ \eTD\bTD $\proofRule{subproof}$ \eTD\eTR
+\stopAlethe
+
+\stopRuleDescription
+
+\startRuleDescription{la_generic}
+A step of the \currule{} rule represents a tautological clause of linear
+disequalities. It can be checked by showing that the conjunction of
+the negated disequalities is unsatisfiable. After the application of
+some strengthening rules, the resulting conjunction is unsatisfiable,
+even if integer variables are assumed to be real variables.
+
+A linear inequality is of term of the form
+\startformula
+\sum_{i=0}^{n}c_i\times{}t_i +
+d_1\bowtie \sum_{i=n+1}^{m} c_i\times{}t_i + d_2
+\stopformula
+where $\bowtie\;\in \{≈, <,
+>, \leq, \geq\}$, where $m\geq n$, $c_i, d_1, d_2$ are either integer or real
+constants, and for each $i$ $c_i$ and $t_i$ have the same sort. We will write
+$s_1 \bowtie s_2$.
+
+Let $l_1,\dots, l_n$ be linear inequalities and $a_1, \dots, a_n$
+rational numbers, then a {\currule} step has the form
+
+\startAlethe
+\setupTABLE[c][3][width=21em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD
+$\varphi_1$, \dots , $\varphi_o$ \eTD\bTD \currule\, [$a_1$, \dots, $a_o$] \eTD\eTR
+\stopAlethe
+
+\noindent
+where $\varphi_i$ is either $\neg l_i$ or $l_i$, but never $s_1
+≈ s_2$.
+
+If the current theory does not have rational numbers, then the $a_i$ are
+printed using integer division. They should, nevertheless, be interpreted
+as rational numbers. If $d_1$ or $d_2$ are $0$, they might not be printed.
+
+To check the unsatisfiability of the negation of $\varphi_1\lor \dots
+\lor \varphi_o$ one performs the following steps for each literal. For
+each $i$, let $\varphi := \varphi_i$ and $a := a_i$.
+
+\startitemize[n,packed]
+ \item If $\varphi = s_1 > s_2$, then let $\varphi := s_1 \leq s_2$.
+ If $\varphi = s_1 \geq s_2$, then let $\varphi := s_1 < s_2$.
+ If $\varphi = s_1 < s_2$, then let $\varphi := s_1 \geq s_2$.
+ If $\varphi = s_1 \leq s_2$, then let $\varphi := s_1 > s_2$. This negates
+ the literal.
+ \item If $\varphi = \neg (s_1 \bowtie s_2)$, then let $\varphi := s_1 \bowtie s_2$.
+ \item Replace $\varphi$ by $\sum_{i=0}^{n}c_i\times{}t_i - \sum_{i=n+1}^{m} c_i\times{}t_i
+ \bowtie d$ where $d := d_2 - d_1$.
+ \item Now $\varphi$ has the form $s_1 \bowtie d$. If all
+ variables in $s_1$ are integer sorted: replace $\bowtie d$ according to
+ \in{Table}[tbl:lageneric].
+ \item If $\bowtie$ is $≈$ replace $l$ by
+ $\sum_{i=0}^{m}a\times{}c_i\times{}t_i ≈ a\times{}d$, otherwise replace it by
+ $\sum_{i=0}^{m}|a|\times{}c_i\times{}t_i ≈ |a|\times{}d$.
+\stopitemize
+
+\placetable[here][tbl:lageneric]{Strengthening rules for \currule{}.}{
+ \bTABLE
+ \setupTABLE[r][each][frame=off]
+ \setupTABLE[c][each][roffset=0.5em]
+ \setupTABLE[r][1][bottomframe=on]
+\bTR\bTD $\bowtie$ \eTD\bTD If $d$ is an integer \eTD\bTD Otherwise \eTD\eTR
+\bTR\bTD $>$ \eTD\bTD $\geq d + 1$ \eTD\bTD $\geq \lfloor d\rfloor + 1$ \eTD\eTR
+\bTR\bTD $\geq$ \eTD\bTD $\geq d$ \eTD\bTD $\geq \lfloor d\rfloor + 1$ \eTD\eTR
+ \eTABLE
+}
+
+Finally, the sum of the resulting literals is trivially contradictory.
+The sum
+\startformula
+ \sum_{k=1}^{o}\sum_{i=1}^{m^o}c_i^k*t_i^k \bowtie \sum_{k=1}^{o}d^k
+\stopformula
+where $c_i^k$ is the constant $c_i$ of literal $l_k$, $t_i^k$ is the term
+$t_i$ of $l_k$, and $d^k$ is the constant $d$ of $l_k$. The operator
+$\bowtie$ is $≈$ if all operators are $≈$, $>$ if all are
+either $≈$ or $>$, and $\geq$ otherwise. The $a_i$ must be such
+that the sum on the left-hand side is $0$ and the right-hand side is $>0$ (or
+$\geq 0$ if $\bowtie$ is $>$).
+\stopRuleDescription
+
+% For some reason verbatim doesn't work in the enumerate environment
+\startruleexample
+A simple \currule{} step in the logic LRA might look like this:
+
+\startSMTCode
+(step t10 (cl (not (> (f a) (f b))) (not (= (f a) (f b))))
+ :rule la_generic :args (1.0 (- 1.0)))
+\stopSMTCode
+
+To verify this we have to check the insatisfiability of $(f\,a) > (f\,b) \land
+(f\,a) ≈ (f\,b)$ (step 2). After step~3 we get $(f\,a) - (f\,b) > 0 \land
+(f\,a) - (f\,b) ≈ 0$. Since we don't have an integer sort in this logic step~4 does
+not apply. Finally, after step~5 the conjunction is $(f\,a) - (f\,b) > 0 \land
+- (f\,a) + (f\,b) ≈ 0$. This sums to $0 > 0$, which is a contradiction.
+\stopruleexample
+
+\startruleexample
+The following \currule{} step is from a {\ss QF\_UFLIA} problem:
+\startSMTCode
+(step t11 (cl (not (<= f3 0)) (<= (+ 1 (* 4 f3)) 1))
+ :rule la_generic :args (1 (div 1 4)))
+\stopSMTCode
+After normalization we get $-f_3 \geq 0 \land 4\times f_3 > 0$.
+This time step~4 applies and we can strengthen this to
+$-f_3 \geq 0 \land 4\times f_3 \geq 1$ and after multiplication we get
+$-f_3 \geq 0 \land f_3 \geq ¼$. Which sums to the contradiction
+$¼ \geq 0$.
+\stopruleexample
+
+\startRuleDescription{lia_generic}
+This rule is a placeholder rule for integer arithmetic solving. It takes the
+same form as \proofRule{la_generic}, without the additional arguments.
+
+\startAlethe
+\setupTABLE[c][3][width=24em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD
+$\varphi_1$, \dots , $\varphi_o$ \eTD\bTD (\currule) \eTD\eTR
+\stopAlethe
+
+\noindent
+with $\varphi_i$ being linear inequalities. The disjunction
+$\varphi_1\lor \dots \lor \varphi_n$ is a tautology in the theory of linear
+integer arithmetic.
+
+\tightpara{Remark.} Since this rule can introduce a disjunction of arbitrary
+linear integer inequalities without any additional hints, proof checking
+can be NP-hard. Hence, this rule should be avoided when possible.
+
+\stopRuleDescription
+
+\startRuleDescription{la_disequality}
+\startAlethe
+\setupTABLE[c][3][width=24em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD
+$t_1 ≈ t_2 \lor \neg (t_1 \leq t_2) \lor \neg (t_2 \leq t_1)$
+\eTD\bTD (\currule) \eTD\eTR
+\stopAlethe
+\stopRuleDescription
+
+\startRuleDescription{la_totality}
+\startAlethe
+\setupTABLE[c][3][width=24.5em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD
+$t_1 \leq t_2 \lor t_2 \leq t_1$
+\eTD\bTD (\currule) \eTD\eTR
+\stopAlethe
+\stopRuleDescription
+
+\startRuleDescription{la_tautology}
+This rule is a linear arithmetic tautology which can be checked without
+sophisticated reasoning. It has either the form
+
+\startAlethe
+\setupTABLE[c][3][width=24.5em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD
+$\varphi$
+\eTD\bTD (\currule) \eTD\eTR
+\stopAlethe
+
+\noindent
+where $\varphi$ is either a linear inequality $s_1 \bowtie s_2$
+or $\neg(s_1 \bowtie s_2)$. After performing step 1 to 3 of the process for
+checking the \proofRule{la_generic} the result is trivially unsatisfiable.
+
+The second form handles bounds on linear combinations. It is binary clause:
+\startAlethe
+\setupTABLE[c][3][width=24.5em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD
+$\varphi_1 \lor \varphi_2$ % Checked: this is a proper disjunction not a cl
+\eTD\bTD (\currule) \eTD\eTR
+\stopAlethe
+
+It can be checked by using the procedure for \proofRule{la_generic} with
+while setting the arguments to $1$. Informally, the rule follows one of several
+cases:
+\startitemize[packed]
+ \item $\neg (s_1 \leq d_1) \lor s_1 \leq d_2$ where $d_1 \leq d_2$
+ \item $s_1 \leq d_1 \lor \neg (s_1 \leq d_2)$ where $d_1 = d_2$
+ \item $\neg (s_1 \geq d_1) \lor s_1 \geq d_2$ where $d_1 \geq d_2$
+ \item $s_1 \geq d_1 \lor \neg (s_1 \geq d_2)$ where $d_1 = d_2$
+ \item $\neg (s_1 \leq d_1) \lor \neg(s_1 \geq d_2)$ where $d_1 < d_2$
+\stopitemize
+The inequalities $s_1 \bowtie d$ are are the result of applying normalization
+as for the rule \proofRule{la_generic}.
+\stopRuleDescription
+
+\startRuleDescription{bind}
+ The \currule{} rule is used to rename bound variables.
+
+\startAletheS
+\setupTABLE[c][4][width=15.3em]
+\aletheLineS
+\bTR[bottomframe=on] \bTD[bottomframe=off] $j$.\eTD\bTD[leftframe=on]
+ $\Gamma, y_1,\dots, y_n, x_1 \mapsto y_1, \dots , x_n \mapsto y_n$
+ \eTD\bTD \ctxsep
+ \eTD\bTD
+ $\varphi ≈ \varphi'$
+ \eTD\bTD (\dots) \eTD\eTR
+\bTR\bTD $k$.\eTD \bTD \eTD
+ \bTD \ctxsep \eTD\bTD
+ $\forall x_1, \dots, x_n.\varphi ≈ \forall y_1, \dots, y_n. \varphi'$
+ \eTD\bTD \currule{} \eTD\eTR
+ \eTD\bTD \eTD\eTR
+\stopAletheS
+
+ \noindent
+ where the variables $y_1, \dots, y_n$ is not free in $\forall x_1,
+ \dots, x_n.\varphi$.
+\stopRuleDescription
+
+\page
+\startRuleDescription{sko_ex}
+The \currule{} rule skolemizes existential quantifiers.
+
+\startAletheS
+\setupTABLE[c][4][width=17em]
+\aletheLineS
+\bTR[bottomframe=on] \bTD[bottomframe=off] $j$.\eTD\bTD[leftframe=on]
+$\Gamma, x_1 \mapsto \varepsilon_1, \dots , x_n \mapsto \varepsilon_n$
+ \eTD\bTD \ctxsep
+ \eTD\bTD
+ $\varphi ≈ \psi$
+ \eTD\bTD (\dots) \eTD\eTR
+\bTR\bTD $k$.\eTD \bTD \eTD
+ \bTD \ctxsep \eTD\bTD
+ $\exists x_1, \dots, x_n.\varphi ≈ \psi$
+ \eTD\bTD \currule{} \eTD\eTR
+ \eTD\bTD \eTD\eTR
+\stopAletheS
+
+\noindent
+where $\varepsilon_i$ stands for $\varepsilon x_i. (\exists x_{i+1}, \dots,
+x_n. \varphi[x_1\mapsto \varepsilon_1,\dots,x_{i-1}\mapsto\varepsilon_{i-1}])$.
+\stopRuleDescription
+
+\startRuleDescription{sko_forall}
+The \currule{} rule skolemizes universal quantifiers.
+
+\startAletheS
+\setupTABLE[c][4][width=11em]
+\aletheLineS
+\bTR[bottomframe=on] \bTD[bottomframe=off] $j$.\eTD\bTD[leftframe=on]
+$\Gamma, x_1 \mapsto (\varepsilon x_1.\neg\varphi), \dots, x_n \mapsto (\varepsilon x_n.\neg\varphi)$
+ \eTD\bTD \ctxsep
+ \eTD\bTD
+ $\varphi ≈ \psi$
+ \eTD\bTD (\dots) \eTD\eTR
+\bTR\bTD $k$.\eTD \bTD \eTD
+ \bTD \ctxsep \eTD\bTD
+$\forall x_1, \dots, x_n.\varphi ≈ \psi$
+ \eTD\bTD \currule{} \eTD\eTR
+ \eTD\bTD \eTD\eTR
+\stopAletheS
+
+\stopRuleDescription
+
+
+\startRuleDescription{forall_inst}
+\startAlethe
+\setupTABLE[c][3][width=18em]
+\setupTABLE[c][4][width=11em,align=flushright]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD
+$\neg (\forall x_1, \dots, x_n. P) \lor P[x_1\mapsto t_1]\dots[x_n\mapsto t_n]$
+\eTD\bTD \currule\, [$(x_{k_1}, t_{k_1})$, \dots, $(x_{k_n}, t_{k_n})$] \eTD\eTR
+\stopAlethe
+
+\noindent
+where $k_1, \dots, k_n$ is a permutation of $1, \dots, n$ and $x_i$ and
+$k_i$ have the same sort. The arguments $(x_{k_i}, t_{k_i})$ are printed as
+\inlineAlethe{(:= xki tki)}.
+
+\tightpara{Remark.} In \in{Section}[sec:qsimp-proof] we discuss an alternative
+quantifier instantiation rule.
+The resulting proof would be more fine grained and this
+would also be an opportunity to provide a proof for the clausification
+as currently done by \proofRule{qnt_cnf}.
+\stopRuleDescription
+
+\startRuleDescription{refl}
+\startAletheS
+\setupTABLE[c][4][width=28em]
+\bTR\bTD $j$.\eTD\bTD \ctxsep \eTD\bTD $\Gamma$ \eTD\bTD
+$t_1 ≈ t_2 $
+\eTD\bTD \currule \eTD\eTR
+\stopAletheS
+
+\noindent
+where, if $\sigma = \subst(\Gamma)$,
+the terms $t_1\sigma$ and $t_2$ are
+syntactically equal up to the orientation of equalities.
+
+\tightpara{Remark.} This is the only rule that requires the application of
+the context.
+\stopRuleDescription
+
+\page
+\startRuleDescription{trans}
+\startAletheS
+\setupTABLE[c][4][width=22em]
+\bTR\bTD $i_1$.\eTD\bTD \ctxsep \eTD\bTD $\Gamma$ \eTD\bTD
+$t_1 ≈ t_2 $
+\eTD\bTD (\dots) \eTD\eTR
+\bTR\bTD $i_2$.\eTD\bTD \ctxsep \eTD\bTD $\Gamma$ \eTD\bTD
+$t_2 ≈ t_3 $
+\eTD\bTD (\dots) \eTD\eTR
+\aletheLineSB
+\bTR\bTD $i_n$.\eTD\bTD \ctxsep \eTD\bTD $\Gamma$ \eTD\bTD
+$t_n ≈ t_{n+1} $
+\eTD\bTD (\dots) \eTD\eTR
+\bTR\bTD $j$.\eTD\bTD \ctxsep \eTD\bTD $\Gamma$ \eTD\bTD
+$t_1 ≈ t_{n+1}$
+\eTD\bTD (\currule\; $i_1$, \dots, $i_n$) \eTD\eTR
+\stopAletheS
+
+\stopRuleDescription
+
+\startRuleDescription{cong}
+\startAletheS
+\setupTABLE[c][4][width=22em]
+\bTR\bTD $i_1$.\eTD\bTD \ctxsep \eTD\bTD $\Gamma$ \eTD\bTD
+$t_1 ≈ u_1 $
+\eTD\bTD (\dots) \eTD\eTR
+\bTR\bTD $i_2$.\eTD\bTD \ctxsep \eTD\bTD $\Gamma$ \eTD\bTD
+$t_2 ≈ u_2 $
+\eTD\bTD (\dots) \eTD\eTR
+\aletheLineSB
+\bTR\bTD $i_n$.\eTD\bTD \ctxsep \eTD\bTD $\Gamma$ \eTD\bTD
+$t_n ≈ u_n $
+\eTD\bTD (\dots) \eTD\eTR
+\bTR\bTD $j$.\eTD\bTD \ctxsep \eTD\bTD $\Gamma$ \eTD\bTD
+$(f\,t_1\,\cdots\,t_n) ≈ (f\,u_1\,\cdots\,u_n)$
+\eTD\bTD (\currule\; $i_1$, \dots, $i_n$) \eTD\eTR
+\stopAletheS
+
+\noindent
+where $f$\, is any $n$-ary function symbol of appropriate sort.
+\stopRuleDescription
+
+\startRuleDescription{eq_reflexive}
+\startAlethe
+\setupTABLE[c][3][width=24.5em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD
+$t ≈ t$
+\eTD\bTD \currule \eTD\eTR
+\stopAlethe
+\stopRuleDescription
+
+\startRuleDescription{eq_transitive}
+\startAlethe
+\setupTABLE[c][3][width=24.5em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD
+$\neg (t_1 ≈ t_2)$, \dots , $\neg (t_{n-1} ≈ t_n)$,
+$t_1 ≈ t_n$
+\eTD\bTD \currule \eTD\eTR
+\stopAlethe
+\stopRuleDescription
+
+\startRuleDescription{eq_congruent}
+\startAlethe
+\setupTABLE[c][3][width=24.5em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD
+$\neg (t_1 ≈ u_1)$, \dots ,$\neg (t_n ≈ u_n)$,
+$(f\,t_1\, \cdots\,t_n) ≈ (f\,u_1\, \cdots\,u_n)$
+\eTD\bTD \currule \eTD\eTR
+\stopAlethe
+\stopRuleDescription
+
+\startRuleDescription{eq_congruent_pred}
+\startAlethe
+\setupTABLE[c][3][width=22em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD
+$\neg (t_1 ≈ u_1)$, \dots ,$\neg (t_n ≈ u_n)$,
+$(P\,t_1\, \cdots\,t_n) ≈ (P\,u_1\, \cdots\,u_n)$
+\eTD\bTD \currule \eTD\eTR
+\stopAlethe
+
+\noindent
+where $P$\, is a function symbol with co-domain sort $\lsymb{Bool}$.
+\stopRuleDescription
+
+\page
+\startRuleDescription{qnt_cnf}
+\startAlethe
+\setupTABLE[c][3][width=27em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD
+$\neg(\forall x_1, \dots, x_n. \varphi) \lor \forall x_{k_1}, \dots, x_{k_m}.\varphi'$
+\eTD\bTD \currule \eTD\eTR
+\stopAlethe
+
+This rule expresses clausification of a term under a universal
+quantifier. This is used by conflicting instantiation. $\varphi'$ is one of the clause
+of the clause normal form of $\varphi$. The variables $x_{k_1}, \dots, x_{k_m}$ are
+a permutation of $x_1, \dots, x_n$ plus additional variables added by prenexing
+$\varphi$. Normalization is performed in two phases. First, the negative normal form
+is formed, then the result is prenexed. The result of the first step is $\Phi(\varphi, 1)$
+where:
+
+\startformula\startalign
+\NC \Phi(\neg \varphi, 1) \NC:= \Phi(\varphi, 0)\NR
+\NC \Phi(\neg \varphi, 0) \NC:= \Phi(\varphi, 1)\NR
+\NC \Phi(\varphi_1 \lor\dots\lor\varphi_n, 1) \NC:= \Phi(\varphi_1, 1)\lor\dots\lor\Phi(\varphi_n, 1)\NR
+\NC \Phi(\varphi_1 \land\dots\land\varphi_n, 1) \NC:= \Phi(\varphi_1, 1)\land\dots\land\Phi(\varphi_n, 1)\NR
+\NC \Phi(\varphi_1 \lor\dots\lor\varphi_n, 0) \NC:= \Phi(\varphi_1, 0)\land\dots\land\Phi(\varphi_n, 0)\NR
+\NC \Phi(\varphi_1 \land\dots\land\varphi_n, 0) \NC:= \Phi(\varphi_1, 0)\lor\dots\lor\Phi(\varphi_n, 0)\NR
+\NC \Phi(\varphi_1 \rightarrow \varphi_2, 1) \NC:= (\Phi(\varphi_1, 0) \lor \Phi(\varphi_2, 1)) \land
+ (\Phi(\varphi_2, 0) \lor \Phi(\varphi_1, 1))\NR
+\NC \Phi(\varphi_1 \rightarrow \varphi_2, 0) \NC:= (\Phi(\varphi_1, 1) \land \Phi(\varphi_2, 0)) \lor
+ (\Phi(\varphi_2, 1) \land \Phi(\varphi_1, 0))\NR
+\NC \Phi(\lsymb{ite}\,\varphi_1\,\varphi_2\,\varphi_3, 1) \NC:=
+ (\Phi(\varphi_1, 0) \lor \Phi(\varphi_2, 1)) \land (\Phi(\varphi_1, 1) \lor \Phi(\varphi_3, 1))\NR
+\NC \Phi(\lsymb{ite}\,\varphi_1\,\varphi_2\,\varphi_3, 0) \NC:=
+ (\Phi(\varphi_1, 1) \land \Phi(\varphi_2, 0)) \lor (\Phi(\varphi_1, 0) \land \Phi(\varphi_3, 0))\NR
+\NC \Phi(\forall x_1, \dots, x_n. \varphi, 1) \NC:= \forall x_1, \dots, x_n. \Phi(\varphi, 1)\NR
+\NC \Phi(\exists x_1, \dots, x_n. \varphi, 1) \NC:= \exists x_1, \dots, x_n. \Phi(\varphi, 1)\NR
+\NC \Phi(\forall x_1, \dots, x_n. \varphi, 0) \NC:= \exists x_1, \dots, x_n. \Phi(\varphi, 0)\NR
+\NC \Phi(\exists x_1, \dots, x_n. \varphi, 0) \NC:= \forall x_1, \dots, x_n. \Phi(\varphi, 0)\NR
+\NC \Phi(\varphi, 1) \NC:= \varphi\NR
+\NC \Phi(\varphi, 0) \NC:= \neg\varphi
+\stopalign\stopformula
+
+\tightpara{Remark.} This is a placeholder rule that combines the many steps
+done during clausification.
+
+\stopRuleDescription
+
+\page
+\startRuleDescription{and}
+\startAlethe
+\setupTABLE[c][3][width=28em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD
+$\varphi_1 \land \cdots \land \varphi_n$
+\eTD\bTD (\dots) \eTD\eTR
+\bTR\bTD $j$.\eTD\bTD \ctxsep \eTD\bTD
+$\varphi_k$
+\eTD\bTD (\currule\;$i$) \eTD\eTR
+\stopAlethe
+
+\noindent
+and $1 \leq k \leq n$.
+\stopRuleDescription
+
+\startRuleDescription{not_or}
+\startAlethe
+\setupTABLE[c][3][width=27em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD
+$\neg (\varphi_1 \lor \cdots \lor \varphi_n)$
+\eTD\bTD (\dots) \eTD\eTR
+\bTR\bTD $j$.\eTD\bTD \ctxsep \eTD\bTD
+$\neg \varphi_k$
+\eTD\bTD (\currule\;$i$) \eTD\eTR
+\stopAlethe
+
+\noindent
+and $1 \leq k \leq n$.
+\stopRuleDescription
+
+\startRuleDescription{or}
+\startAlethe
+\setupTABLE[c][3][width=28em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD
+$\varphi_1 \lor \cdots \lor \varphi_n$
+\eTD\bTD (\dots) \eTD\eTR
+\bTR\bTD $j$.\eTD\bTD \ctxsep \eTD\bTD
+$\varphi_1, \dots, \varphi_n$
+\eTD\bTD (\currule\;$i$) \eTD\eTR
+\stopAlethe
+
+\tightpara{Remark.} This rule deconstructs the \inlineAlethe{or} operator
+into a clause denoted by \inlineAlethe{cl}.
+\stopRuleDescription
+
+\startruleexample
+An application of the \currule{} rule.
+
+\startSMTCode
+(step t15 (cl (or (= a b) (not (<= a b)) (not (<= b a))))
+ :rule la_disequality)
+(step t16 (cl (= a b) (not (<= a b)) (not (<= b a)))
+ :rule or :premises (t15))
+\stopSMTCode
+\stopruleexample
+
+
+\startRuleDescription{not_and}
+\startAlethe
+\setupTABLE[c][3][width=26em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD
+$\neg (\varphi_1 \land \dots \land \varphi_n)$
+\eTD\bTD (\dots) \eTD\eTR
+\bTR\bTD $j$.\eTD\bTD \ctxsep \eTD\bTD
+$\neg\varphi_1 , \dots , \neg\varphi_n$
+\eTD\bTD (\currule\;$i$) \eTD\eTR
+\stopAlethe
+
+\stopRuleDescription
+
+\startRuleDescription{xor1}
+\startAlethe
+\setupTABLE[c][3][width=28em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD
+$\lsymb{xor}\,\varphi_1\,\varphi_2$
+\eTD\bTD (\dots) \eTD\eTR
+\bTR\bTD $j$.\eTD\bTD \ctxsep \eTD\bTD
+$\varphi_1, \varphi_2$
+\eTD\bTD (\currule\;$i$) \eTD\eTR
+\stopAlethe
+\stopRuleDescription
+
+\page
+\startRuleDescription{xor2}
+\startAlethe
+\setupTABLE[c][3][width=28em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD
+$\lsymb{xor}\,\varphi_1\,\varphi_2$
+\eTD\bTD (\dots) \eTD\eTR
+\bTR\bTD $j$.\eTD\bTD \ctxsep \eTD\bTD
+$\neg\varphi_1 , \neg\varphi_2$
+\eTD\bTD (\currule\;$i$) \eTD\eTR
+\stopAlethe
+
+\stopRuleDescription
+
+\startRuleDescription{not_xor1}
+\startAlethe
+\setupTABLE[c][3][width=26em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD
+$\neg(\lsymb{xor}\,\varphi_1\,\varphi_2)$
+\eTD\bTD (\dots) \eTD\eTR
+\bTR\bTD $j$.\eTD\bTD \ctxsep \eTD\bTD
+$\varphi_1 , \neg\varphi_2$
+\eTD\bTD (\currule\;$i$) \eTD\eTR
+\stopAlethe
+
+\noindent
+\stopRuleDescription
+
+\startRuleDescription{not_xor2}
+\startAlethe
+\setupTABLE[c][3][width=26em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD
+$\neg(\lsymb{xor}\,\varphi_1\,\varphi_2)$
+\eTD\bTD (\dots) \eTD\eTR
+\bTR\bTD $j$.\eTD\bTD \ctxsep \eTD\bTD
+$\neg\varphi_1 , \varphi_2$
+\eTD\bTD (\currule\;$i$) \eTD\eTR
+\stopAlethe
+\stopRuleDescription
+
+\startRuleDescription{implies}
+\startAlethe
+\setupTABLE[c][3][width=26em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD
+$\varphi_1\rightarrow\varphi_2$
+\eTD\bTD (\dots) \eTD\eTR
+\bTR\bTD $j$.\eTD\bTD \ctxsep \eTD\bTD
+$\neg\varphi_1 , \varphi_2$
+\eTD\bTD (\currule\;$i$) \eTD\eTR
+\stopAlethe
+\stopRuleDescription
+
+\startRuleDescription{not_implies1}
+\startAlethe
+\setupTABLE[c][3][width=24em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD
+$\neg (\varphi_1\rightarrow\varphi_2)$
+\eTD\bTD (\dots) \eTD\eTR
+\bTR\bTD $j$.\eTD\bTD \ctxsep \eTD\bTD
+$\varphi_1$
+\eTD\bTD (\currule\;$i$) \eTD\eTR
+\stopAlethe
+\stopRuleDescription
+
+\startRuleDescription{not_implies2}
+\startAlethe
+\setupTABLE[c][3][width=24em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD
+$\neg (\varphi_1\rightarrow\varphi_2)$
+\eTD\bTD (\dots) \eTD\eTR
+\bTR\bTD $j$.\eTD\bTD \ctxsep \eTD\bTD
+$\neg\varphi_2$
+\eTD\bTD (\currule\;$i$) \eTD\eTR
+\stopAlethe
+\stopRuleDescription
+
+\startRuleDescription{equiv1}
+\startAlethe
+\setupTABLE[c][3][width=25em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD
+$\varphi_1≈\varphi_2$
+\eTD\bTD (\dots) \eTD\eTR
+\bTR\bTD $j$.\eTD\bTD \ctxsep \eTD\bTD
+$\neg\varphi_1 , \varphi_2$
+\eTD\bTD (\currule\;$i$) \eTD\eTR
+\stopAlethe
+\stopRuleDescription
+
+\page
+\startRuleDescription{equiv2}
+\startAlethe
+\setupTABLE[c][3][width=25em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD
+$\varphi_1≈\varphi_2$
+\eTD\bTD (\dots) \eTD\eTR
+\bTR\bTD $j$.\eTD\bTD \ctxsep \eTD\bTD
+$\varphi_1, \neg\varphi_2$
+\eTD\bTD (\currule\;$i$) \eTD\eTR
+\stopAlethe
+\stopRuleDescription
+
+\startRuleDescription{not_equiv1}
+\startAlethe
+\setupTABLE[c][3][width=25em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD
+$\neg(\varphi_1≈\varphi_2)$
+\eTD\bTD (\dots) \eTD\eTR
+\bTR\bTD $j$.\eTD\bTD \ctxsep \eTD\bTD
+$\varphi_1 , \varphi_2$
+\eTD\bTD (\currule\;$i$) \eTD\eTR
+\stopAlethe
+\stopRuleDescription
+
+
+\startRuleDescription{not_equiv2}
+\startAlethe
+\setupTABLE[c][3][width=25em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD
+$\neg(\varphi_1≈\varphi_2)$
+\eTD\bTD (\dots) \eTD\eTR
+\bTR\bTD $j$.\eTD\bTD \ctxsep \eTD\bTD
+$\neg\varphi_1 , \neg\varphi_2$
+\eTD\bTD (\currule\;$i$) \eTD\eTR
+\stopAlethe
+\stopRuleDescription
+
+\startRuleDescription{and_pos}
+\startAlethe
+\setupTABLE[c][3][width=26em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD
+$\neg (\varphi_1 \land \cdots \land \varphi_n) , \varphi_k$
+\eTD\bTD \currule \eTD\eTR
+\stopAlethe
+
+\noindent
+with $1 \leq k \leq n$.
+\stopRuleDescription
+
+\startRuleDescription{and_neg}
+\startAlethe
+\setupTABLE[c][3][width=26em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD
+$(\varphi_1 \land \cdots \land \varphi_n), \neg\varphi_1, \dots , \neg\varphi_n$
+\eTD\bTD \currule \eTD\eTR
+\stopAlethe
+
+\stopRuleDescription
+
+\startRuleDescription{or_pos}
+\startAlethe
+\setupTABLE[c][3][width=26.5em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD
+$\neg (\varphi_1 \lor \cdots \lor \varphi_n) , \varphi_1 , \dots, \varphi_n $
+\eTD\bTD \currule \eTD\eTR
+\stopAlethe
+\stopRuleDescription
+
+\startRuleDescription{or_neg}
+\startAlethe
+\setupTABLE[c][3][width=26.5em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD
+$(\varphi_1 \lor \cdots \lor \varphi_n) , \neg \varphi_k$
+\eTD\bTD \currule \eTD\eTR
+\stopAlethe
+
+\noindent
+with $1 \leq k \leq n$.
+\stopRuleDescription
+
+\startRuleDescription{xor_pos1}
+\startAlethe
+\setupTABLE[c][3][width=26.5em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD
+$\neg (\varphi_1\,\lsymb{xor}\,\varphi_2) , \varphi_1 , \varphi_2$
+\eTD\bTD \currule \eTD\eTR
+\stopAlethe
+\stopRuleDescription
+
+\page
+\startRuleDescription{xor_pos2}
+\startAlethe
+\setupTABLE[c][3][width=26.5em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD
+$\neg (\varphi_1\,\lsymb{xor}\,\varphi_2), \neg \varphi_1, \neg \varphi_2$
+\eTD\bTD \currule \eTD\eTR
+\stopAlethe
+\stopRuleDescription
+
+\startRuleDescription{xor_neg1}
+\startAlethe
+\setupTABLE[c][3][width=26.5em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD
+$\varphi_1 \,\lsymb{xor}\, \varphi_2, \varphi_1 , \neg \varphi_2$
+\eTD\bTD \currule \eTD\eTR
+\stopAlethe
+\stopRuleDescription
+
+\startRuleDescription{xor_neg2}
+\startAlethe
+\setupTABLE[c][3][width=26.5em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD
+$\varphi_1\,\lsymb{xor}\,\varphi_2, \neg \varphi_1 , \varphi_2$
+\eTD\bTD \currule \eTD\eTR
+\stopAlethe
+\stopRuleDescription
+
+\startRuleDescription{implies_pos}
+\startAlethe
+\setupTABLE[c][3][width=25.5em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD
+$\neg (\varphi_1 \rightarrow \varphi_2), \neg \varphi_1 , \varphi_2$
+\eTD\bTD \currule \eTD\eTR
+\stopAlethe
+\stopRuleDescription
+
+\startRuleDescription{implies_neg1}
+\startAlethe
+\setupTABLE[c][3][width=25em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD
+$\varphi_1 \rightarrow \varphi_2, \varphi_1$
+\eTD\bTD \currule \eTD\eTR
+\stopAlethe
+\stopRuleDescription
+
+\startRuleDescription{implies_neg2}
+\startAlethe
+\setupTABLE[c][3][width=25em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD
+$\varphi_1 \rightarrow \varphi_2, \neg \varphi_2$
+\eTD\bTD \currule \eTD\eTR
+\stopAlethe
+\stopRuleDescription
+
+\startRuleDescription{equiv_pos1}
+\startAlethe
+\setupTABLE[c][3][width=25.5em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD
+$\neg (\varphi_1 ≈ \varphi_2) , \varphi_1 , \neg \varphi_2$
+\eTD\bTD \currule \eTD\eTR
+\stopAlethe
+\stopRuleDescription
+
+\startRuleDescription{equiv_pos2}
+\startAlethe
+\setupTABLE[c][3][width=25.5em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD
+$\neg (\varphi_1 ≈ \varphi_2) , \neg \varphi_1 , \varphi_2$
+\eTD\bTD \currule \eTD\eTR
+\stopAlethe
+\stopRuleDescription
+
+\startRuleDescription{equiv_neg1}
+\startAlethe
+\setupTABLE[c][3][width=25.5em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD
+$\varphi_1 ≈ \varphi_2 , \neg \varphi_1 , \neg \varphi_2$
+\eTD\bTD \currule \eTD\eTR
+\stopAlethe
+\stopRuleDescription
+
+\startRuleDescription{equiv_neg2}
+\startAlethe
+\setupTABLE[c][3][width=25.5em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD
+$\varphi_1 ≈ \varphi_2 , \varphi_1 , \varphi_2$
+\eTD\bTD \currule \eTD\eTR
+\stopAlethe
+\stopRuleDescription
+
+\startRuleDescription{ite1}
+\startAlethe
+\setupTABLE[c][3][width=26em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD
+$\lsymb{ite}\,\varphi_1\,\varphi_2\,\varphi_3$
+\eTD\bTD (\dots) \eTD\eTR
+\bTR\bTD $j$.\eTD\bTD \ctxsep \eTD\bTD
+$\varphi_1 , \varphi_3$
+\eTD\bTD (\currule\;$i$) \eTD\eTR
+\stopAlethe
+\stopRuleDescription
+
+\startRuleDescription{ite2}
+\startAlethe
+\setupTABLE[c][3][width=26em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD
+$\lsymb{ite}\,\varphi_1\,\varphi_2\,\varphi_3$
+\eTD\bTD (\dots) \eTD\eTR
+\bTR\bTD $j$.\eTD\bTD \ctxsep \eTD\bTD
+$\neg\varphi_1 , \varphi_2$
+\eTD\bTD (\currule\;$i$) \eTD\eTR
+\stopAlethe
+\stopRuleDescription
+
+\startRuleDescription{ite_pos1}
+\startAlethe
+\setupTABLE[c][3][width=26em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD
+ $\neg (\lsymb{ite}\,\varphi_1\,\varphi_2\,\varphi_3) , \varphi_1 , \varphi_3$
+\eTD\bTD (\currule) \eTD\eTR
+\stopAlethe
+\stopRuleDescription
+
+\startRuleDescription{ite_pos2}
+\startAlethe
+\setupTABLE[c][3][width=26em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD
+ $\neg (\lsymb{ite}\,\varphi_1\,\varphi_2\,\varphi_3) , \neg \varphi_1 , \varphi_2$
+\eTD\bTD (\currule) \eTD\eTR
+\stopAlethe
+\stopRuleDescription
+
+\startRuleDescription{ite_neg1}
+\startAlethe
+\setupTABLE[c][3][width=26em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD
+ $\lsymb{ite}\,\varphi_1\,\varphi_2\,\varphi_3 , \varphi_1 , \neg \varphi_3$
+\eTD\bTD (\currule) \eTD\eTR
+\stopAlethe
+\stopRuleDescription
+
+\startRuleDescription{ite_neg2}
+\startAlethe
+\setupTABLE[c][3][width=26em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD
+ $\lsymb{ite}\,\varphi_1\,\varphi_2\,\varphi_3 , \neg \varphi_1 , \neg \varphi_2$
+\eTD\bTD (\currule) \eTD\eTR
+\stopAlethe
+\stopRuleDescription
+
+\startRuleDescription{not_ite1}
+\startAlethe
+\setupTABLE[c][3][width=26em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD
+$\neg(\lsymb{ite}\,\varphi_1\,\varphi_2\,\varphi_3)$
+\eTD\bTD (\dots) \eTD\eTR
+\bTR\bTD $j$.\eTD\bTD \ctxsep \eTD\bTD
+$\varphi_1 , \neg\varphi_3$
+\eTD\bTD (\currule\;$i$) \eTD\eTR
+\stopAlethe
+\stopRuleDescription
+
+\startRuleDescription{not_ite2}
+\startAlethe
+\setupTABLE[c][3][width=26em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD
+$\neg(\lsymb{ite}\,\varphi_1\,\varphi_2\,\varphi_3)$
+\eTD\bTD (\dots) \eTD\eTR
+\bTR\bTD $j$.\eTD\bTD \ctxsep \eTD\bTD
+$\neg\varphi_1 , \neg\varphi_2$
+\eTD\bTD (\currule\;$i$) \eTD\eTR
+\stopAlethe
+
+\stopRuleDescription
+
+\page
+\startRuleDescription{connective_def}
+ This rule is used to replace connectives by their definition. It can be one
+ of the following:
+
+\startAletheS
+\setupTABLE[c][4][width=23em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD $\Gamma$ \eTD\bTD
+ $\varphi_1\,\lsymb{xor}\,\varphi_2 ≈
+ (\neg\varphi_1 \land \varphi_2) \lor (\varphi_1 \land \neg\varphi_2)$
+\eTD\bTD \currule \eTD\eTR
+\stopAletheS
+
+\startAletheS
+\setupTABLE[c][4][width=23em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD $\Gamma$ \eTD\bTD
+ $\varphi_1≈\varphi_2 ≈
+ (\varphi_1 \rightarrow \varphi_2) \land (\varphi_2 \rightarrow \varphi_1)$
+\eTD\bTD \currule \eTD\eTR
+\stopAletheS
+
+\startAletheS
+\setupTABLE[c][4][width=23em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD $\Gamma$ \eTD\bTD
+ $\lsymb{ite}\,\varphi_1\,\varphi_2\,\varphi_3 ≈
+ (\varphi_1 \rightarrow \varphi_2) \land (\neg\varphi_1 \rightarrow \varphi_3)$
+\eTD\bTD \currule \eTD\eTR
+\stopAletheS
+
+\startAletheS
+\setupTABLE[c][4][width=23em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD $\Gamma$ \eTD\bTD
+ $\forall x_1, \dots, x_n.\,\varphi ≈ \neg(\exists x_1, \dots, x_n.\,
+ \neg\varphi)$
+\eTD\bTD \currule \eTD\eTR
+\stopAletheS
+
+\stopRuleDescription
+
+
+\startRuleDescription{and_simplify}
+This rule simplifies an $\land$ term by applying equivalent
+transformations as long as possible. Hence, the general form is
+
+\startAletheS
+\setupTABLE[c][4][width=23em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD $\Gamma$ \eTD\bTD
+$\varphi_1\land \cdots\land\varphi_n ≈ \psi$
+\eTD\bTD \currule \eTD\eTR
+\stopAletheS
+
+\noindent
+where $\psi$ is the transformed term.
+
+The possible transformations are:
+\startitemize[packed]
+ \item $\top \land \cdots \land \top ⇒ \top$
+ \item $\varphi_1 \land \cdots \land \varphi_n ⇒ \varphi_1
+ \land \cdots \land \varphi_{n'} $ where the right-hand side has all
+ $\top$ literals removed.
+ \item $\varphi_1 \land \cdots \land \varphi_n ⇒ \varphi_1
+ \land \cdots \land \varphi_{n'} $ where the right-hand side has all
+ repeated literals removed.
+ \item $\varphi_1 \land\cdots\land \bot\land\cdots \land \varphi_n ⇒ \bot$
+ \item $\varphi_1 \land\cdots\land \varphi_i\land \cdots \land \varphi_j\land\cdots \land \varphi_n ⇒ \bot$
+ and $\varphi_i$, $\varphi_j$ are such that
+ \startformula\startalign
+ \NC \varphi_i \NC= \underbrace{\neg \dots \neg}_n \psi \NR
+ \NC \varphi_j \NC= \underbrace{\neg \dots \neg}_m \psi
+ \stopalign\stopformula
+ and one of $n, m$ is odd and the other even. Either can be $0$.
+\stopitemize
+\stopRuleDescription
+
+\startRuleDescription{or_simplify}
+This rule simplifies an $\lor$ term by applying equivalent
+transformations as long as possible. Hence, the general form is
+
+\startAletheS
+\setupTABLE[c][4][width=23em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD $\Gamma$ \eTD\bTD
+$(\varphi_1\lor \cdots\lor\varphi_n) ≈ \psi$
+\eTD\bTD \currule \eTD\eTR
+\stopAletheS
+
+\noindent
+where $\psi$ is the transformed term.
+
+The possible transformations are:
+\startitemize[packed]
+ \item $\bot \lor \cdots \lor \bot ⇒ \bot$
+ \item $\varphi_1 \lor \cdots \lor \varphi_n ⇒ \varphi_1
+ \lor \cdots \lor \varphi_{n'} $ where the right-hand side has all
+ $\bot$ literals removed.
+ \item $\varphi_1 \lor \cdots \lor \varphi_n ⇒ \varphi_1
+ \lor \cdots \lor \varphi_{n'} $ where the right-hand side has all
+ repeated literals removed.
+ \item $\varphi_1 \lor\cdots\lor \top\lor\cdots \lor \varphi_n ⇒ \top$
+ \item $\varphi_1 \lor\cdots\lor \varphi_i\lor \cdots \lor \varphi_j\lor\cdots \lor \varphi_n ⇒ \top$
+ and $\varphi_i$, $\varphi_j$ are such that
+ \startformula\startalign
+ \NC \varphi_i \NC= \underbrace{\neg \dots \neg}_n \psi \NR
+ \NC \varphi_j \NC= \underbrace{\neg \dots \neg}_m \psi
+ \stopalign\stopformula
+ and one of $n, m$ is odd and the other even. Either can be $0$.
+\stopitemize
+\stopRuleDescription
+
+\startRuleDescription{not_simplify}
+This rule simplifies an $\neg$ term by applying equivalent
+transformations as long as possible. Hence, the general form is
+
+\startAletheS
+\setupTABLE[c][4][width=23em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD $\Gamma$ \eTD\bTD
+$\neg\varphi ≈ \psi$
+\eTD\bTD \currule \eTD\eTR
+\stopAletheS
+
+\noindent
+where $\psi$ is the transformed term.
+
+The possible transformations are:
+\startitemize[packed]
+ \item $\neg (\neg \varphi) ⇒ \varphi$
+ \item $\neg \bot ⇒ \top$
+ \item $\neg \top ⇒ \bot$
+\stopitemize
+\stopRuleDescription
+
+\startRuleDescription{implies_simplify}
+This rule simplifies an $\rightarrow$ term by applying equivalent
+transformations as long as possible. Hence, the general form is
+
+\startAletheS
+\setupTABLE[c][4][width=23em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD $\Gamma$ \eTD\bTD
+$\varphi_1\rightarrow \varphi_2 ≈ \psi$
+\eTD\bTD \currule \eTD\eTR
+\stopAletheS
+
+\noindent
+where $\psi$ is the transformed term.
+
+The possible transformations are:
+\startitemize[packed]
+ \item $\neg \varphi_1 \rightarrow \neg \varphi_2 ⇒ \varphi_2\rightarrow \varphi_1$
+ \item $\bot \rightarrow \varphi ⇒ \top$
+ \item $ \varphi \rightarrow \top ⇒ \top$
+ \item $\top \rightarrow \varphi ⇒ \varphi$
+ \item $ \varphi \rightarrow \bot ⇒ \neg \varphi$
+ \item $ \varphi \rightarrow \varphi ⇒ \top$
+ \item $\neg \varphi \rightarrow \varphi ⇒ \varphi$
+ \item $ \varphi \rightarrow \neg \varphi ⇒ \neg \varphi$
+ \item $( \varphi_1\rightarrow \varphi_2)\rightarrow \varphi_2 ⇒ \varphi_1\lor \varphi_2$
+\stopitemize
+\stopRuleDescription
+
+\startRuleDescription{equiv_simplify}
+This rule simplifies a formula with the head symbol $≈\,: \lsymb{Bool}\,\lsymb{Bool}\,\lsymb{Bool}$
+by applying equivalent
+transformations as long as possible. Hence, the general form is
+
+\startAletheS
+\setupTABLE[c][4][width=23em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD $\Gamma$ \eTD\bTD
+$(\varphi_1≈ \varphi_2) ≈ \psi$
+\eTD\bTD \currule \eTD\eTR
+\stopAletheS
+
+\noindent
+where $\psi$ is the transformed term.
+
+The possible transformations are:
+\startitemize[packed]
+ \item $(\neg \varphi_1 ≈ \neg \varphi_2) ⇒ ( \varphi_1≈ \varphi_2)$
+ \item $( \varphi≈ \varphi) ⇒ \top$
+ \item $( \varphi≈ \neg \varphi) ⇒ \bot$
+ \item $(\neg \varphi≈ \varphi) ⇒ \bot$
+ \item $(\top ≈ \varphi) ⇒ \varphi$
+ \item $( \varphi ≈ \top) ⇒ \varphi$
+ \item $(\bot ≈ \varphi) ⇒ \neg \varphi$
+ \item $( \varphi ≈ \bot) ⇒ \neg \varphi$
+\stopitemize
+\stopRuleDescription
+
+\startRuleDescription{bool_simplify}
+This rule simplifies a boolean term by applying equivalent
+transformations as long as possible. Hence, the general form is
+
+\startAletheS
+\setupTABLE[c][4][width=23em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD $\Gamma$ \eTD\bTD
+$\varphi≈ \psi$
+\eTD\bTD \currule \eTD\eTR
+\stopAletheS
+
+\noindent
+where $\psi$ is the transformed term.
+
+The possible transformations are:
+\startitemize[packed]
+ \item $\neg(\varphi_1\rightarrow \varphi_2) ⇒ (\varphi_1 \land \neg \varphi_2)$
+ \item $\neg(\varphi_1\lor \varphi_2) ⇒ (\neg \varphi_1 \land \neg \varphi_2)$
+ \item $\neg(\varphi_1\land \varphi_2) ⇒ (\neg \varphi_1 \lor \neg \varphi_2)$
+ \item $(\varphi_1 \rightarrow (\varphi_2\rightarrow \varphi_3)) ⇒ (\varphi_1\land \varphi_2) \rightarrow \varphi_3$
+ \item $((\varphi_1\rightarrow \varphi_2)\rightarrow \varphi_2) ⇒ (\varphi_1\lor \varphi_2)$
+ \item $(\varphi_1 \land (\varphi_1\rightarrow \varphi_2)) ⇒ (\varphi_1 \land \varphi_2)$
+ \item $((\varphi_1\rightarrow \varphi_2) \land \varphi_1) ⇒ (\varphi_1 \land \varphi_2)$
+\stopitemize
+\stopRuleDescription
+
+\page
+\startRuleDescription{ac_simp}
+ This rule simplifies nested occurrences of $\lor$ or $\land$:
+
+\startAletheS
+\setupTABLE[c][4][width=23em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD $\Gamma$ \eTD\bTD
+ $\psi ≈ \varphi_1 \circ\cdots\circ\varphi_n$
+\eTD\bTD \currule \eTD\eTR
+\stopAletheS
+
+\noindent
+ where $\circ \in \{\lor, \land\}$ and $\psi$ is a nested application of $\circ$.
+ The literals $\varphi_i$ are literals of the flattening of $\psi$ with duplicates
+ removed.
+\stopRuleDescription
+
+\startRuleDescription{ite_simplify}
+ This rule simplifies an if-then-else term by applying equivalent
+ transformations until fix point\footnote{Note however that the order of the
+ application is important, since the set of rules is not confluent. For
+ example, the term $(\lsymb{ite} \top \; t_1 \; t_2 ≈
+ t_1)$ can be simplified into both $p$ and $(\neg (\neg p))$ depending on the
+ order of applications.}
+ %
+It has the form
+\startAletheS
+\setupTABLE[c][4][width=23em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD $\Gamma$ \eTD\bTD
+$\lsymb{ite}\,\varphi\,t_1\,t_2 ≈ u$
+\eTD\bTD \currule \eTD\eTR
+\stopAletheS
+
+\noindent
+where $u$ is the transformed term.
+
+The possible transformations are:
+\startitemize[packed]
+ \item $\lsymb{ite}\, \top \, t_1 \, t_2 ⇒ t_1$
+ \item $\lsymb{ite}\, \bot \, t_1 \, t_2 ⇒ t_2$
+ \item $\lsymb{ite}\, \psi \, t \, t ⇒ t$
+ \item $\lsymb{ite}\, \neg \varphi \, t_1 \, t_2 ⇒ \lsymb{ite}\, \varphi \, t_2 \, t_1$
+ \item $\lsymb{ite}\, \psi \, (\lsymb{ite}\, \psi\,t_1\,t_2)\, t_3 ⇒
+ \lsymb{ite}\, \psi\, t_1\, t_3$
+ \item $\lsymb{ite}\, \psi \, t_1\, (\lsymb{ite}\, \psi\,t_2\,t_3) ⇒
+ \lsymb{ite}\, \psi\, t_1\, t_3$
+ \item $\lsymb{ite}\, \psi \, \top\, \bot ⇒ \psi$
+ \item $\lsymb{ite}\, \psi \, \bot\, \top ⇒ \neg\psi$
+ \item $\lsymb{ite}\, \psi \, \top \, \varphi ⇒ \psi\lor\varphi$
+ \item $\lsymb{ite}\, \psi \, \varphi\,\bot ⇒ \psi\land\varphi$
+ \item $\lsymb{ite}\, \psi \, \bot\, \varphi ⇒ \neg\psi\land\varphi$
+ \item $\lsymb{ite}\, \psi \, \varphi\,\top ⇒ \neg\psi\lor\varphi$
+\stopitemize
+\stopRuleDescription
+
+\startRuleDescription{qnt_simplify}
+ This rule simplifies a $\forall$-formula with a constant predicate.
+
+\startAletheS
+\setupTABLE[c][4][width=23em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD $\Gamma$ \eTD\bTD
+ $\forall x_1, \dots, x_n. \varphi ≈ \varphi$
+\eTD\bTD \currule \eTD\eTR
+\stopAletheS
+
+\noindent
+ where $\varphi$ is either $\top$ or $\bot$.
+\stopRuleDescription
+
+\page
+\startRuleDescription{onepoint}
+The {\currule} rule is the \quotation{one-point-rule}. That is: it eliminates quantified
+variables that can only have one value.
+
+\startAletheS
+\setupTABLE[c][4][width=10em]
+\aletheLineS
+\bTR[bottomframe=on] \bTD[bottomframe=off] $j$.\eTD\bTD[leftframe=on]
+ $\Gamma, x_{k_1},\dots, x_{k_m}, x_{j_1} \mapsto t_{j_1}, \dots , x_{j_o} \mapsto t_{j_o}$
+ \eTD\bTD \ctxsep
+ \eTD\bTD
+ $\varphi ≈ \varphi'$
+ \eTD\bTD (\dots) \eTD\eTR
+\bTR\bTD $k$.\eTD \bTD \eTD
+ \bTD \ctxsep \eTD\bTD
+$Q x_1, \dots, x_n.\varphi ≈ Q x_{k_1}, \dots, x_{k_m}. \varphi'$
+ \eTD\bTD \currule{} \eTD\eTR
+ \eTD\bTD \eTD\eTR
+\stopAletheS
+
+\noindent
+where $Q\in\{\forall, \exists\}$, $n = m + o$, $k_1, \dots, k_m$ and
+$j_1, \dots, j_o$ are monotone
+mappings to $1, \dots, n$, and no $x_{k_i}$ appears in $x_{j_1}, \dots, x_{j_o}$.
+
+The terms $t_{j_1}, \dots, t_{j_o}$ are the points of the variables
+$x_{j_1}, \dots, x_{j_o}$. Points are defined by equalities $x_i≈ t_i$
+with positive polarity in the term $\varphi$.
+
+\tightpara{Remark.} Since an eliminated variable $x_i$ might appear free in a
+term $t_j$, it is necessary to replace $x_i$ with $t_i$ inside $t_j$. While
+this substitution is performed correctly, the proof for it is currently
+missing.
+
+\stopRuleDescription
+
+\startruleexample
+An application of the \currule{} rule on the term $(\forall x, y.\, x ≈ y
+\rightarrow (f\,x)\land (f\,y))$ look like this:
+
+\startSMTCode
+(anchor :step t3 :args ((:= y x)))
+(step t3.t1 (cl (= x y)) :rule refl)
+(step t3.t2 (cl (= (= x y) (= x x)))
+ :rule cong :premises (t3.t1))
+(step t3.t3 (cl (= x y)) :rule refl)
+(step t3.t4 (cl (= (f y) (f x)))
+ :rule cong :premises (t3.t3))
+(step t3.t5 (cl (= (and (f x) (f y)) (and (f x) (f x))))
+ :rule cong :premises (t3.t4))
+(step t3.t6 (cl (= (=> (= x y) (and (f x) (f y)))
+ (=> (= x x) (and (f x) (f x)))))
+ :rule cong :premises (t3.t2 t3.t5))
+(step t3 (cl (=
+ (forall ((x S) (y S)) (=> (= x y) (and (f x) (f y))))
+ (forall ((x S)) (=> (= x x) (and (f x) (f x))))))
+ :rule qnt_simplify)
+\stopSMTCode
+\stopruleexample
+
+\page
+\startRuleDescription{qnt_join}
+\startAletheS
+\setupTABLE[c][4][width=26em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD $\Gamma$ \eTD\bTD
+ $Q x_1, \dots, x_n.\,(Q x_{n+1}, \dots, x_{m}.\,\varphi)
+ ≈
+ Q x_{k_1}, \dots, x_{k_o}.\,\varphi$
+\eTD\bTD \currule \eTD\eTR
+\stopAletheS
+
+\noindent
+ where $m > n$ and $Q\in\{\forall, \exists\}$. Furthermore, $k_1, \dots, k_o$ is a monotonic
+ map to $1, \dots, m$ such that $x_{k_1}, \dots, x_{k_o}$ are pairwise
+ distinct, and $\{x_1, \dots, x_m\} = \{x_{k_1}, \dots, x_{k_o}\}$.
+\stopRuleDescription
+
+\startRuleDescription{qnt_rm_unused}
+\startAletheS
+\setupTABLE[c][4][width=23em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD $\Gamma$ \eTD\bTD
+ $Q x_1, \dots, x_n.\,\varphi ≈ Q x_{k_1}, \dots, x_{k_m}.\,\varphi$
+\eTD\bTD \currule \eTD\eTR
+\stopAletheS
+
+ \noindent
+ where $m \leq n$ and $Q\in\{\forall, \exists\}$. Furthermore, $k_1, \dots, k_m$ is
+ a monotonic map to $1, \dots, n$ and if $x\in \{x_j\; |\; j \in \{1, \dots,
+ n\} \land j\in\not \{k_1, \dots, k_m\}\}$ then $x$ is not free in $P$.
+
+\stopRuleDescription
+
+\startRuleDescription{eq_simplify}
+ This rule simplifies an $≈$ term by applying equivalent
+ transformations as long as possible. Hence, the general form is
+
+\startAletheS
+\setupTABLE[c][4][width=25em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD $\Gamma$ \eTD\bTD
+ $(t_1≈ t_2) ≈ \varphi$
+\eTD\bTD \currule \eTD\eTR
+\stopAletheS
+
+\noindent
+ where $\psi$ is the transformed term.
+
+ The possible transformations are:
+ \startitemize[packed]
+ \item $t ≈ t ⇒ \top$
+ \item $(t_1 ≈ t_2) ⇒ \bot$ if $t_1$ and $t_2$ are different numeric constants.
+ \item $\neg (t ≈ t) ⇒ \bot$ if $t$ is a numeric constant.
+ \stopitemize
+\stopRuleDescription
+
+\startRuleDescription{div_simplify}
+This rule simplifies a division by applying equivalent
+transformations. The general form is
+
+\startAletheS
+\setupTABLE[c][4][width=25em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD $\Gamma$ \eTD\bTD
+$(t_1\, /\, t_2) ⇒ t_3$
+\eTD\bTD \currule \eTD\eTR
+\stopAletheS
+
+\noindent The possible transformations are:
+\startitemize[packed]
+ \item $t\, /\, t ⇒ 1$
+ \item $t\, /\, 1 ⇒ t$
+ \item $t_1\, /\, t_2 ⇒ t_3$
+ if $t_1$ and $t_2$ are constants and $t_3$ is $t_1$
+ divided by $t_2$ according to the semantic of the current theory.
+\stopitemize
+\stopRuleDescription
+
+\page
+\startRuleDescription{prod_simplify}
+This rule simplifies a product by applying equivalent
+transformations as long as possible. The general form is
+
+\startAletheS
+\setupTABLE[c][4][width=25em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD $\Gamma$ \eTD\bTD
+$t_1\times\cdots\times t_n ≈ u$
+\eTD\bTD \currule \eTD\eTR
+\stopAletheS
+
+\noindent
+where $u$ is either a constant or a product.
+
+The possible transformations are:
+\startitemize[packed]
+ \item $t_1\times\cdots\times t_n ⇒ u$ where all
+ $t_i$ are constants and $u$ is their product.
+ \item $t_1\times\cdots\times t_n ⇒ 0$ if any
+ $t_i$ is $0$.
+ \item $t_1\times\cdots\times t_n ⇒
+ c \times t_{k_1}\times\cdots\times t_{k_n}$ where $c$
+ is the product of the constants of $t_1, \dots, t_n$ and
+ $t_{k_1}, \dots, t_{k_n}$ is $t_1, \dots, t_n$
+ with the constants removed.
+ \item $t_1\times\cdots\times t_n ⇒
+ t_{k_1}\times\cdots\times t_{k_n}$: same as above if $c$ is $1$.
+\stopitemize
+\stopRuleDescription
+
+\startRuleDescription{unary_minus_simplify}
+This rule is either
+
+\startAletheS
+\setupTABLE[c][4][width=20em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD $\Gamma$ \eTD\bTD
+$- (-t) ≈ t$
+\eTD\bTD \currule \eTD\eTR
+\stopAletheS
+
+\noindent
+or
+\startAletheS
+\setupTABLE[c][4][width=20em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD $\Gamma$ \eTD\bTD
+$-t ≈ u$
+\eTD\bTD \currule \eTD\eTR
+\stopAletheS
+
+\noindent
+where $u$ is the negated numerical constant $t$.
+\stopRuleDescription
+
+
+\startRuleDescription{minus_simplify}
+This rule simplifies a subtraction by applying equivalent
+transformations. The general form is
+
+\startAletheS
+\setupTABLE[c][4][width=22em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD $\Gamma$ \eTD\bTD
+$t_1- t_2 ≈ u$
+\eTD\bTD \currule \eTD\eTR
+\stopAletheS
+
+\noindent The possible transformations are:
+\startitemize[packed]
+ \item $t - t ⇒ 0$
+ \item $t_1 - t_2 ⇒ t_3$ where $t_1$
+ and $t_2$ are numerical constants and $t_3$ is $t_2$ subtracted
+ from~$t_1$.
+ \item $t - 0 ⇒ t$
+ \item $0 - t ⇒ -t$
+\stopitemize
+\stopRuleDescription
+
+\startRuleDescription{sum_simplify}
+This rule simplifies a sum by applying equivalent
+transformations as long as possible. The general form is
+
+\startAletheS
+\setupTABLE[c][4][width=22em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD $\Gamma$ \eTD\bTD
+$t_1+\cdots+t_n ≈ u$
+\eTD\bTD \currule \eTD\eTR
+\stopAletheS
+
+\noindent
+where $u$ is either a constant or a product.
+
+The possible transformations are:
+\startitemize[packed]
+ \item $t_1+\cdots+t_n ⇒ c$ where all
+ $t_i$ are constants and $c$ is their sum.
+ \item $t_1+\cdots+t_n ⇒
+ c + t_{k_1}+\cdots+t_{k_n}$ where $c$
+ is the sum of the constants of $t_1, \dots, t_n$ and
+ $t_{k_1}, \dots, t_{k_n}$ is $t_1, \dots, t_n$
+ with the constants removed.
+ \item $t_1+\cdots+t_n ⇒
+ t_{k_1}+\cdots+t_{k_n}$: same as above if $c$ is
+ $0$.
+\stopitemize
+\stopRuleDescription
+
+
+\startRuleDescription{comp_simplify}
+This rule simplifies a comparison by applying equivalent
+transformations as long as possible. The general form is
+
+\startAletheS
+\setupTABLE[c][4][width=22em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD $\Gamma$ \eTD\bTD
+$t_1 \bowtie t_n ≈ \psi$
+\eTD\bTD \currule \eTD\eTR
+\stopAletheS
+
+\noindent
+where $\bowtie$ is as for the proof rule \proofRule{la_generic}, but never
+$≈$.
+
+The possible transformations are:
+\startitemize[packed]
+ \item $t_1 < t_2 ⇒ \varphi$ where $t_1$ and
+ $t_2$ are numerical constants and $\varphi$ is $\top$ if $t_1$ is
+ strictly greater than $t_2$ and $\bot$ otherwise.
+ \item $t < t ⇒ \bot$
+ \item $t_1 \leq t_2 ⇒ \varphi$ where $t_1$ and
+ $t_2$ are numerical constants and $\varphi$ is $\top$ if $t_1$ is
+ greater than $t_2$ or equal and $\bot$ otherwise.
+ \item $t \leq t ⇒ \top$
+ \item $t_1 \geq t_2 ⇒ t_2 \leq t_1$
+ \item $t_1 < t_2 ⇒ \neg (t_2 \leq t_1)$
+ \item $t_1 > t_2 ⇒ \neg (t_1 \leq t_2)$
+\stopitemize
+\stopRuleDescription
+
+\startRuleDescription{let}
+ This rule eliminates $\lsymb{let}$. It has the form
+
+\startAletheS
+\setupTABLE[c][4][width=14.5em]
+\bTR \bTD $i_1$.\eTD\bTD
+ $\Gamma$
+ \eTD\bTD \ctxsep \eTD\bTD
+ $t_{1} ≈ s_{1}$
+ \eTD\bTD (\dots) \eTD\eTR
+\aletheLineSB
+\bTR \bTD $i_n$.\eTD\bTD
+ $\Gamma$
+ \eTD\bTD \ctxsep \eTD\bTD
+ $t_{n} ≈ s_{n}$
+ \eTD\bTD (\dots) \eTD\eTR
+\aletheLineS
+\bTR[bottomframe=on] \bTD[bottomframe=off] $j$.\eTD\bTD[leftframe=on]
+ $\Gamma, x_1 \mapsto s_1, \dots, x_n \mapsto s_n$
+ \eTD\bTD \ctxsep
+ \eTD\bTD
+ $u ≈ u'$
+ \eTD\bTD (\dots) \eTD\eTR
+\bTR\bTD $k$.\eTD \bTD $\Gamma$ \eTD
+ \bTD \ctxsep \eTD\bTD
+ $(\lsymb{let}\,x_1 = t_1,\, \dots,\, x_n = t_n\,\lsymb{in}\, u) ≈ u'$
+ \eTD\bTD (\currule{}\;$i_1$, \dots, $i_n$) \eTD\eTR
+ \eTD\bTD \eTD\eTR
+\stopAletheS
+
+ The premise $i_1, \dots, i_n$ must be in the same subproof as
+ the \currule{} step. If for $t_i≈ s_i$ the $t_i$ and $s_i$
+ are syntactically equal, the premise
+ is skipped.
+\stopRuleDescription
+
+\page
+\startRuleDescription{distinct_elim}
+This rule eliminates the $\lsymb{distinct}$ predicate. If called with one
+argument this predicate always holds:
+\startAletheS
+\setupTABLE[c][4][width=22em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD $\Gamma$ \eTD\bTD
+$(\lsymb{distinct}\, t) ≈ \top$
+\eTD\bTD \currule \eTD\eTR
+\stopAletheS
+
+If applied to terms of type $\lsymb{Bool}$ more than two terms can never be
+distinct, hence only two cases are possible:
+
+\startAletheS
+\setupTABLE[c][4][width=22em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD $\Gamma$ \eTD\bTD
+$(\lsymb{distinct}\,\varphi\,\psi) ≈ \neg (\varphi ≈ \psi)$
+\eTD\bTD \currule \eTD\eTR
+\stopAletheS
+
+\noindent
+and
+\startAletheS
+\setupTABLE[c][4][width=22em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD $\Gamma$ \eTD\bTD
+$(\lsymb{distinct}\,\varphi_1\,\varphi_2\,\varphi_3\,\dots) ≈ \bot$
+\eTD\bTD \currule \eTD\eTR
+\stopAletheS
+
+The general case is
+\startAletheS
+\setupTABLE[c][4][width=22em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD $\Gamma$ \eTD\bTD
+$(\lsymb{distinct}\,t_1\,\dots\, t_n) ≈
+\bigwedge_{i=1}^{n}\bigwedge_{j=i+1}^{n} t_i\;{≈\not}\;t_j$
+\eTD\bTD \currule \eTD\eTR
+\stopAletheS
+\stopRuleDescription
+
+\startRuleDescription{la_rw_eq}
+\startAlethe
+\setupTABLE[c][3][width=26em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD
+$(t ≈ u) ≈ (t \leq u \land u \leq t)$
+\eTD\bTD \currule \eTD\eTR
+\stopAlethe
+
+\tightpara{Remark.} While the connective could be $≈$,
+currently an equality is used.
+\stopRuleDescription
+
+\startRuleDescription{nary_elim}
+This rule replaces $n$-ary operators with their equivalent
+application of the binary operator. It is never applied to $\land$ or $\lor$.
+
+Three cases are possible.
+If the operator $\circ$ is left associative, then the rule has the form
+\startAletheS
+\setupTABLE[c][4][width=25em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD $\Gamma$ \eTD\bTD
+$\bigcirc_{i=1}^{n} t_i ≈
+(\dots( t_1\circ t_2) \circ t_3)\circ \cdots t_n)$
+\eTD\bTD \currule \eTD\eTR
+\stopAletheS
+
+If the operator $\circ$ is right associative, then the rule has the form
+\startAletheS
+\setupTABLE[c][4][width=25em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD $\Gamma$ \eTD\bTD
+$\bigcirc_{i=1}^{n} t_i ≈
+( t_1 \circ \cdots \circ ( t_{n-2} \circ ( t_{n-1} \circ t_n)\dots)$
+\eTD\bTD \currule \eTD\eTR
+\stopAletheS
+
+If the operator is {\em chainable}, then it has the form
+
+\startAletheS
+\setupTABLE[c][4][width=25em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD $\Gamma$ \eTD\bTD
+$\bigcirc_{i=1}^{n} t_i ≈
+( t_1\circ t_2) \land ( t_2 \circ t_3) \land \cdots
+\land ( t_{n-1}\circ t_n)$
+\eTD\bTD \currule \eTD\eTR
+\stopAletheS
+\stopRuleDescription
+
+\startRuleDescription{bfun_elim}
+\startAlethe
+\setupTABLE[c][3][width=24em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD
+$\psi$
+\eTD\bTD (\dots) \eTD\eTR
+\bTR\bTD $j$.\eTD\bTD \ctxsep \eTD\bTD
+$\varphi$
+\eTD\bTD (\currule\; $i$) \eTD\eTR
+\stopAlethe
+
+The formula $\varphi$ is $\psi$ after boolean functions have been simplified.
+This happens in a two step process. Both steps recursively iterate over $\psi$.
+The first step expands quantified variable of type $\lsymb{Bool}$. Hence,
+$(\exists x.\,t)$ becomes $t[x\mapsto \bot]\lor t[x\mapsto \top]$ and
+$(\forall x.\,t)$ becomes $t[x\mapsto \bot]\land t[x\mapsto \top]$. If $n$ variables of sort
+$\lsymb{Bool}$ appear in a quantifier, the disjunction (conjunction) has
+$2^n$ terms. Each term replaces the variables in $t$ according
+to the bits of a number which is increased by one for each subsequent
+term starting from zero. The left-most variable corresponds to the
+least significant bit.
+
+The second step expands function argument of boolean types by introducing
+appropriate if-then-else terms. For example, consider $(f\,x\, P\, y)$ where
+$P$ is some formula. Then we replace this term by $(\lsymb{ite}\, P\,
+(f\,x\, \top\ y)\,(f\,x\, \bot\, y))$. If the argument is already the constant $\top$
+or $\bot$, it is ignored.
+
+\stopRuleDescription
+
+\startRuleDescription{ite_intro}
+\startAlethe
+\setupTABLE[c][3][width=24em]
+\bTR\bTD $i$.\eTD\bTD \ctxsep \eTD\bTD
+$t ≈ (t' \land u_1 \land \dots \land u_n)$
+\eTD\bTD (\currule) \eTD\eTR
+\stopAlethe
+
+The term $t$ (the formula $\varphi$) contains the $\lsymb{ite}$ operator.
+Let $s_1, \dots, s_n$ be the terms starting with $\lsymb{ite}$, i.e.
+$s_i := \lsymb{ite}\,\psi_i\,r_i\,r'_i$, then $u_i$ has the form
+\startformula
+ \lsymb{ite}\,\psi_i\,(s_i ≈ r_i)\,(s_i ≈ r'_i)
+\stopformula
+
+\noindent
+The term $t'$ is equal to the term $t$ up to the
+reordering of equalities where one argument is an $\lsymb{ite}$
+term.
+
+\tightpara{Remark.} This rule stems from the introduction of fresh
+constants for if-then-else terms inside veriT. Internally $s_i$ is a new
+constant symbol and the $\varphi$ on the right side of the equality is
+$\varphi$ with the if-then-else terms replaced by the constants. Those
+constants are unfolded during proof printing. Hence, the slightly strange
+form and the reordering of equalities.
+\stopRuleDescription
+
+\page % TODO: double sided
+\subject[sec:alethe:rules-index]{Rule Index}
+\placeruleIndex[textstyle={\ss\addff{table}},style={\bf\WORDS}]
+
+\stoptitle
+\stopcomponent
+
diff --git a/spec/publications.bib b/spec/publications.bib
new file mode 100644
index 0000000000000000000000000000000000000000..4dca1ed0cd0b9f83a7631e2de6471f1afa8d0cc4
--- /dev/null
+++ b/spec/publications.bib
@@ -0,0 +1,1438 @@
+@misc{smtcomp21-rules,
+ title = "16th International Satisfiability Modulo Theories Competition ({SMT-COMP 2021}): Rules and Procedures",
+ author = "Barbosa, Haniel and Hoenicke, Jochen and Hyvarinen Antti",
+ howpublished = "\href{https://smt-comp.github.io/2021/rules.pdf}",
+ year = 2021,
+ note = "Accessed: 2021-08-08"
+}
+
+@inproceedings{pulp,
+ title={{PuLP} : A Linear Programming Toolkit for {Python}},
+ author={Stuart Mitchell and Michael O'Sullivan and Iain Dunning},
+ year={2011}
+}
+
+@misc{par2,
+ author = {Marijn Heule and Matti Järvisalo and Martin Suda},
+ title = {{SAT} Race 2019},
+ howpublished = {\href{http://sat-race-2019.ciirc.cvut.cz/}},
+ year = 2019,
+ note = "Accessed: 2022-02-28"
+}
+
+@inproceedings{gridtpt,
+ TITLE = {{GridTPT}: a distributed platform for Theorem Prover Testing},
+ AUTHOR = {Bouton, Thomas and Caminha B. De Oliveira, Diego and D{\'e}harbe, David and Fontaine, Pascal},
+ BOOKTITLE = {PAAR 2},
+ ADDRESS = {Edinburgh, United Kingdom},
+ YEAR = {2010},
+ pages={33--39},
+ MONTH = jul,
+}
+
+@inbook{manzano-1993,
+ author = {Manzano, Mar\'{\i}a},
+ title = {Introduction to Many-Sorted Logic},
+ year = {1993},
+ isbn = {0471934852},
+ publisher = {John Wiley & Sons, Inc.},
+ address = {USA},
+ booktitle = {Many-Sorted Logic and Its Applications},
+ pages = {3--86},
+ month=jan,
+ numpages = {84}
+}
+
+@inproceedings{wolf-1998,
+ author = {Wolf, Andreas and Letz, Reinhold},
+ title = {Strategy Parallelism in Automated Theorem Proving},
+ year = {1998},
+ doi = {10.5555/646811.706867},
+ publisher = {AAAI Press},
+ booktitle = {Proceedings of the Eleventh International Florida Artificial Intelligence Research Society Conference},
+ pages = {142--146},
+ numpages = {5}
+}
+
+@article{blanchette-2013,
+ author = {Jasmin Christian Blanchette and
+ Sascha B{\"{o}}hme and
+ Lawrence C. Paulson},
+ title = {Extending Sledgehammer with {SMT} Solvers},
+ journal = {Journal of Automated Reasoning},
+ volume = {51},
+ number = {1},
+ pages = {109--128},
+ year = {2013},
+ doi = {10.1007/s10817-013-9278-5},
+}
+
+@article{tamel-1997,
+ author = {Tammet, Tanel},
+ title = {Gandalf},
+ year = {1997},
+ doi = {10.1023/A:1005887414560},
+ journal = {Journal of Automated Reasoning},
+ pages = {199--204},
+ volume = {18},
+ number = {2},
+}
+
+
+@article{kuehlwein-2015,
+ author = {K\"{u}hlwein, Daniel and Urban, Josef},
+ title = {{MaLeS}: A Framework for Automatic Tuning of Automated Theorem Provers},
+ year = {2015},
+ publisher = {Springer},
+ address = {Berlin, Heidelberg},
+ volume = {55},
+ number = {2},
+ doi = {10.1007/s10817-015-9329-1},
+ journal = {Journal of Automated Reasoning},
+ month = {aug},
+ pages = {91-–116},
+ numpages = {26},
+}
+
+@incollection{rice-1976,
+ title = {The Algorithm Selection Problem},
+ editor = {Morris Rubinoff and Marshall C. Yovits},
+ series = {Advances in Computers},
+ publisher = {Elsevier},
+ volume = {15},
+ pages = {65--118},
+ year = {1976},
+ doi = {10.1016/S0065-2458(08)60520-3},
+ author = {John R. Rice},
+}
+
+@article{hutter-2009,
+ author = {Hutter, Frank and Hoos, Holger H. and Leyton-Brown, Kevin and St\"{u}tzle, Thomas},
+ title = {{ParamILS}: An Automatic Algorithm Configuration Framework},
+ year = {2009},
+ publisher = {AI Access Foundation},
+ address = {El Segundo, CA, USA},
+ volume = {36},
+ number = {1},
+ doi = {10.5555/1734953.1734959},
+ journal = {Journal of Artificial Intelligence Research},
+ month = {sep},
+ pages = {267--306},
+ numpages = {40}
+}
+
+@inproceedings{urban-2015,
+ author = {Josef Urban},
+ title = {{BliStr}: The Blind Strategymaker},
+ booktitle = {GCAI 2015},
+ editor = {Georg Gottlob and Geoff Sutcliffe and Andrei Voronkov},
+ series = {EPiC Series in Computing},
+ volume = {36},
+ pages = {312--319},
+ year = {2015},
+ publisher = {EasyChair},
+ issn = {2398-7340},
+ doi = {10.29007/8n7m}
+}
+
+@misc{casc-15-gandalf,
+ author = {Tanel Tammet},
+ title = {Gandalf c-1.1},
+ howpublished = {\href{http://www.tptp.org/CASC/15/SystemDescriptions.html#Gandalf}},
+ year = 1998,
+ note = "Accessed: 2022-03-24"
+}
+
+@article{riazanov-2003,
+ author = {Riazanov, Alexandre and Voronkov, Andrei},
+ title = {Limited Resource Strategy in Resolution Theorem Proving},
+ year = {2003},
+ issue_date = {July 2003},
+ publisher = {Academic Press, Inc.},
+ address = {USA},
+ volume = {36},
+ number = {1–2},
+ doi = {10.1016/S0747-7171(03)00040-3},
+ journal = {Journal of Symbolic Computation},
+ month = {jul},
+ pages = {101--115},
+ numpages = {15}
+}
+
+@InProceedings{wenzel-2013,
+ author="Wenzel, Makarius",
+ editor="Blazy, Sandrine
+ and Paulin-Mohring, Christine
+ and Pichardie, David",
+ title="Shared-Memory Multiprocessing for Interactive Theorem Proving",
+ booktitle="ITP 4",
+ year="2013",
+ publisher="Springer Berlin Heidelberg",
+ pages="418--434",
+ doi="10.1007/978-3-642-39634-2_30"
+}
+
+@InProceedings{desharnais-2022,
+ author = {Desharnais, Martin and Vukmirovi\'{c}, Petar and Blanchette, Jasmin and Wenzel, Makarius},
+ title = {{Seventeen Provers Under the Hammer}},
+ booktitle = {ITP 13},
+ pages = {8:1--8:18},
+ series = {Leibniz International Proceedings in Informatics (LIPIcs)},
+ year = {2022},
+ volume = {237},
+ editor = {Andronick, June and de Moura, Leonardo},
+ publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
+ address = {Dagstuhl, Germany},
+ doi = {10.4230/LIPIcs.ITP.2022.8},
+}
+
+@misc{weber-2018,
+ author = {Tjark Weber},
+ title = {{Par4}},
+ howpublished = {\href{http://smt2019.galois.com/papers/tool_paper_9.pdf}},
+ year = 2018,
+ note = "SMT-COMP 2018 system description. Accessed: 2022-03-30"
+}
+
+@inproceedings{balunovic-2018,
+ author = {Balunovi\'{c}, Mislav and Bielik, Pavol and Vechev, Martin},
+ title = {Learning to Solve {SMT} Formulas},
+ year = {2018},
+ publisher = {Curran Associates Inc.},
+ booktitle = {NIPS 32},
+ pages = {10338--10349},
+ doi = {10.5555/3327546.3327694},
+ numpages = {12},
+ location = {Montr\'{e}al, Canada},
+}
+
+@inbook{demoura-2013,
+ author="de Moura, Leonardo
+ and Passmore, Grant Olney",
+ editor="Bonacina, Maria Paola
+ and Stickel, Mark E.",
+ title="The Strategy Challenge in {SMT} Solving",
+ bookTitle="Automated Reasoning and Mathematics: Essays in Memory of William W. McCune",
+ year="2013",
+ publisher="Springer",
+ address="Berlin, Heidelberg",
+ pages="15--44",
+ doi="10.1007/978-3-642-36675-8_2",
+}
+
+@inproceedings{ReyEtAl-FROCOS-17,
+ author = {Andrew Reynolds and
+ Cesare Tinelli and
+ Dejan Jovanovic and
+ Clark W. Barrett},
+ title = {Designing Theory Solvers with Extensions},
+ booktitle = {FroCoS 11},
+ pages = {22--40},
+ doi = {10.1007/978-3-319-66167-4\_2},
+ editor = {Clare Dixon and
+ Marcelo Finger},
+ series = {Lecture Notes in Computer Science},
+ volume = {10483},
+ publisher = {Springer},
+ year = {2017},
+}
+
+@InProceedings{scott-2021,
+ author="Scott, Joseph
+ and Niemetz, Aina
+ and Preiner, Mathias
+ and Nejati, Saeed
+ and Ganesh, Vijay",
+ editor="Groote, Jan Friso
+ and Larsen, Kim Guldstrand",
+ title="MachSMT: A Machine Learning-based Algorithm Selector for {SMT} Solvers",
+ booktitle="TACAS 27",
+ year="2021",
+ doi="10.1007/978-3-030-72013-1_16",
+ publisher="Springer International Publishing",
+ address="Cham",
+ pages="303--325"
+}
+
+@article{burel-2020,
+ author = {Guillaume Burel and
+ Guillaume Bury and
+ Rapha{\"{e}}l Cauderlier and
+ David Delahaye and
+ Pierre Halmagrand and
+ Olivier Hermant},
+ title = {First-Order Automated Reasoning with Theories: When Deduction Modulo
+ Theory Meets Practice},
+ journal = {Journal of Automated Reasoning},
+ volume = {64},
+ number = {6},
+ pages = {1001--1050},
+ year = {2020},
+ doi = {10.1007/s10817-019-09533-z},
+}
+
+@article{dowek-2015,
+ author = {Gilles Dowek},
+ title = {Deduction modulo theory},
+ journal = {CoRR},
+ volume = {abs/1501.06523},
+ year = {2015},
+ url = {http://arxiv.org/abs/1501.06523},
+ eprinttype = {arXiv},
+ eprint = {1501.06523},
+ timestamp = {Mon, 13 Aug 2018 16:47:14 +0200},
+ biburl = {https://dblp.org/rec/journals/corr/Dowek15a.bib},
+ bibsource = {dblp computer science bibliography, https://dblp.org}
+}
+
+@article{xu-2008,
+ author = {Xu, Lin and Hutter, Frank and Hoos, Holger H. and Leyton-Brown, Kevin},
+ title = {{SATzilla}: Portfolio-Based Algorithm Selection for {SAT}},
+ year = {2008},
+ issue_date = {May 2008},
+ publisher = {AI Access Foundation},
+ address = {El Segundo, CA, USA},
+ volume = {32},
+ number = {1},
+ journal = {Journal of Artificial Intelligence Research},
+ month = {jun},
+ doi = {10.5555/1622673.1622687},
+ pages = {565--606},
+ numpages = {42}
+}
+
+@InProceedings{barbosa-2022,
+ author="Barbosa, Haniel
+ and Barrett, Clark
+ and Brain, Martin
+ and Kremer, Gereon
+ and Lachnitt, Hanna
+ and Mann, Makai
+ and Mohamed, Abdalrhman
+ and Mohamed, Mudathir
+ and Niemetz, Aina
+ and N{\"o}tzli, Andres
+ and Ozdemir, Alex
+ and Preiner, Mathias
+ and Reynolds, Andrew
+ and Sheng, Ying
+ and Tinelli, Cesare
+ and Zohar, Yoni",
+ editor="Fisman, Dana
+ and Rosu, Grigore",
+ title="{cvc5}: A Versatile and Industrial-Strength {SMT} Solver",
+ booktitle="TACAS 28",
+ year="2022",
+ publisher="Springer International Publishing",
+ address="Cham",
+ pages="415--442",
+ doi="10.1007/978-3-030-99524-9_24"
+}
+
+@InProceedings{barbosa-2017,
+ author = "Barbosa, Haniel
+ and Fontaine, Pascal
+ and Reynolds, Andrew",
+ editor = "Legay, Axel
+ and Margaria, Tiziana",
+ title = "Congruence Closure with Free Variables",
+ booktitle = "TACAS 23",
+ year = "2017",
+ series = {Lecture Notes in Computer Science},
+ volume = "10206",
+ publisher = "Springer Berlin Heidelberg",
+ pages = "214--230",
+ doi = {10.1007/978-3-662-54580-5\_13}
+}
+
+@phdthesis{barbosa-2017-phd,
+ author = {Haniel Barbosa},
+ title = {New techniques for instantiation and proof production in {SMT} solving.
+ (Nouvelles techniques pour l'instanciation et la production des preuves
+ dans {SMT)}},
+ school = {University of Lorraine, Nancy, France},
+ year = {2017},
+ url = {https://tel.archives-ouvertes.fr/tel-01591108},
+}
+
+@InProceedings{vampire,
+author="Kov{\'a}cs, Laura
+and Voronkov, Andrei",
+editor="Sharygina, Natasha
+and Veith, Helmut",
+title="First-Order Theorem Proving and {Vampire}",
+booktitle="CAV 25",
+year="2013",
+publisher="Springer Berlin Heidelberg",
+pages="1--35",
+isbn="978-3-642-39799-8",
+doi={10.1007/978-3-642-39799-8\_1}
+}
+
+@InProceedings{SMTCoq,
+ author = "Ekici, Burak
+ and Mebsout, Alain
+ and Tinelli, Cesare
+ and Keller, Chantal
+ and Katz, Guy
+ and Reynolds, Andrew
+ and Barrett, Clark",
+ editor = "Majumdar, Rupak
+ and Kun{\v{c}}ak, Viktor",
+ title = "{SMTC}oq: A Plug-In for Integrating {SMT} Solvers into {C}oq",
+ booktitle = "CAV 29",
+ series = {Lecture Notes in Computer Science},
+ volume = {10426},
+ year = "2017",
+ publisher = "Springer",
+ pages = "126--133",
+ isbn = "978-3-319-63390-9",
+ doi = {10.1007/978-3-319-63390-9\_7}
+}
+
+@INPROCEEDINGS{reynolds-2014,
+ author={Andrew {Reynolds} and Cesare {Tinelli} and Leonardo {de Moura}},
+ booktitle={{FMCAD} 14},
+ title={Finding conflicting instances of quantified formulas in {SMT}},
+ doi = {10.1109/FMCAD.2014.6987613},
+ year = {2014},
+ publisher = {IEEE},
+ pages = {195-202},
+}
+
+@inproceedings{verit,
+ author = {Thomas Bouton
+ and Diego C. B. de Oliveira
+ and David D{\'{e}}harbe
+ and Pascal Fontaine},
+ title = {{veriT}: An Open, Trustable and Efficient {SMT}-solver},
+ booktitle = "CADE 22",
+ pages = {151--156},
+ year = {2009},
+ editor = {Renate A. Schmidt},
+ series = {Lecture Notes in Computer Science},
+ volume = {5663},
+ publisher = "Springer Berlin Heidelberg",
+ doi = {10.1007/978-3-642-02959-2_12}
+}
+
+@inproceedings{CVC4,
+ author="Barrett, Clark
+ and Conway, Christopher L.
+ and Deters, Morgan
+ and Hadarean, Liana
+ and Jovanovi{\'{c}}, Dejan
+ and King, Tim
+ and Reynolds, Andrew
+ and Tinelli, Cesare",
+ editor = "Gopalakrishnan, Ganesh
+ and Qadeer, Shaz",
+ title = {{CVC4}},
+ booktitle = "CAV 23",
+ year = "2011",
+ series = {Lecture Notes in Computer Science},
+ volume = {6806},
+ publisher = "Springer Berlin Heidelberg",
+ pages = "171--177",
+ doi = {10.1007/978-3-642-22110-1_14}
+}
+
+@inproceedings{reynolds-2018,
+ author = {Andrew Reynolds and
+ Haniel Barbosa and
+ Pascal Fontaine},
+ title = {Revisiting Enumerative Instantiation},
+ booktitle = {TACAS 24},
+ pages = {112--131},
+ year = {2018},
+ doi = {10.1007/978-3-319-89963-3_7},
+ editor = {Dirk Beyer and
+ Marieke Huisman},
+ series = {Lecture Notes in Computer Science},
+ volume = {10806},
+ publisher = {Springer International Publishing}
+}
+
+@InProceedings{Z3,
+ author = "de Moura, Leonardo
+ and Bj{\o}rner, Nikolaj",
+ editor = "Ramakrishnan, C. R.
+ and Rehof, Jakob",
+ title = "{Z3}: An Efficient {SMT} Solver",
+ booktitle = "TACAS 14",
+ volume = {4963},
+ series = {Lecture Notes in Computer Science},
+ year = "2008",
+ publisher = "Springer Berlin Heidelberg",
+ pages = "337--340",
+ doi = {10.1007/978-3-540-78800-3_24}
+}
+
+@TECHREPORT{SMTLIB,
+ author = {Clark Barrett and Pascal Fontaine and Cesare Tinelli},
+ title = {{The SMT-LIB Standard: Version 2.6}},
+ institution = {Department of Computer Science, The University of Iowa},
+ year = 2017,
+ note = {Available at \texttt{www.SMT-LIB.org}}
+}
+
+
+@incollection{barrett-2021,
+ author={Clark W. Barrett and Roberto Sebastiani and Sanjit A. Seshia and Cesare Tinelli},
+ editor = {Biere, Armin and Heule, Marijn and van Maaren, Hans and Walsh, Toby},
+ title = {Satisfiability Modulo Theories},
+ booktitle = {Handbook of Satisfiability},
+ title = {Satisfiability Modulo Theories},
+ booktitle = {Handbook of Satisfiability -- Second Edition},
+ series = {Frontiers in Artificial Intelligence and Applications},
+ volume = {336},
+ pages = {1267--1329},
+ publisher = {{IOS} Press},
+ year = {2021},
+ doi = {10.3233/FAIA201017},
+}
+
+@InProceedings{yeting-2007,
+ author="Ge, Yeting
+ and Barrett, Clark
+ and Tinelli, Cesare",
+ editor="Pfenning, Frank",
+ title="Solving Quantified Verification Conditions Using Satisfiability Modulo Theories",
+ booktitle="CADE 21",
+ year="2007",
+ publisher="Springer Berlin Heidelberg",
+ pages="167--182",
+ doi={10.1007/978-3-540-73595-3_12}
+}
+
+@InProceedings{demoura-2007,
+ author="de Moura, Leonardo
+ and Bj{\o}rner, Nikolaj",
+ editor="Pfenning, Frank",
+ title="Efficient {E}-Matching for {SMT} Solvers",
+ booktitle="CADE 21",
+ year="2007",
+ publisher="Springer Berlin Heidelberg",
+ pages="183--198",
+ doi={10.1007/978-3-540-73595-3\_13}
+}
+
+@article{detlefs-2005,
+ author = {Detlefs, David and Nelson, Greg and Saxe, James B.},
+ title = {{Simplify}: A Theorem Prover for Program Checking},
+ year = {2005},
+ publisher = {Association for Computing Machinery},
+ address = {New York, NY, USA},
+ volume = {52},
+ number = {3},
+ issn = {0004-5411},
+ doi = {10.1145/1066100.1066102},
+ journal = {Journal of the ACM},
+ month = may,
+ pages = {365–473},
+ numpages = {109},
+}
+
+@article{nelson-1979,
+author = {Nelson, Greg and Oppen, Derek C.},
+title = {Simplification by Cooperating Decision Procedures},
+year = {1979},
+publisher = {Association for Computing Machinery},
+address = {New York, NY, USA},
+volume = {1},
+number = {2},
+doi = {10.1145/357073.357079},
+journal = {ACM Transactions on Programming Languages and Systems},
+month = {oct},
+pages = {245--257},
+numpages = {13}
+}
+
+@InProceedings{yeting-2009,
+ author="Ge, Yeting
+ and de Moura, Leonardo",
+ editor="Bouajjani, Ahmed
+ and Maler, Oded",
+ title="Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories",
+ booktitle="CAV 21",
+ year="2009",
+ publisher="Springer Berlin Heidelberg",
+ pages="306--320",
+ doi={10.1007/978-3-642-02658-4_25}
+}
+
+@inbook{sekar-2001,
+ author = {Sekar, R. and Ramakrishnan, I. V. and Voronkov, Andrei},
+ title = {Term Indexing},
+ year = {2001},
+ isbn = {0444508120},
+ publisher = {Elsevier Science Publishers B. V.},
+ address = {Amsterdam, Netherlands},
+ booktitle = {Handbook of Automated Reasoning},
+ pages = {1853--1964},
+ numpages = {112},
+ doi={10.5555/778522.778535}
+}
+
+@inproceedings{besson-2011,
+ title = {A Flexible Proof Format for {SMT}: A Proposal},
+ author = {Besson, Fr{\'e}d{\'e}ric and Fontaine, Pascal and Th{\'e}ry, Laurent},
+ editor = "Pascal Fontaine and Aaron Stump",
+ booktitle = {PxTP 1},
+ year = {2011},
+ pages = "15--26",
+ url = {https://hal.inria.fr/hal-00642544/},
+ month = Aug,
+}
+
+@inproceedings{deharbe-2011,
+ TITLE = {Quantifier Inference Rules for {SMT} Proofs},
+ AUTHOR = {D{\'e}harbe, David and Fontaine, Pascal and Woltzenlogel Paleo, Bruno},
+ editor = "Pascal Fontaine and Aaron Stump",
+ BOOKTITLE = {PxTP 1},
+ YEAR = {2011},
+ pages = "33--39",
+ MONTH = Aug,
+ url = {https://hal.inria.fr/hal-00642535}
+}
+
+
+@article{martelli-1982,
+ author = {Martelli, Alberto and Montanari, Ugo},
+ title = {An Efficient Unification Algorithm},
+ year = {1982},
+ publisher = {Association for Computing Machinery},
+ address = {New York, NY, USA},
+ volume = {4},
+ number = {2},
+ doi = {10.1145/357162.357169},
+ journal = {ACM Transactions on Programming Languages and Systems},
+ month = apr,
+ pages = {258-–282},
+ numpages = {25}
+}
+
+@incollection{baaz-2001,
+ title = {Chapter 5 -- Normal Form Transformations},
+ editor = {Alan Robinson and Andrei Voronkov},
+ booktitle = {Handbook of Automated Reasoning},
+ publisher = {North-Holland},
+ address = {Amsterdam},
+ pages = {273--333},
+ year = {2001},
+ series = {Handbook of Automated Reasoning},
+ doi = {10.1016/B978-044450813-3/50007-2},
+ author = {Matthias Baaz and Uwe Egly and Alexander Leitsch and Jean Goubault-Larrecq and David Plaisted}
+}
+
+@InProceedings{schurr-2021,
+author="Schurr, Hans-J{\"o}rg
+and Fleury, Mathias
+and Desharnais, Martin",
+editor="Platzer, Andr{\'e}
+and Sutcliffe, Geoff",
+title="Reliable Reconstruction of Fine-grained Proofs in a Proof Assistant",
+booktitle="CADE 28",
+year="2021",
+publisher="Springer International Publishing",
+address="Cham",
+pages="450--467",
+series = {Lecture Notes in Computer Science},
+doi= {10.1007/978-3-030-79876-5_26}
+}
+
+@inproceedings{schurr-2021a,
+ author = "Fontaine, Pascal
+ and Schurr, Hans-J{\"o}rg",
+ editor = "Konev, Boris and Reger, Giles",
+ title = "Quantifier Simplification by Unification in SMT",
+ booktitle = "FroCoS 13",
+ year = "2021",
+ publisher = "Springer International Publishing",
+ address = "Cham",
+ pages = "232--249",
+ doi = "10.1007/978-3-030-86205-3_13",
+}
+
+
+@article{robinson-1965,
+author = {Robinson, John Alan},
+title = {A Machine-Oriented Logic Based on the Resolution Principle},
+year = {1965},
+publisher = {Association for Computing Machinery},
+address = {New York, NY, USA},
+volume = {12},
+number = {1},
+doi = {10.1145/321250.321253},
+journal = {Journal of the ACM},
+month = jan,
+pages = {23–41},
+numpages = {19}
+}
+
+@article{bonacina-2011,
+ author = {Bonacina, Maria Paola and Lynch, Christopher and de Moura, Leonardo},
+ year = {2011},
+ month = {08},
+ pages = {161-189},
+ title = {On Deciding Satisfiability by Theorem Proving with Speculative Inferences},
+ volume = {47},
+ journal = {Journal of Automated Reasoning},
+ doi = {10.1007/s10817-010-9213-y}
+}
+
+@InProceedings{demoura-2008,
+author="de Moura, Leonardo
+and Bj{\o}rner, Nikolaj",
+editor="Armando, Alessandro
+and Baumgartner, Peter
+and Dowek, Gilles",
+title="Engineering {DPLL(T)} + Saturation",
+year="2008",
+publisher="Springer Berlin Heidelberg",
+pages="475--490",
+doi={10.1007/978-3-540-71070-7\_40},
+booktitle="IJCAR 4",
+}
+
+@InProceedings{voronkov-2014,
+author="Voronkov, Andrei",
+editor="Biere, Armin
+and Bloem, Roderick",
+title="{AVATAR}: The Architecture for First-Order Theorem Provers",
+booktitle="CAV 26",
+year="2014",
+publisher="Springer International Publishing",
+pages="696--710",
+doi={10.1007/978-3-319-08867-9\_46},
+isbn="978-3-319-08867-9"
+}
+
+@proceedings{zenodo,
+ title = {Quantifier Simplification by Unification in {SMT}},
+ author = {Pascal Fontaine and Hans-Jörg Schurr},
+ year = 2021,
+ publisher = {Zenodo},
+ month = jul,
+ doi = {10.5281/zenodo.5088868},
+}
+
+
+@misc{ip-tutorial,
+ title = "A Tutorial on Integer Programming",
+ author = "Gérard Cornuéjols and Michael A. Trick and Matthew J. Saltzman",
+ howpublished = "\href{https://www.math.clemson.edu/~mjs/courses/mthsc.440/integer.pdf}",
+ year = 1995,
+ note = "Accessed: 2022-04-07"
+}
+
+@inproceedings{fontaine-21,
+ author = "Fontaine, Pascal
+ and Schurr, Hans-J{\"o}rg",
+ editor = "Konev, Boris and Reger, Giles",
+ title = "Quantifier Simplification by Unification in {SMT}",
+ booktitle = "Frontiers of Combining Systems",
+ year = "2021",
+ publisher = "Springer International Publishing",
+ address = "Cham",
+ pages = "232--249",
+ doi = "10.1007/978-3-030-86205-3_13",
+}
+
+@misc{tange_2021_5123056,
+ author = {Tange, Ole},
+ title = {{GNU} Parallel 20210722 ('Blue Unity')},
+ month = jul,
+ year = 2021,
+ note = {{GNU Parallel is a general parallelizer to run
+ multiple serial command line programs in parallel
+ without changing them.}},
+ publisher = {Zenodo},
+ doi = {10.5281/zenodo.5123056},
+ url = {https://doi.org/10.5281/zenodo.5123056}
+}
+
+@article{nieuwenhuis-06,
+ author = {Nieuwenhuis, Robert and Oliveras, Albert and Tinelli, Cesare},
+ title = {Solving {SAT} and {SAT} Modulo Theories: From an Abstract Davis--Putnam--Logemann--Loveland Procedure to DPLL(T)},
+ year = {2006},
+ issue_date = {November 2006},
+ publisher = {Association for Computing Machinery},
+ address = {New York, NY, USA},
+ volume = {53},
+ number = {6},
+ doi = {10.1145/1217856.1217859},
+ journal = {Journal of the ACM},
+ month = {nov},
+ pages = {937--977},
+ numpages = {41},
+}
+
+@phdthesis{dross-2014,
+ author = {Claire Dross},
+ title = {Generic Decision Procedures for Axiomatic First-Order Theories},
+ school = {Universit{\'e} Paris-Sud},
+ year = 2014,
+ month = apr
+}
+
+@InProceedings{leino-2016,
+author="Leino, K. R. M.
+and Pit-Claudel, Cl{\'e}ment",
+editor="Chaudhuri, Swarat
+and Farzan, Azadeh",
+title="Trigger Selection Strategies to Stabilize Program Verifiers",
+booktitle="Computer Aided Verification",
+year="2016",
+publisher="Springer International Publishing",
+address="Cham",
+pages="361--381",
+doi="10.1007/978-3-319-41528-4_20"
+}
+
+@inproceedings{reynolds-2016,
+ author = {Andrew Reynolds},
+ title = {Conflicts, Models and Heuristics for Quantifier Instantiation in {SMT}},
+ booktitle = {Vampire 3},
+ editor = {Laura Kovacs and Andrei Voronkov},
+ series = {EPiC Series in Computing},
+ volume = {44},
+ pages = {1--15},
+ year = {2017},
+ publisher = {EasyChair},
+ doi = {10.29007/jmd3}
+}
+
+@InProceedings{blanchette-2011,
+ author = "Blanchette, Jasmin Christian and B{\"o}hme, Sascha and
+ Paulson, Lawrence C.",
+ editor = "Bj{\o}rner, Nikolaj and Sofronie-Stokkermans, Viorica",
+ title = "Extending {Sledgehammer} with {SMT} Solvers",
+ booktitle = "CADE 23",
+ year = "2011",
+ series = {Lecture Notes in Computer Science},
+ volume = {6803},
+ publisher = "Springer Berlin Heidelberg",
+ pages = "116--130",
+ doi = {10.1007/978-3-642-22438-6\_11}
+}
+
+@InProceedings{bohme-2010,
+ author = "B{\"o}hme, Sascha
+ and Weber, Tjark",
+ editor = "Kaufmann, Matt
+ and Paulson, Lawrence C.",
+ title = "Fast {LCF}-Style Proof Reconstruction for {Z3}",
+ booktitle = "ITP 1",
+ series = {Lecture Notes in Computer Science},
+ volume = "6172",
+ year = "2010",
+ publisher = "Springer Berlin Heidelberg",
+ pages = "179--194",
+ doi = {10.1007/978-3-642-14052-5\_14}
+}
+
+@article{Blanchette2016-isar,
+ author = {Blanchette, Jasmin C. and
+ B{\"{o}}hme, Sascha and
+ Fleury, Mathias and
+ Smolka, Steffen J. and
+ Albert Steckermeier},
+ title = {Semi-intelligible {I}sar Proofs from Machine-Generated Proofs},
+ journal = jar,
+ volume = {56},
+ number = {2},
+ pages = {155--200},
+ year = {2016},
+ doi = {10.1007/s10817-015-9335-3},
+}
+
+@InProceedings{ebner-2021,
+ author="Ebner, Gabriel
+ and Blanchette, Jasmin
+ and Tourret, Sophie",
+ editor="Platzer, Andr{\'e}
+ and Sutcliffe, Geoff",
+ title="A Unifying Splitting Framework",
+ booktitle="CADE 28",
+ year="2021",
+ publisher="Springer International Publishing",
+ address="Cham",
+ doi = {10.1007/978-3-030-79876-5_20},
+ pages="344--360",
+}
+
+@inproceedings{mikolas-2021,
+ author="Janota, Mikoláš and Barbosa, Haniel and Fontaine, Pascal and Reynolds, Andrew",
+ editor="Piskac, Ruzica and Whalen, Michael W.",
+ title="Fair and Adventurous Enumeration of Quantifier Instantiations",
+ booktitle="FMCAD 21",
+ year=2021,
+ publisher="TU Wien Academic Press",
+ address="Vienna, Austria",
+ doi={10.34727/2021/isbn.978-3-85448-046-4},
+ pages="256-–260"
+}
+
+@article{barbosa-2019,
+ title = "Scalable Fine-Grained Proofs for Formula Processing",
+ journal = "Journal of Automated Reasoning",
+ year = {2019},
+ month = jan,
+ author = "Barbosa, Haniel
+ and Blanchette, Jasmin C.
+ and Fleury, Mathias
+ and Fontaine, Pascal",
+ publisher = "Springer",
+ doi = {10.1007/s10817-018-09502-y},
+volume = {64},
+ number = {3},
+ pages = {485--510},
+ year = {2020},
+}
+
+@inproceedings{fleury-2019,
+ author = {Mathias Fleury and
+ Hans{-}J{\"{o}}rg Schurr},
+ editor = {Giselle Reis and
+ Haniel Barbosa},
+ title = {Reconstructing {veriT} Proofs in {Isabelle/HOL}},
+ booktitle = {PxTP 6},
+ series = {{EPTCS}},
+ volume = {301},
+ pages = {36--50},
+ year = {2019},
+ doi = {10.4204/EPTCS.301.6},
+}
+
+@book{gordon-1979-lcf,
+ author = {Michael J. C. Gordon and
+ Robin Milner and
+ Christopher P. Wadsworth},
+ title = {Edinburgh {LCF}: A Mechanised Logic of Computation},
+ series = {Lecture Notes in Computer Science},
+ volume = {78},
+ publisher = {Springer Berlin Heidelberg},
+ year = {1979},
+ doi = {10.1007/3-540-09724-4}
+}
+
+@inproceedings{verit-ho,
+ author = {Haniel Barbosa and
+ Andrew Reynolds and
+ Daniel El Ouraoui and
+ Cesare Tinelli and
+ Clark W. Barrett},
+ editor = {Pascal Fontaine},
+ title = {Extending {SMT} Solvers to Higher-Order Logic},
+ booktitle = {CADE 27},
+ series = {Lecture Notes in Computer Science},
+ volume = {11716},
+ pages = {35--54},
+ publisher = {Springer International Publishing},
+ year = {2019},
+ doi = {10.1007/978-3-030-29436-6\_3},
+}
+
+@techreport{SRI:simplex:dpllt,
+ author = { Bruno Dutertre and Leonardo de Moura},
+ title = { Integrating Simplex with {DPLL(T)} },
+ year = {2006},
+ month = may,
+ url = {http://www.csl.sri.com/users/bruno/publis/sri-csl-06-01.pdf},
+ institution = { {SRI International} },
+}
+
+@article{schulz-2002,
+ author = {Stephan Schulz},
+ title = {{E} -- a brainiac theorem prover},
+ journal = {{AI} Communications},
+ volume = {15},
+ number = {2-3},
+ pages = {111--126},
+ year = {2002},
+ publisher = {IOS Press},
+}
+
+@article{green-jar,
+ author = {Mohammad Abdulaziz and
+ Lawrence C. Paulson},
+ title = {An {Isabelle/HOL} Formalisation of {Green}'s Theorem},
+ journal = jar,
+ volume = {63},
+ number = {3},
+ pages = {763--786},
+ year = {2019},
+ month = nov,
+ doi = {10.1007/s10817-018-9495-z},
+}
+
+@article{Prime_Distribution_Elementary-AFP,
+ author = {Manuel Eberl},
+ title = {Elementary Facts About the Distribution of Primes},
+ journal = {Archive of Formal Proofs},
+ month = feb,
+ url = {https://isa-afp.org/entries/Prime_Distribution_Elementary.html},
+ year = 2019,
+ note = {Formal proof development},
+ ISSN = {2150-914x},
+}
+
+@article{Simplex-AFP,
+ author = {Filip Marić and Mirko Spasić and René Thiemann},
+ title = {An Incremental Simplex Algorithm with Unsatisfiable Core Generation},
+ journal = {Archive of Formal Proofs},
+ month = aug,
+ year = 2018,
+ url = {https://isa-afp.org/entries/Simplex.html},
+ note = {Formal proof development},
+ ISSN = {2150-914x},
+}
+
+@misc{bug-report,
+ author = {Fabian Immler},
+ year = {2019},
+ month = may,
+ title = {{Re: [isabelle] Isabelle2019-RC2 sporadic smt failures}},
+ howpublished = {Email},
+ url = {https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2019-May/msg00130.html}
+}
+
+
+@article{Ordered_Resolution_Prover-AFP,
+ author = {Schlichtkrull, Anders and Blanchette, Jasmin C. and Traytel, Dmitriy and Waldmann, Uwe},
+ title = {Formalization of {B}achmair and {G}anzinger's Ordered Resolution Prover},
+ journal = {Archive of Formal Proofs},
+ month = jan,
+ year = 2018,
+ url = {https://isa-afp.org/entries/Ordered_Resolution_Prover.html},
+ note = {Formal proof development},
+ ISSN = {2150-914x},
+}
+
+
+@inproceedings{barbosa-2016,
+ author = {Haniel Barbosa},
+ title = {Efficient Instantiation Techniques in {SMT} (Work In Progress)},
+ pages = {1--10},
+ year = {2016},
+ month = jul,
+ url = {http://ceur-ws.org/Vol-1635/#paper-01},
+ editor = {Pascal Fontaine and
+ Stephan Schulz and
+ Josef Urban},
+ title = {{PAAR} 5},
+ volume = {1635},
+ publisher = {CEUR-WS.org},
+}
+
+@article{Prime_Number_Theorem-AFP,
+ author = {Manuel Eberl and Lawrence C. Paulson},
+ title = {The Prime Number Theorem},
+ journal = {Archive of Formal Proofs},
+ month = sep,
+ year = 2018,
+ url = {https://isa-afp.org/entries/Prime_Number_Theorem.html},
+ note = {Formal proof development},
+ ISSN = {2150-914x},
+}
+
+
+@article{Lambda_Free_KBOs-AFP,
+ author = {Heiko Becker and Jasmin Christian Blanchette and Uwe Waldmann and Daniel Wand},
+ title = {Formalization of {Knuth–Bendix} Orders for Lambda-Free Higher-Order Terms},
+ journal = {Archive of Formal Proofs},
+ month = nov,
+ year = 2016,
+ url = {https://isa-afp.org/entries/Lambda_Free_KBOs.html},
+ note = {Formal proof development},
+ ISSN = {2150-914x},
+}
+
+
+@article{green-afp,
+ author = {Mohammad Abdulaziz and Lawrence C. Paulson},
+ title = {An {Isabelle/HOL} formalisation of {Green}'s Theorem},
+ journal = {Archive of Formal Proofs},
+ month = jan,
+ year = 2018,
+ url = {https://isa-afp.org/entries/Green.html},
+ note = {Formal proof development},
+ ISSN = {2150-914x},
+}
+
+@article{meng-2009,
+ author = {Jia Meng and
+ Paulson, Lawrence C. },
+ title = {Lightweight relevance filtering for machine-generated resolution problems},
+ doi = {10.1016/j.jal.2007.07.004},
+ journal = {Journal of Applied Logic},
+ volume = {7},
+ number = {1},
+ pages = {41--57},
+ year = {2009}
+}
+
+@inproceedings{kuehlwein-2013,
+ author = {K{\"{u}}hlwein, Daniel and
+ Blanchette, Jasmin Christian and
+ Kaliszyk, Cezary and
+ Urban, Josef},
+ title = {{MaSh}: Machine Learning for {Sledgehammer}},
+ booktitle = {{ITP} 4},
+ series = {{LNCS}},
+ volume = {7998},
+ pages = {35--50},
+ publisher = {Springer},
+ year = {2013},
+ doi = {10.1007/978-3-642-39634-2_6}
+}
+
+@InProceedings{judgementday,
+ author = "B{\"o}hme, Sascha and Nipkow, Tobias",
+ editor = "Giesl, J{\"u}rgen and H{\"a}hnle, Reiner",
+ title = "{Sledgehammer}: Judgement Day",
+ booktitle = "IJCAR 5",
+ year = "2010",
+ publisher = "Springer Berlin Heidelberg",
+ pages = "107--121",
+ doi = {10.1007/978-3-642-14203-1_9}
+}
+
+@proceedings{schurr_hans_jorg_2021_4727349,
+ title = {{Reliable Reconstruction of Fine-Grained Proofs in
+ a Proof Assistant}},
+ author = {Hans-Jörg Schurr
+ and Mathias Fleury
+ and Martin Desharnais},
+ year = 2021,
+ publisher = {Zenodo},
+ month = apr,
+ doi = {10.5281/zenodo.4727349},
+}
+
+@inproceedings{rodin,
+ TITLE = {{SMT} solvers for {R}odin},
+ AUTHOR = {D{\'e}harbe, David
+ and Fontaine, Pascal
+ and Guyot, Yoann
+ and Voisin, Laurent},
+ BOOKTITLE = {{ABZ 2012}},
+ EDITOR = {John Derrick
+ and John A. Fitzgerald
+ and Stefania Gnesi
+ and Sarfraz Khurshid
+ and Michael Leuschel
+ and Steve Reeves
+ and Elvinia Riccobene},
+ publisher = "Springer Berlin Heidelberg",
+ SERIES = lncs,
+ VOLUME = {7316},
+ PAGES = {194-207},
+ YEAR = {2012},
+ MONTH = Jun,
+ doi = {10.1007/978-3-642-30885-7_14}
+}
+
+@inproceedings{interpolants,
+ author = {Kenneth L. McMillan},
+ title = {Interpolants from {Z3} proofs},
+ booktitle = {{FMCAD} 11},
+ isbn = {9780983567813},
+ publisher = {FMCAD Inc},
+ address = {Austin, Texas},
+ pages = {19--27},
+ year = {2011},
+}
+
+@article{mclaughlin-2006,
+ author = {Sean McLaughlin and
+ Clark Barrett and
+ Yeting Ge},
+ title = {Cooperating Theorem Provers: {A} Case Study Combining {HOL-Light} and
+ {CVC} {L}ite},
+ journal = {Electronic Notes in Theoretical Computer Science},
+ volume = {144},
+ number = {2},
+ pages = {43--51},
+ year = {2006},
+ doi = {10.1016/j.entcs.2005.12.005}
+}
+
+@inproceedings{armand-2011,
+ author = {Micha{\"e}l Armand and
+ Germain Faure and
+ Benjamin Gr{\'e}goire and
+ Chantal Keller and
+ Laurent Th{\'e}ry and
+ Benjamin Werner},
+ title = {A Modular Integration of {SAT}\slash{SMT} Solvers to {Coq} through
+ Proof Witnesses},
+ booktitle = {CPP~1},
+ pages = {135--150},
+ editor = {Jean-Pierre Jouannaud and
+ Zhong Shao},
+ publisher = {Springer Berlin Heidelberg},
+ series = lncs,
+ volume = {7086},
+ year = {2011},
+ doi = {10.1007/978-3-642-25379-9_12}
+}
+
+@inproceedings{ekici-2017,
+ author = {Burak Ekici and
+ Alain Mebsout and
+ Cesare Tinelli and
+ Chantal Keller and
+ Guy Katz and
+ Andrew Reynolds and
+ Clark W. Barrett},
+ title = {{SMTCoq}: {A} Plug-In for Integrating {SMT} Solvers into {Coq}},
+ booktitle = {CAV 29},
+ pages = {126--133},
+ year = {2017},
+ doi = {10.1007/978-3-319-63390-9_7},
+ editor = {Rupak Majumdar and
+ Viktor Kuncak},
+ series = lncs,
+ volume = {10427},
+ publisher = {Springer International Publishing},
+}
+
+@phdthesis{bohme-thesis,
+ author = {Sascha B\"ohme},
+ title = {Proving Theorems of Higher-Order Logic with {SMT} Solvers},
+ school = {Technische Universit\"at M\"unchen},
+ year = 2012,
+ url = {http://mediatum.ub.tum.de/node?id=1084525}
+}
+
+@article{stump-2013,
+ author = {Stump, Aaron and Oe, Duckki and Reynolds, Andrew and Hadarean,
+ Liana and Tinelli, Cesare},
+ title = {{SMT} Proof Checking Using a Logical Framework},
+ journal = {Formal Methods in System Design},
+ volume = {42},
+ number = {1},
+ month = feb,
+ year = {2013},
+ issn = {0925-9856},
+ pages = {91--118},
+ numpages = {28},
+ publisher = {Kluwer Academic Publishers},
+ doi = {10.1007/s10703-012-0163-3}
+}
+
+@inproceedings{christ-2012,
+ author = {J{\"{u}}rgen Christ and
+ Jochen Hoenicke and
+ Alexander Nutz},
+ editor = {Alastair F. Donaldson and
+ David Parker},
+ title = {SMTInterpol: An Interpolating {SMT} Solver},
+ booktitle = {SPIN 19},
+ series = {Lecture Notes in Computer Science},
+ volume = {7385},
+ pages = {248--254},
+ publisher = {Springer},
+ year = {2012},
+ doi = {10.1007/978-3-642-31759-0_19},
+}
+
+@InProceedings{hyvarinen-2016,
+ author="Hyv{\"a}rinen, Antti E. J.
+ and Marescotti, Matteo
+ and Alt, Leonardo
+ and Sharygina, Natasha",
+ editor="Creignou, Nadia
+ and Le Berre, Daniel",
+ title="{OpenSMT2}: An {SMT} Solver for Multi-core and Cloud Computing",
+ booktitle="SAT 19",
+ year="2016",
+ publisher="Springer International Publishing",
+ address="Cham",
+ pages="547--553",
+ isbn="978-3-319-40970-2"
+}
+
+@InProceedings{barbosa-2022a,
+ author="Barbosa, Haniel
+ and Reynolds, Andrew
+ and Kremer, Gereon
+ and Lachnitt, Hanna
+ and Niemetz, Aina
+ and N{\"o}tzli, Andres
+ and Ozdemir, Alex
+ and Preiner, Mathias
+ and Viswanathan, Arjun
+ and Viteri, Scott
+ and Zohar, Yoni
+ and Tinelli, Cesare
+ and Barrett, Clark",
+ editor="Blanchette, Jasmin
+ and Kov{\'a}cs, Laura
+ and Pattinson, Dirk",
+ title="Flexible Proof Production in an Industrial-Strength SMT Solver",
+ booktitle="IJCAR 11",
+ year="2022",
+ publisher="Springer International Publishing",
+ address="Cham",
+ pages="15--35",
+ doi={10.1007/978-3-031-10769-6_3}
+}
+
+
+@inproceedings{hoenicke-2022,
+ author = {Jochen Hoenicke and
+ Tanja Schindler},
+ editor = {David D{\'{e}}harbe and
+ Antti E. J. Hyv{\"{a}}rinen},
+ title = {A Simple Proof Format for {SMT}},
+ booktitle = {SMT 20},
+ series = {{CEUR} Workshop Proceedings},
+ volume = {3185},
+ pages = {54--70},
+ publisher = {CEUR-WS.org},
+ year = {2022},
+}
+
+@inproceedings{schurr-2022,
+ author = {Hans-Jörg Schurr},
+ editor = {Boris Konev and
+ Claudia Schon and
+ Alexander Steen},
+ title = {Optimal Strategy Schedules for Everyone},
+ booktitle = {PAAR 8},
+ series = {{CEUR} Workshop Proceedings},
+ volume = {3201},
+ publisher = {CEUR-WS.org},
+ year = {2022},
+}
+
+@inproceedings{otoni-2021,
+ title = {Theory-Specific Proof Steps Witnessing Correctness of {SMT} Executions},
+ booktitle = {DAC 58},
+ year = {2021},
+ month = {11},
+ publisher = {IEEE},
+ organization = {IEEE},
+ address = {San Francisco, CA, USA},
+ doi = {10.1109/DAC18074.2021.9586272},
+ author = {Rodrigo Otoni and Martin Blicha and Patrick Eugster and Antti E. J. Hyv{\"a}rinen and Natasha Sharygina}
+}
+
+@inproceedings{assaf-2016,
+ TITLE = {Expressing theories in the λΠ-calculus modulo theory and in the {Dedukti} system},
+ AUTHOR = {Assaf, Ali and Burel, Guillaume and Cauderlier, Raphal and Delahaye, David and Dowek, Gilles and Dubois, Catherine and Gilbert, Fr{\'e}d{\'e}ric and Halmagrand, Pierre and Hermant, Olivier and Saillard, Ronan},
+ BOOKTITLE = {{TYPES}: Types for Proofs and Programs},
+ ADDRESS = {Novi SAd, Serbia},
+ YEAR = {2016},
+ MONTH = May,
+}
+
+
+@article{Downey1980,
+ author = {Downey, Peter J. and Sethi, Ravi and Tarjan, Robert Endre},
+ title = {Variations on the Common Subexpression Problem},
+ journal = {Journal of the ACM},
+ volume = {27},
+ number = {4},
+ month = oct,
+ year = {1980},
+ issn = {0004-5411},
+ pages = {758--771},
+ numpages = {14},
+ doi = {10.1145/322217.322228},
+ acmid = {322228},
+ publisher = {ACM},
+ address = {New York, NY, USA}
+}
+
+@article{Nelson1980,
+ author = {Nelson, Greg and Oppen, Derek C.},
+ title = {Fast Decision Procedures Based on Congruence Closure},
+ journal = {Journal of the ACM},
+ month = apr,
+ volume = {27},
+ number = {2},
+ year = {1980},
+ pages = {356--364},
+ numpages = {9},
+ doi = {10.1145/322186.322198},
+ publisher = {ACM}
+}
+
+@inproceedings{biere-2020,
+ title={CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling Entering the {SAT} Competition 2020},
+ author={Armin Biere and Katalin Fazekas and Mathias Fleury and Maximilian Heisinger},
+ year={2020}
+}
+
+@inproceedings{barbosa-2019a,
+ author = {Haniel Barbosa and
+ Andrew Reynolds and
+ Daniel El Ouraoui and
+ Cesare Tinelli and
+ Clark W. Barrett},
+ editor = {Pascal Fontaine},
+ title = {Extending {SMT} Solvers to Higher-Order Logic},
+ booktitle = {{CADE 27}},
+ series = {Lecture Notes in Computer Science},
+ volume = {11716},
+ pages = {35--54},
+ publisher = {Springer},
+ year = {2019},
+ doi = {10.1007/978-3-030-29436-6\_3},
+}
+
+@misc{aguirre-2016,
+ author = {Alejandro Aguirre},
+ title = {Towards a Provably Correct Encoding from {F*} to {SMT}},
+ howpublished = {Inria Internship Report},
+ month = aug,
+ year = {2016},
+ url = {http://prosecco.gforge.inria.fr/personal/hritcu/students/alejandro/report.pdf},
+}
+
+@misc{matryoshka,
+ author = {Jasmin Blanchette},
+ title = {Matryoshka},
+ howpublished = {Project Webpage},
+ note = "Accessed: 2022-07-14",
+ month = july,
+ year = {2022},
+ url = {https://matryoshka-project.github.io/#},
+}
+
+@inproceedings{defourne-2021,
+ TITLE = {Improving Automation for Higher-Order Proof Steps},
+ AUTHOR = {Defourn{\'e}, Rosalie},
+ BOOKTITLE = {FroCos 13},
+ ADDRESS = {Birmingham, United Kingdom},
+ EDITOR = {Boris Konev and Giles Reger},
+ PUBLISHER = {{Springer}},
+ SERIES = {FroCoS 13},
+ VOLUME = {12941},
+ PAGES = {139--153},
+ YEAR = {2021},
+ MONTH = Sep,
+ DOI = {10.1007/978-3-030-86205-3_8},
+}
+
+@misc{wp:alethe,
+author = "{Wikipedia contributors}",
+title = "Alethe (bird) --- {Wikipedia}{,} The Free Encyclopedia",
+year = "2022",
+url = "https://en.wikipedia.org/w/index.php?title=Alethe_(bird)&oldid=1064503766",
+note = "Online; accessed 2022-09-02"
+}
+
+@inproceedings{claessen-2003,
+author = {Claessen, Koen and Sorensson, Niklas},
+year = {2003},
+month = {08},
+pages = {},
+title = {New Techniques that Improve {MACE}-style Finite Model Finding},
+ BOOKTITLE = {MODEL},
+}
+
diff --git a/spec/spec.tex b/spec/spec.tex
new file mode 100644
index 0000000000000000000000000000000000000000..90e52d487e9b22544c120b166138d3e14a4f2d20
--- /dev/null
+++ b/spec/spec.tex
@@ -0,0 +1,1520 @@
+\documentclass{scrartcl}
+
+
+\usepackage{scrlayer-scrpage}
+\usepackage{hyperref}
+\usepackage{breakurl}
+\usepackage{unicode-math}
+\usepackage{fontsetup}
+
+\usepackage{minted}
+\usemintedstyle{trac}
+% TODO: tweak hilighter
+\newminted[AletheVerb]{smtlib2.py -x}{}
+\newmintinline[inlineAlethe]{smtlib2.py -x}{}
+
+\usepackage{cite}
+\usepackage{url}
+\usepackage[useregional]{datetime2}
+\usepackage{xltabular} % Gives us stretchable, breakable tables. for proofs
+\usepackage{environ} % Gives us NewEnviron to define environements with tables
+\usepackage{fancyvrb} % Gives us \Verb which can be used in footnotes
+
+\usepackage{tikz}
+\usetikzlibrary{tikzmark,positioning}
+\usetikzlibrary{shapes,arrows,fit, scopes}
+\usetikzlibrary{arrows.meta}
+\usetikzlibrary{svg.path}
+
+\usepackage{bussproofs}
+\EnableBpAbbreviations
+
+\usepackage{amsthm}
+
+\usepackage[english]{babel}
+\nonfrenchspacing
+
+\usepackage[final,tracking=true,stretch=10,shrink=10]{microtype}
+\microtypecontext{spacing=nonfrench}
+% Used for Aletheia in greek
+%\newfontfamily\greekfont[Script=Greek, Scale=MatchUppercase, Ligatures=TeX]{CMU Serif}
+
+\hyphenation{Isa-belle Nieuw-en-huis meta-logic multi-set multi-sets non-unit Mini-Sat}
+
+\newcommand\smtlib{SMT-LIB}
+\newcommand\cdclt{CDCL(T)}
+
+\newcommand\tool[1]{\textsf{#1}}
+\newcommand\tactic[1]{\texttt{#1}}
+\newcommand\verit{\tool{veriT}}
+\newcommand\cvcfive{\tool{cvc5}}
+\newcommand\cvcfour{\tool{CVC4}}
+\newcommand\isabelle{\tool{Isabelle/HOL}}
+
+\newcommand\lsymb[1]{\mathbf{#1}}
+\DeclareMathOperator*{\subst}{subst}
+\DeclareMathOperator*{\reify}{reify}
+\newcommand\groundbox[1]{\boxed{#1}}
+
+% Proofs
+\newcommand\textAlethe[1]{\texttt{#1}}
+\newcommand\ctxsep{$\vartriangleright$}
+\newcommand\spctxsep{\multicolumn{1}{|c}{\ctxsep}}
+\newcommand\spctx[1]{\multicolumn{1}{|c}{#1}}
+\newcommand\spsep{\cline{2-4}}
+\newcolumntype{Y}{>{\centering\arraybackslash}X}
+
+\newcommand{\ruleTypeImpl}[1]{%
+ \microtypesetup{tracking=false}\textsf{#1}\microtypesetup{tracking=true}%
+}
+\def\ruleType#1{\ruleTypeImpl{\detokenize{#1}}}
+\def\proofRule#1{\hyperref[rule:\detokenize{#1}]{\ruleTypeImpl{\detokenize{#1}}}}
+%\newcommand{\ruleref}[1]{\ruleType{\nameref{rule:#1}}~(\ref{rule:#1})}
+
+\NewEnviron{Alethe}{%
+\renewcommand\spsep{\cline{2-4}}
+\setlength{\arrayrulewidth}{0.8pt}
+\addtolength{\tabcolsep}{-4pt}
+\begin{xltabular}{\linewidth}{l c Y l}
+ \BODY
+\end{xltabular}
+\addtolength{\tabcolsep}{+4pt}
+}
+\NewEnviron{AletheS}{%
+\renewcommand\spsep{\cline{2-5}}
+\setlength{\arrayrulewidth}{0.8pt}
+\addtolength{\tabcolsep}{-4pt}
+\begin{xltabular}{\linewidth}{l l c Y l}
+ \BODY
+\end{xltabular}
+\addtolength{\tabcolsep}{+4pt}
+}
+
+% TODO: synchronize colors!
+\definecolor{SmtBlue}{HTML}{00007f}
+\definecolor{SmtGreen}{HTML}{3b7f31}
+\definecolor{SmtStepId}{HTML}{3b7f31}
+
+\newcommand{\grNT}[1]{\textcolor{SmtGreen}{\langle\texttt{#1}\rangle}}
+\newcommand{\grT}[1]{\textcolor{SmtBlue}{\texttt{#1}}}
+\newcommand{\grRule}{≔}
+\newcommand{\grOr}{|}
+
+\theoremstyle{definition}
+\newtheorem{example}{Example}
+\newtheorem{theorem}{Theorem}[example]
+\newtheorem{lemma}{Lemma}[example]
+\newtheorem{definition}{Definition}[example]
+\newtheorem{seppara}{}
+
+\title{The Alethe Proof Format}
+\subtitle{An Evolving Specification and Reference}
+\author{Haniel Barbosa\textsuperscript{1}
+\and Mathias Fleury\textsuperscript{2}
+\and Pascal Fontaine\textsuperscript{3}
+\and Hans-Jörg Schurr\textsuperscript{4}}
+\date{}
+\publishers{
+ \textsuperscript{1} Universidade Federal de Minas Gerais\\
+ \textsuperscript{2} Johannes Kepler University Linz\\
+ \textsuperscript{3} Université de Liège\\
+ \textsuperscript{4} University of Lorraine, CNRS, Inria, and LORIA, Nancy\\
+}
+
+
+\begin{document}
+
+\maketitle
+\tableofcontents
+\clearpage
+
+\begin{abstract}
+\section*{Foreword}
+This document is a speculative specification and reference of a proof
+format for SMT solvers. The format consists of a language to express
+proofs and a set of proof rules. On the one side, the language is
+inspired by natural-deduction and is based on the widely used SMT-LIB
+format. The language also includes a flexible mechanism to reason
+about bound variables which allows fine-grained preprocessing proofs.
+%
+On the other side, the rules are structured around resolution and the
+introduction of theory lemmas, in the same way as CDCL(T)-based SMT
+solvers.
+
+The specification is not yet
+cast in stone, but it will evolve over time. It emerged from a list
+of proof rules used by the SMT solver veriT collected in a document
+called ``Proofonomicon''. Following the fate presupposed by its name,
+it informally circulated among researchers interested in the proofs
+produced by veriT after a few months. We now polished this document
+and gave it a respectable name.
+
+Instead of aiming for theoretical purity, our approach
+is pragmatic: the specification describes the format as it is in use
+right now. It will develop in parallel with practical support for the
+format within SMT solvers, proof checkers, and other tools. We believe
+it is not a perfect specification that fosters the adaption of a format,
+but great tooling. This document will be a guide to develop
+such tools.
+
+Nevertheless, it not only serves as a norm to ensure compatibility
+between tools, it also allows us to uncover the unsatisfactory aspects
+that would otherwise be hidden deep within the nooks and crannies of
+solver and checker implementations.
+%
+Every uncovered problem presents an opportunity
+to improve the format. The authors of this document overlap with the
+authors of those tools and we are committed to improve the tools, the
+format, and ultimately the specification together.
+This document is also an invitation to other researchers to join
+these efforts. To read the reference and provide feedback, or to even
+implement support for Alethe into their own tools. Please
+get in touch!
+
+\bigskip
+\hspace*{\fill}The authors.
+\end{abstract}
+
+This document is a reference of the
+Alethe\footnote{Alethe is a genus of small birds that occur in West Africa~\cite{wp:alethe}.
+The name was chosen, because it
+resembles the Greek word {αλήθεια} (alÃtheia) -- truth.} proof format. Alethe is
+designed to be a flexible format to represent unsatisfiability proofs
+generated by SMT solvers. Alethe proofs can be consumed by other systems,
+such as interactive theorem provers or proof checkers. The design
+is based on natural-deduction style structure
+and rules generating and operating on first-order clauses.
+%
+The Alethe calculus consists of two parts: the proof
+language based on {\smtlib} and a collection of proof rules.
+Section~\ref{sec:alethe:language} introduces the language. First as an
+abstract language, then as a concrete syntax.
+%
+Section~\ref{sec:alethe:rules-generic} discusses the core
+concepts behind the Alethe proof rules.
+%
+The Section~\ref{apx:rules} presents a list of
+all proof rules currently used by {\verit}.
+
+Alethe follows a few core design principles. First, proofs should
+be easy to understand by humans to ensure working with Alethe proofs
+is easy. Second, the language of the format should directly
+correspond to the language used by the solver. Since many solvers use the
+{\smtlib} language, Alethe also uses this language.
+Therefore, Alethe's base logic is the many-sorted first-order logic of {\smtlib}.
+Third, the format should
+be uniform for all theories used by SMT solvers. With the exception
+of clauses for propositional reasoning, there is no dedicated syntax for
+any theory.
+
+The format is currently used by the SMT solver {\verit}. If requested
+by the user, {\verit} outputs a proof if it can deduce that the input problem is
+unsatisfiable. In proof production mode, {\verit} supports the theory of
+uninterpreted functions, the theory of linear integer and real arithmetic, and
+quantifiers.
+%
+The Alethe proofs can be reconstructed by the \tactic{smt} tactic of
+the proof assistant {\isabelle}~\cite{fleury-2019,schurr-2021}~(see
+Section~\ref{sec:reconstruction}). The \tool{SMTCoq} tool can
+reconstruct an older version of the format in the
+proof assistant \tool{Coq}~\cite{SMTCoq}. An effort to update the
+tool to the latest version of Alethe is ongoing.
+%
+The SMT solver {\cvcfive}~\cite{barbosa-2022} (the successor of
+{\cvcfour}) supports Alethe experimentally as one of its multiple proof
+output formats.
+%
+Furthermore, there is an experimental
+high-performance proof checker written in Rust.\footnote{Available at
+\url{https://github.com/ufmg-smite/carcara}.}
+
+In addition to this reference, the proof format has been discussed in past
+publications, which provide valuable background information. The core of
+the format goes back to 2011 when two publications at the PxTP workshop
+outlined the fundamental ideas behind the format~\cite{besson-2011}
+and proposed rules for quantifier instantiation~\cite{deharbe-2011}.
+%
+More recently, the format has gained support for reasoning typically used for
+processing, such as skolemization, substitutions, and other manipulations of
+bound variables~\cite{barbosa-2019}.
+
+
+\section{The Alethe Language}
+\label{sec:alethe:language}
+
+This section provides an overview of the core concepts of the
+\index{Alethe}Alethe language and also introduces some notation used
+throughout this chapter.
+The section first introduces an abstract notation to write Alethe proofs.
+Then, it introduces the concrete, {\smtlib}-based syntax. Finally,
+we show how a concrete Alethe proof can be checked.
+
+\begin{example}
+The following example shows a simple Alethe proof
+expressed in the abstract notation used in this document.
+It uses quantifier instantiation and resolution to show a contradiction.
+The paragraphs below describe the concepts necessary to
+understand the proof step by step.
+
+\begin{Alethe}
+1.& \ctxsep & $\forall x.\, (P\,x)$ & $ \proofRule{assume}$ \\
+2.& \ctxsep & $\neg (P\,a) $ & $ \proofRule{assume}$ \\
+3.& \ctxsep & $\neg (\forall x.\, (P\,x)) \lor (P\,a)$ & $\proofRule{forall_inst}\,[(x, a)]$ \\
+4.& \ctxsep & $\neg (\forall x.\, (P\,x)), (P\,a)$ & $ (\proofRule{or}\:3)$ \\
+5.& \ctxsep & $\bot $ & $ (\proofRule{resolution}\: 1, 2, 4)$ \\
+\end{Alethe}
+
+\end{example}
+
+\paragraph{Many-Sorted First-Order Logic.}
+Alethe builds on the {\smtlib} language.
+%
+This includes its many-sorted first-order logic described in
+Section~\ref{sec:ti-logic}. % TODO: clarify!
+The available sorts depend on
+the selected {\smtlib} theory/logic as well as on those defined by the user, but the
+distinguished $\lsymb{Bool}$ sort is always available.
+%
+However, Alethe also extends this logic with Hilbert's choice
+operator $\varepsilon$.
+%
+The term $\varepsilon x.\, \varphi[x]$ stands for a value $v$
+such that $\varphi[v]$ is true if such a value exists. Any value is
+possible otherwise. Alethe requires that $\varepsilon$ is functional
+with respect to logical equivalence: if for two formulas $\varphi$, $\psi$
+that contain the free variable $x$, it holds that
+$(\forall x.\,\varphi ≈ \psi)$,
+then $(\varepsilon x.\, \varphi)\approx(\varepsilon x.\, \psi)$ must also hold.
+Note that, choice terms can only appear in Alethe proofs, not in {\smtlib} problems.
+%\end{seppara}
+
+\paragraph{Steps.}
+A \index{proof}proof in the Alethe language is an indexed list of \index{step}steps.
+To mimic the concrete syntax of Alethe proofs, proof steps in the
+abstract notation have the form
+
+\begin{AletheS}
+$i$.& $c_1,\,\dots,\, c_j$ & \ctxsep &
+$l_1,\dots ,l_k$ & $(\ruleType{rule}\; p_1,\,\dots,\, p_n)\,[a_1,\,\dots,\,a_m]$ \\
+\end{AletheS}
+
+\noindent
+Each step has a unique index $i \in \mathbb{I}$, where $\mathbb{I}$ is a countable
+infinite set of valid indices. In the concrete syntax all {\smtlib} symbols are
+valid indices, but for examples we will use natural numbers.
+%
+Furthermore, $l_1, \dots ,l_k$ is a clause with the literals
+$l_i$. It is the conclusion of the step. If a step has the empty clause
+as its conclusion (i.e., $k = 0$) we write $\bot$. While this
+muddles the water a bit with regard to steps which have the unit clause
+with the unit literal $\bot$ as their conclusion, it simplifies the
+notation. We will remark on the difference if it is relevant. The rule
+name \ruleType{rule} is taken from a set of possible proof
+rules (see Section~\ref{apx:rules}).
+Furthermore, each step has a possibly empty set of premises $\{p_1,
+\dots, p_n\} \subseteq \mathbb{I}$,
+and a rule-dependent and possibly
+empty list of arguments $[a_1, \dots, a_m]$. The list of premises
+only references earlier steps, such that the proof forms a directed
+acyclic graph. If the list of premises is empty, we will drop the
+parentheses around the proof rule.
+The arguments $a_i$ are either terms or tuples $(x_i,
+t_i)$ where $x_i$ is a variable and $t_i$ is a term. The interpretation
+of the arguments is rule specific. The list $c_1, \dots, c_j$ is
+the \index{context}{\em context} of the step. Contexts are discussed below.
+Every proof ends with a step that has the empty clause as the conclusion
+and an empty context. The list of proof rules in the appendix also uses
+this notation to define the proof rules.
+
+The example above consists of five steps. Step~4 and~5 use premises.
+Since step~3 introduces a tautology, it uses no premises. However,
+it uses arguments to express the substitution $[x\mapsto a]$ used to instantiate
+the quantifier. Step~4 translates the disjunction into a clause.
+In the example above, the contexts are all empty.
+
+\paragraph{Assumptions.}
+An \proofRule{assume} step introduces a term as an
+\index{assumption}assumption. The proof starts with a number of
+\proofRule{assume} steps. Each such step corresponds to an input
+assertion. Within a subproof, additional assumptions can be introduced
+too. In this case, each assumption must be discharged with an appropriate
+step. The rule \proofRule{subproof} can be used to do so. In the concrete
+syntax, \proofRule{assume} steps have a dedicated command \inlineAlethe{assume}
+to clearly distinguish them from normal steps that use the \inlineAlethe{step}
+command (see~Section~\ref{sec:alethe:syntax}).
+
+The example above uses two assumptions which are introduced in the first
+two steps.
+
+
+\paragraph{Subproofs and Lemmas.}
+Alethe uses subproofs to prove lemmas and to create and manipulate the context.
+%
+To prove \index{lemma}lemmas, a \index{subproof}subproof can
+introduce local assumptions. The \proofRule{subproof} {\em rule} discharges the
+local assumptions.
+From an
+assumption $\varphi$ and a formula $\psi$ proved
+from $\varphi$, the \proofRule{subproof} rule deduces the clause $\neg \varphi,
+\psi$ that discharges the local assumption $\varphi$.
+%
+A \proofRule{subproof} step cannot use a premise from a subproof nested
+within the current subproof.
+
+Subproofs are also used to manipulate the context.
+As the example below shows, the abstract notation denotes subproofs by a
+frame around the steps in the subproof. In this case the subproof
+concludes with a step that does not use the \proofRule{subproof} rule,
+but another rule, such as the \proofRule{bind} rule.
+
+\begin{example}
+This example shows a refutation of the
+formula $(2 + 2) ≈ 5$. The proof uses a subproof to prove the
+lemma $((2 + 2) ≈ 5) \Rightarrow 4 ≈ 5$.
+
+\begin{Alethe}
+1.& \ctxsep & $(2 + 2) ≈ 5$ & $\proofRule{assume}$ \\
+2.& \spctxsep & $(2 + 2) ≈ 5 $ & $\proofRule{assume}$ \\
+3.& \spctxsep & $(2 + 2) ≈ 4 $ & $\proofRule{sum_simplify}$ \\
+4.& \spctxsep & $4 ≈ 5 $ & $(\proofRule{trans}\ 2, 3)$ \\
+\spsep
+5.& \ctxsep & $\neg((2 + 2) ≈ 5), 4 ≈ 5$ & $\proofRule{subproof}$ \\
+6.& \ctxsep & $(4 ≈ 5)≈ \bot$ & $\proofRule{eq_simplify}$ \\
+7.& \ctxsep & $\neg((4 ≈ 5)≈ \bot), \neg(4≈ 5), \bot $ & $\proofRule{equiv_pos2}$ \\
+8.& \ctxsep & $\bot $ & $(\proofRule{resolution}\ 1, 5, 6, 7)$ \\
+\end{Alethe}
+
+\end{example}
+
+\paragraph{Contexts.}
+A specificity of the Alethe proofs
+is the step \index{context}context.
+Alethe contexts are a general mechanism to write
+substitutions and to change them by attaching new elements.
+A context is a possible empty list $c_1,
+\dots, c_l$, where each element is either a variable or a variable-term tuple
+denoted $x_i\mapsto t_i$.
+%
+In the first case, we say that $c_i$ {\em fixes} the
+variable. The second case is a mapping.
+Throughout this chapter, $\Gamma$ denotes
+an arbitrary context.
+
+% TODO: define \subst and related
+Every context $\Gamma$ induces a substitution
+$\subst(\Gamma)$. If $\Gamma$ is the empty list,
+$\subst(\Gamma)$ is the empty substitution, i.e, the
+identity function.
+The first case fixes $x_n$ and allows the context to shadow a previously defined
+substitution for $x_n$:
+\[
+\subst([c_1,\dots, c_{n-1}, x_n])
+\text{ is }\subst([c_1,\dots, c_{n-1}])\text{, but }x_n\text{ maps to }x_n.
+\]
+
+When $\Gamma$ ends in a mapping, the substitution is extended
+with this mapping:
+\[
+\subst([c_1,\dots, c_{n-1}, x_n\mapsto t_n]) =
+ \subst([c_1,\dots, c_{n-1}])\circ \{x_n\mapsto t_n\}.
+\]
+
+
+\label{ex:alethe:substctx}The following example illustrates this idea:
+\begin{align*}
+ \subst([x\mapsto 7, x \mapsto g(x)]) &= \{x\mapsto g(7)\} \\
+ \subst([x\mapsto 7, x, x \mapsto g(x)]) &= \{x\mapsto g(x)\} \\
+\end{align*}
+
+Contexts are used to express proofs about the preprocessing of terms. The
+conclusions of proof rules that use contexts always have the form
+\begin{AletheS}
+i. & $\Gamma$ & \ctxsep & $t ≈ u$ & ($\ruleType{rule}$, …) \\
+\end{AletheS}
+
+where the term $t$\, is the original term, and $u$ is the term after
+preprocessing. Tautologies with contexts correspond to judgments
+$\vDash_T \subst(\Gamma)(t) ≈ u$.
+
+Formally, the context can be translated to \index{abstraction+lambda}λ-abstractions and
+applications. This is discussed in Section~\ref{sec:alethe:semantic}.
+
+
+\begin{example}\label{ex:ti:ctx-abstract}
+This example shows a proof that uses a subproof with a context to rename a bound
+variable.
+\begin{AletheS}
+1.& & \ctxsep & $\forall x.\,(P\,x)$ & $\proofRule{assume}$ \\
+2.& & \ctxsep & $\neg (\forall y.\,(P\,y))$ & $\proofRule{assume}$ \\
+3.& \spctx{$y, x \mapsto y$} & \ctxsep & $x ≈ y$ & $\proofRule{refl}$\\
+4.& \spctx{$y, x \mapsto y$} & \ctxsep & $(P\,x) ≈ (P\,y)$
+ & $(\proofRule{cong}\,3) $\\
+\spsep
+5.& & \ctxsep & $\forall x.\,(P\,x) ≈ \forall y.\,(P\,y)$ & $\proofRule{bind}$ \\
+6.& & \ctxsep &
+ $\neg(\forall x.\,(P\,x) ≈ \forall y.\,(P\,y))$, $\neg(\forall x.\,(P\,x)), (\forall y.\,(P\,y))$
+ & $\proofRule{equiv_pos2}$ \\
+7.& &\ctxsep & $\bot$ & $(\proofRule{resolution}\,1, 2, 5, 6)$ \\
+\end{AletheS}
+\end{example}
+
+
+\paragraph{Implicit Reordering of Equalities.}
+In addition to the explicit steps, solvers might reorder equalities,
+i.e., apply symmetry of the equality predicate, without generating steps.
+The sole exception is the topmost equality in the conclusion of steps
+with non-empty context. The order of the arguments of this equality can
+never change.
+As described above, all rules that accept a non-empty context have
+a conclusion of the form $t ≈ u$. Since the context
+represents a substitution applied to the left-hand side,
+this equality symbol is not symmetric.
+
+The SMT solver {\verit} currently applies this freedom in a restricted
+form: equalities are reordered only
+when the term below the equality changes during proof search. One such
+case is the instantiation of universally quantified variables. If an
+instantiated variable appears below an equality, then the equality might
+have an arbitrary order after instantiation.
+Nevertheless, consumers of Alethe must consider the possible
+implicit reordering of equalities everywhere.
+
+
+\subsection{The Syntax}\label{sec:alethe:syntax}
+
+The concrete text representation of the Alethe proofs
+is based on the {\smtlib} standard. Figure~\ref{fig:proof_ex} shows an
+example proof as printed by {\verit} with light edits for readability.
+%
+The format follows the {\smtlib} standard when possible.
+%
+Input problems in the {\smtlib} formats are scripts. A {\smtlib} script
+is a list of commands that manipulate the SMT solver. For example,
+\inlineAlethe{assert} introduces an assertion, \inlineAlethe{check-sat} starts
+solving, and \inlineAlethe{get-proof} instructs the SMT solver to print the
+proof.
+%
+Alethe mirrors this structure. Therefore, beside the {\smtlib}
+logic and term language, it also uses commands to structure the proof.
+An Alethe proof is a list of commands.
+
+\begin{figure}[t]
+ \begin{AletheVerb}
+(assume h1 (not (p a)))
+(assume h2 (forall ((z1 U)) (forall ((z2 U)) (p z2))))
+...
+(anchor :step t9 :args ((:= z2 vr4)))
+(step t9.t1 (cl (= z2 vr4)) :rule refl)
+(step t9.t2 (cl (= (p z2) (p vr4)))
+ :rule cong :premises (t9.t1))
+(step t9 (cl (= (forall ((z2 U)) (p z2))
+ (forall ((vr4 U)) (p vr4))))
+ :rule bind)
+...
+(step t14 (cl (forall ((vr5 U)) (p vr5)))
+ :rule th_resolution :premises (t11 t12 t13))
+(step t15 (cl (or (not (forall ((vr5 U)) (p vr5)))
+ (p a)))
+ :rule forall_inst :args ((:= vr5 a)))
+(step t16 (cl (not (forall ((vr5 U)) (p vr5))) (p a))
+ :rule or :premises (t15))
+(step t17 (cl) :rule resolution :premises (t16 h1 t14))
+ \end{AletheVerb}
+\caption{Example proof output. Assumptions are
+ introduced; a subproof renames bound variables; the proof finishes with
+ instantiation and resolution steps.}
+\label{fig:proof_ex}
+\end{figure}
+
+
+\begin{figure}[t]
+\[
+ \begin{array}{r c l}
+ \grNT{proof} &\grRule & \grNT{proof\_command}^{*} \\
+ \grNT{proof\_command} &\grRule & \textAlethe{(assume}\; \grNT{symbol}\; \grNT{proof\_term}\,\textAlethe{)} \\
+ &\grOr & \textAlethe{(step}\; \grNT{symbol}\; \grNT{clause}
+ \; \textAlethe{:rule}\; \grNT{symbol} \\
+ & & \quad \grNT{premises\_annotation}^{?} \\
+ & & \quad \grNT{context\_annotation}^{?}\;\grNT{attribute}^{*}\,\textAlethe{)} \\
+ & \grOr & \textAlethe{(anchor :step}\; \grNT{symbol}\;
+ \\
+ & & \quad \grNT{args\_annotation}^{?}\;\grNT{attribute}^{*}\,\textAlethe{)} \\
+ & \grOr & \textAlethe{(define-fun}\; \grNT{function\_def}\,\textAlethe{)} \\
+ \grNT{clause} &\grRule & \textAlethe{(cl}\; \grNT{proof\_term}^{*}\,\textAlethe{)} \\
+ \grNT{proof\_term} &\grRule & \grNT{term}\text{ extended with } \\
+ & & \textAlethe{(choice (}\, \grNT{sorted\_var}\,\textAlethe{)}\; \grNT{proof\_term}\,\textAlethe{)} \\
+ \grNT{premises\_annotation} &\grRule & \textAlethe{:premises (}\; \grNT{symbol}^{+}\textAlethe{)} \\
+ \grNT{args\_annotation} &\grRule & \textAlethe{:args}\,\textAlethe{(}\,\grNT{step\_arg}^{+}\,\textAlethe{)} \\
+ \grNT{step\_arg} &\grRule & \grNT{symbol} \grOr
+ \textAlethe{(}\; \grNT{symbol}\; \grNT{proof\_term}\,\textAlethe{)} \\
+ \grNT{context\_annotation} &\grRule & \textAlethe{:args}\,\textAlethe{(}\,\grNT{context\_assignment}^{+}\,\textAlethe{)} \\
+ \grNT{context\_assignment} &\grRule & \textAlethe{(} \,\grNT{sorted\_var}\,\textAlethe{)} \\
+ & \grOr & \textAlethe{(:=}\, \grNT{symbol}\;\grNT{proof\_term}\,\textAlethe{)} \\
+ \end{array}
+ \]
+ \caption{The proof grammar.}
+ \label{fig:grammar}
+\end{figure}
+
+
+Usually, an Alethe proof is associated with a concrete {\smtlib} problem
+that is proved by the Alethe proof. This can either be a concrete
+problem file or, if the incremental solving commands of {\smtlib}
+are used, the implicit problem constructed at the invocation of a
+\inlineAlethe{get-proof} command.
+In this document, we will call this {\smtlib} problem the {\em input problem}.
+All symbols declared or defined in the input problem remain declared or
+defined, respectively. Furthermore, the symbolic names introduced
+by the \inlineAlethe{:named} annotation also stay valid and can be used
+in the script. For the purpose of the proof rules, terms are treated
+as if proxy names introduced by \inlineAlethe{:named} annotations have been
+expanded and annotations have been removed. For example, the term
+\inlineAlethe{(or (! (P a) :named baz) (! baz :foo))} and
+\inlineAlethe{(or (P a) (P a))} are considered to be syntactically equal.
+Here \inlineAlethe{:foo} is an arbitrary {\smtlib} annotation.
+
+Figure~\ref{fig:grammar} shows the grammar of the proof text. It
+is based on the {\smtlib} grammar, as defined in the {\smtlib}
+standard~\cite[Appendix~B]{SMTLIB}. The non-terminals
+$\grNT{attribute}$,
+$\grNT{function\_def}$,
+$\grNT{sorted\_var}$,
+$\grNT{symbol}$, and
+$\grNT{term}$
+are as defined in the standard. The non-terminal $\grNT{proof\_term}$
+corresponds to the $\grNT{term}$ non-terminal of {\smtlib}, but is
+extended with the additional production for the \inlineAlethe{choice}\index{choice} binder.
+
+Alethe proofs are a list of commands.
+The \inlineAlethe{assume} command introduces a new assumption. While this
+command could also be expressed using the \inlineAlethe{step} command with
+a special rule, the special semantic of an assumption justifies the
+presence of a dedicated command: assumptions are neither tautological nor
+derived from premises. The \inlineAlethe{step} command, on the other hand,
+introduces a derived or tautological clause. Both commands \inlineAlethe{assume}
+and \inlineAlethe{step} require an index as the first argument to later
+refer back to it. This index is an arbitrary {\smtlib} symbol.
+It must be unique for each \inlineAlethe{assume} and \inlineAlethe{step} command.
+A special restriction applies to the \inlineAlethe{assume} commands
+not within a subproof,
+those reference assertions in the input {\smtlib} problem. To simplify
+proof checking, the \inlineAlethe{assume} command must use the name assigned
+to the asserted formula if there is any. For example, if the input
+problem contains \inlineAlethe{(assert (! (P c) :named foo))}, then
+the proof must refer to this assertion (if it is needed in the proof) as
+\inlineAlethe{(assume foo (P c))}. Note that a {\smtlib} problem can
+assign a name to a term at any point, not only at its first occurrence.
+If a term has more than one name, any can be picked.
+
+The second argument of \inlineAlethe{step} and \inlineAlethe{assume}
+is the conclusion of the command.
+For a \inlineAlethe{step}, this term is always a clause.
+To express disjunctions in {\smtlib} the \inlineAlethe{or} operator is used.
+This operator, however, needs at least two arguments and cannot
+represent unary or empty clauses. To circumvent this, we introduce a new
+\inlineAlethe{cl} operator. It corresponds to the standard \inlineAlethe{or}
+function
+extended to one argument, where it is equal to the identity, and zero
+arguments, where it is equal to \inlineAlethe{false}.
+The \inlineAlethe{anchor} and \inlineAlethe{define-fun} commands are used for
+subproofs and sharing, respectively. The \inlineAlethe{define-fun} command
+corresponds exactly to the \inlineAlethe{define-fun} command of the
+{\smtlib} language.
+
+Furthermore, the syntax uses annotations as used by {\smtlib}. The
+original {\smtlib} syntax uses the non-terminal $\grNT{attribute}$.
+The Alethe syntax uses some predefined annotation. To simplify parsing,
+the order in which those must be printed is strict.
+The \inlineAlethe{:premises} annotation denotes the premises and is skipped
+if the rule does not require premises. If the rule carries arguments, the
+\inlineAlethe{:args} annotation is used to denote them.
+Anchors have two annotations: \inlineAlethe{:step} provides the name of the
+step that concludes the subproof and \inlineAlethe{:args} provides the context
+as sorted variables and assignments. Note that in this annotation,
+the $\grNT{symbol}$ non-terminal is intended to be a variable.
+After those pre-defined annotations, the solver can use additional
+annotations. This can be used for debugging, or other purposes.
+A consumer of Alethe proofs {\em must} be able to parse proofs
+that contain such annotations.
+
+\paragraph{Subproofs}
+The abstract notation denotes subproofs by marking them with a vertical
+line. To map this notation to a list of commands, Alethe \index{anchor}uses the
+\inlineAlethe{anchor} command. This command indicates the start of a subproof.
+A subproof is concluded by a matching \inlineAlethe{step} command. This step must use
+a \index{rule+concluding}{\em concluding rule}
+(such as \proofRule{subproof}, \proofRule{bind}, and so forth).
+
+After the \inlineAlethe{anchor} command, the proof uses \inlineAlethe{assume} commands to list
+the assumptions of the subproof. Subsequently, the subproof is a list of
+\inlineAlethe{step} commands that can use prior steps in the subproofs as premises.
+% the assumptions of any parent subproof
+% as premises.
+
+In the abstract notation, every step is associated with a context. The
+concrete syntax uses anchors to optimize this.
+The \index{context}context is manipulated in a nested way: if a step
+pops $c_1,\dots, c_n$ from a context $\Gamma$, there is an earlier step which
+pushes precisely $c_1,\dots, c_n$ onto the context.
+%
+Since contexts can only be manipulated by push and pop, context manipulations
+are nested. The \inlineAlethe{anchor} commands push onto the context and the
+corresponding \inlineAlethe{step} commands pop from the context.
+To indicate these changes to the context, every anchor is associated with a list
+of fixed variables and mappings.
+This list can be empty.
+
+The \inlineAlethe{:step} annotation of the anchor command is used to indicate the \inlineAlethe{step}
+command that will end the subproof. The clause of this \inlineAlethe{step}
+command is the conclusion of the subproof. While it is possible to infer the
+step that concludes a subproof from the structure of the proof, the explicit
+annotation simplifies reconstruction and makes the proof easier to read.
+If the subproof uses a
+context, the \inlineAlethe{:args} annotation of the \inlineAlethe{anchor} command
+indicates the arguments added to the context for this subproof. The
+annotation provides the sort of fixed variables.
+
+In the example proof (Figure~\ref{fig:proof_ex}) a
+subproof starts at the \inlineAlethe{anchor} command.
+It ends with the \proofRule{bind} steps that finishes the
+proof for the renaming of the bound variable \inlineAlethe{z2}
+to \inlineAlethe{vr4}.
+
+A further restriction applies: only the conclusion of a subproof can be used
+as a premise outside the subproof. Hence, a proof checking tool can
+remove the steps of the subproof from memory after checking it.
+
+\begin{example}
+\label{ex:ti:ctx-concrete}
+This example shows the proof from Example~\ref{ex:ti:ctx-abstract}
+expressed as a concrete proof.
+
+\begin{AletheVerb}
+(assume h1 (forall ((x S)) (P x)))
+(assume h2 (not (forall ((y S)) (P y))))
+(anchor :step t5 :args ((:= x y)))
+(step t3 (cl (= x y)) :rule refl)
+(step t4 (cl (= (P x) (P y))) :rule cong :premises (t3))
+(step t5 (cl (= (forall ((x S)) (P x)) (forall ((y S)) (P y))))
+ :rule bind)
+(step t6 (cl (= (forall ((x S)) (P x)) (forall ((y S)) (P y)))
+ (not (forall ((x S)) (P x)))
+ (forall ((y S)) (P y)))) :rule equiv_pos2)
+(step t7 (cl) :rule resolution :premises (h1 h2 t5 t6))
+\end{AletheVerb}
+\end{example}
+
+\tikzset{
+ solver/.style={draw, thin},
+ system/.style={draw, thin, rounded corners},
+}
+
+ \begin{figure}[t]
+\center
+\begin{tikzpicture}[node distance=2cm, auto,>=latex', thick,scale=0.8]
+ \node[solver] (unsat) {\textsf{Unsat mode}};
+ \node[system, right=of unsat] (assume) {\textsf{Assumptions}};
+ \path[->] (unsat) edge[bend left] node[font=\scriptsize] {\texttt{get-proof}} (assume);
+ \path[->] (assume) edge[loop above] node[align=center,font=\scriptsize] {\inlineAlethe{assume},\\\inlineAlethe{define-fun},\\\inlineAlethe{anchor}} (assume);
+ \node[system, right=of assume] (step) {\textsf{Steps}};
+ \path[->] (assume) edge[bend left] node[font=\scriptsize] {\inlineAlethe{step}} (step);
+ \path[->] (step) edge[loop above] node[align=center,font=\scriptsize] {\inlineAlethe{step},\\ \inlineAlethe{define-fun}} (step);
+ \path[->] (step) edge[above, bend left] node[font=\scriptsize] {\inlineAlethe{anchor}} (assume);
+ \path[->] (step) edge[above, bend left] node[font=\scriptsize] {\textsf{Last step}} (unsat);
+\end{tikzpicture}
+\label{fig:proof-states}\caption{Abstract view of the transitions in an Alethe proof.}
+\end{figure}
+
+
+\paragraph{Alethe Proof Printing States}
+Figure~\ref{fig:proof-states} shows the states of an Alethe proof
+abstractly. To generate a proof, the SMT solver must be in the
+{\em Unsat mode}, i.e., the solver determined that the problem
+is unsatisfiable. The {\smtlib} problem script then requests the proof by
+invoking the \inlineAlethe{get-proof} command. It is possible that this command
+fails. For example, if proof production was not activated up front.
+If there is no error, the proof is printed and printing starts with
+the assumptions. The solver prints the proof as a list of commands
+according to the state. The states ensure one constraint is maintained:
+assumptions can only appear at either the beginning of a proof or right
+after a subproof is started by the \inlineAlethe{anchor} command. They cannot
+be mixed with ordinary proof steps. This simplifies
+reconstruction. Each assumption printed at the beginning of the proof
+corresponds to assertions in the input problem, up to symmetry of equality.
+Proof printing concludes after the last step is printed and the solver
+returns to the Unsat mode and the user can issue further commands.
+Usually the last step is an outermost step
+(i.e., not within a subproof) that concludes the proof by deriving
+the empty clause, but this is not necessary.
+The solver is allowed to print some additional, useless,
+steps after the proof is concluded.
+
+
+\paragraph{Sharing and Skolem Terms}
+Usually, SMT solvers store terms internally in an efficient manner. A term data
+structure with perfect sharing ensures that every term is stored in memory
+precisely once. When printing the proof, this compact storage is unfolded.
+This leads to a blowup of the proof size.
+
+Alethe can optionally use sharing\footnote{For {\verit} this can be activated
+by the command-line option \Verb{--proof-with-sharing}.} to print common
+subterms only once. This is realized using the standard naming mechanism
+of {\smtlib}. A term $t$ is annotated with a name $n$ by writing
+\inlineAlethe{(!}\,$t$\,\inlineAlethe{:named}\;$n$\,\inlineAlethe{)}
+where $n$ is a symbol. After a term is annotated with a name, the name can
+be used in place of the term. This is a purely syntactical replacement.
+Alethe continues to use the names already used in the input problem.
+Hence, terms that already have a name in the input problem can be replaced
+by that name and new names introduced in the proof must not use names
+already used in the input problem.
+
+To limit the number of names, an SMT solver can use the following
+simple approach used by {\verit}.
+Before printing the proof, it iterates over all terms of the proof and
+recursively descend into the terms. It marks every unmarked subterm it
+visits. If a visited term is already marked, the solver assigns a new name
+to this term. If a term already has a name, it does not descend further
+into the term.
+%
+By doing so, it ensures that only terms that appear as
+child of two different parent terms get a name. Since a named term
+is replaced with its name after it first appearance, a term that only
+appears as a child of one single term does not need a distinct name.
+%
+Thanks to the perfect
+sharing representation, testing if a term is marked takes constant time
+and the overall traversal takes linear time in the proof size.
+
+To simplify reconstruction, Alethe can optionally\footnote{For {\verit} by
+using the command-line option \Verb{--proof-define-skolems}.} define
+Skolem constants as functions. In this case, the proof contains a list
+of \inlineAlethe{define-fun} commands that define shorthand 0-ary functions for
+the \inlineAlethe{(choice }\dots\inlineAlethe{)} terms needed. Without this option,
+no \inlineAlethe{define-fun} commands are issued, and the constants are expanded.
+
+\paragraph{Implicit Transformations}
+Overall, the following aspects are treated implicitly by Alethe.
+\begin{itemize}
+ \item Symmetry of equalities that are not top-most equalities in steps with
+ non-empty context.
+ \item The order of literals in the clauses.
+ \item The unfolding of names introduced by
+ \inlineAlethe{(!}\,$t$\,\inlineAlethe{:named }\;$s$\,\inlineAlethe{)}.
+ \item The removal of other {\smtlib} annotations of the form
+ \inlineAlethe{(!}\,$t$\,\dots\,\inlineAlethe{)}.
+ \item The unfolding of function symbols introduced by
+ \inlineAlethe{define-fun}.\footnote{For {\verit} this is only used when the user
+ introduces {\verit} to print Skolem terms as defined functions. User defined
+ functions in the input problem are not supported by {\verit} in proof production
+ mode.}
+\end{itemize}
+
+Alethe proofs contain steps for other aspects that are commonly left implicit, such
+as renaming of bound variables, and the application of substitutions.
+
+\section{Checking Alethe Proofs}
+\label{sec:alethe:semantic}
+
+In this section we present an abstract procedure to check if an Alethe
+proof is \index{well-formed}well-formed and valid. An Alethe proof is
+well-formed only if its anchors and steps are balanced. To check that
+this is the case, we replace innermost subproofs by holes until there is
+no subproof left. If the resulting proof is free of anchors and steps
+that use concluding rules, then the proof is well-formed.
+If all the steps in the subproofs adhere to the conditions of
+their rules, the subproof is valid. If all subproofs are valid,
+then the entire proof is valid.
+
+Formally, an Alethe proof $P$ is a list $[C_1, \dots, C_n]$ of steps
+and anchors.
+Since every step uses an unique index, we assume that each step
+$C_i$ in $P$ uses $i$ as its index.
+The context
+only changes at anchors and subproof-concluding steps.
+Therefore, the elements of $C_1, \dots, C_n$ that are steps
+are not associated with a context.
+Instead, the context can be computed
+from the prior anchors.
+The anchors only ever extends the context.
+
+To check an Alethe proof we can iteratively eliminate the first-innermost
+subproof, i.e., the innermost subproof that does not come after a
+complete subproof. The restriction to the first subproofs simplifies
+the calculation of the context of the steps in the subproof.
+
+\begin{definition}[First-Innermost Subproof]
+ Let $P$\, be the proof $[C_1, \dots, C_n]$ and $1 \leq \mathit{start}
+ < \mathit{end} \leq n$ be two indices such that
+ \begin{itemize}
+ \item $C_{\mathit{start}}$ is an anchor,
+ \item $C_{\mathit{end}}$ is a step that uses a concluding rule,
+ \item no $C_k$ with $k < \mathit{start}$ uses a concluding rule,
+ \item no $C_k$ with $\mathit{start} < k < \mathit{end}$ is an anchor or
+ a step that uses a concluding rule.
+ \end{itemize}
+ Then $[C_{\mathit{start}}, \dots, C_{\mathit{end}}]$ is the
+ \index{subproof+first-innermost}first-innermost subproof of $P$.
+\end{definition}
+
+\begin{example}
+The proof in Example~\ref{ex:ti:ctx-concrete} has only one subproof
+and this subproof is also a first-innermost subproof. It is the subproof
+\begin{AletheVerb}
+(anchor :step t5 :args ((:= x y)))
+(step t3 (cl (= x y)) :rule refl)
+(step t4 (cl (= (P x) (P y))) :rule cong :premises (t3))
+(step t5 (cl (= (forall ((x S)) (P x)) (forall ((y S)) (P y))))
+ :rule bind)
+\end{AletheVerb}
+\end{example}
+
+\noindent
+It is easy to calculate the context of the first-innermost subproof.
+
+\begin{definition}[Calculated Context]
+ Let $[C_{\mathit{start}}, \dots, C_{\mathit{end}}]$ be
+ the first-innermost subproof of $P$.
+ For $\mathit{start} \leq i < \mathit{end}$, let
+ $A_1, \dots, A_m$ be the anchors among $C_1, \dots, C_{i-1}$.
+
+ The \index{context+calculated}calculated context of $C_i$ is the context
+ \[
+ c_{1,1}, \dots, c_{1, n_1}, \dots, c_{m,1}, \dots, c_{m, n_m}
+ \]
+ where $c_{k,1}, \dots, c_{k, n_k}$ is the list of fixed variables
+ and mappings associated with $A_k$.
+\end{definition}
+
+Note that if $C_i$ is an anchor, its calculated context does not
+contain the elements associated with $C_i$.
+Therefore, the context of $C_{\mathit{start}}$
+is the context of the steps before the subproof.
+Furthermore, the step $C_{\mathit{end}}$ is the concluding
+step of the subproof and must have the same context as the steps surrounding
+the subproof.
+Hence, the context of $C_{\mathit{end}}$ is the calculated
+context of $C_{\mathit{start}}$.
+
+\begin{example}
+The calculated context of the steps \texttt{\color{SmtStepId}t3} and \texttt{\color{SmtStepId}t5} in
+Example~\ref{ex:ti:ctx-concrete} is the context $x \mapsto y$.
+The calculated context of the concluding step \texttt{\color{SmtStepId}t5} and the anchor is empty.
+\end{example}
+
+\noindent
+A first-innermost subproof is valid if all its steps adhere to
+the conditions of their rule and only use premises that occur in front of them
+in the subproof. The conditions of each rule are listed in
+Section~\ref{apx:rules}.
+
+\begin{definition}[Valid First-Innermost Subproof]
+ Let $[C_{\mathit{start}}, \dots, C_{\mathit{end}}]$
+ be the first-innermost subproof of $P$.
+ The subproof is \index{subproof+valid}{\em valid} if
+ \begin{itemize}
+ \item all steps $C_i$ with $\mathit{start} < i <
+ \mathit{end}$ only use premises $C_j$ with $\mathit{start} <
+ j < i$,
+ \item all $C_i$ that are steps adhere to the conditions of their
+ rule under the calculated context of $C_i$,
+ \item the step $C_{\mathit{end}}$
+ adheres to the conditions of its
+ rule under the calculated context of $C_{\mathit{start}}$.
+ \end{itemize}
+\end{definition}
+
+Since the \proofRule{assume} rule expects an empty context, an admissible
+subproof can contain assumptions only if the rule used by $C_{\mathit{end}}$
+is the \proofRule{subproof} rule.
+
+To eliminate a subproof we can replace the subproof with a hole that has
+at its conclusion the conclusion of the subproof. This is safe as long
+as the subproof that is eliminated is valid (see Section~\ref{sec:alethe:soundness-eh}).
+
+\begin{definition}
+The function $E$ eliminates the first-innermost subproof from a proof
+if there is one.
+Let $P$ be a proof $[C_1, \dots C_n]$.
+Then $E(P) = P$ if $P$ has no first-innermost subproof.
+Otherwise, $P$ has the first-innermost subproof
+$[C_{\mathit{start}}, \dots, C_{\mathit{end}}]$, and
+$E(P) = [C_1, \dots, C_{\mathit{start}-1}, C', C_{\mathit{end}+1},
+\dots, C_n]$ where $C'$ is a new step that uses the \proofRule{hole} rule
+and has the index, conclusion, and premises of $C_{\mathit{end}}$.
+\end{definition}
+
+It is important to add the premises of $C_{\mathit{end}}$
+to $C'$. The \proofRule{let} rule can use additional premises
+and omitting those premises results in an unsound step.
+We can apply $E$ iteratively to a proof $P$ until we reach the least fixed point.
+Since $P$ is finite we will always reach a fixed point in finitely many steps.
+The result is a list $[P_0, P_1, P_2, \dots, P_{\mathit{last}}]$ where $P_0 = P$,
+$P_1 = E(P)$, $P_2 = E(E(P))$ and $P_{\mathit{last}} = E(P_{\mathit{last}})$.
+
+\begin{example}
+Applying $E$\, to the proof in
+Example~\ref{ex:ti:ctx-concrete} gives us the proof
+
+\begin{AletheVerb}
+(assume h1 (forall ((x S)) (P x)))
+(assume h2 (not (forall ((y S)) (P y))))
+(step t5 (cl (= (forall ((x S)) (P x)) (forall ((y S)) (P y))))
+ :rule hole)
+(step t6 (cl (= (forall ((x S)) (P x)) (forall ((y S)) (P y)))
+ (not (forall ((x S)) (P x)))
+ (forall ((y S)) (P y)))) :rule equiv_pos2)
+(step t7 (cl) :rule resolution :premises (h1 h2 t5 t6))
+\end{AletheVerb}
+
+Since this proof contains no subproof, it is also $P_{\mathit{last}}$.
+\end{example}
+
+
+\begin{definition}[Well-Formed Proof]
+ \label{def:well_formed_proof}
+ The Alethe proof $P$ is \index{proof+well-formed}well-formed
+ if every step uses a unique index and $P_{\mathit{last}}$
+ contains no anchor or step that uses a concluding rule.
+\end{definition}
+
+\begin{definition}[Valid Alethe Proof]
+ The proof $P$ is a \index{proof+valid}{\em valid Alethe proof} if
+ \begin{itemize}
+ \item $P$\, is well-formed,
+ \item $P$\, does not contain any step that uses the \proofRule{hole} rule,
+ \item $P_{\mathit{last}}$ contains a step that has the empty clause as its conclusion,
+ \item the first-innermost subproof of every $P_i$, $i < \mathit{last}$ is valid,
+ \item all steps $C_i$ in $P_{\mathit{last}}$ only use premises
+ $C_j$ in $P_{\mathit{last}}$ with $1 \leq j < i$,
+ \item all steps $C_i$ in $P_{\mathit{last}}$ adhere to the conditions of their
+ rule under the empty context.
+ \end{itemize}
+\end{definition}
+
+The condition that $P$ contains no hole ensures that the original
+proof is complete and holes are only introduced by eliminating valid
+subproofs.
+
+\begin{example}
+The proof in Example~\ref{ex:ti:ctx-concrete} is valid. The only
+subproof is valid, the proof contains no hole, and $P_{\mathit{last}}$
+contains the step \textsf{\color{SmtStepId} t7} that concludes with the empty clause.
+\end{example}
+
+It is sometimes useful to speak about the steps that are not within a
+subproof. We call such a step an \index{step+outermost}{\em outermost
+step}. In a well-formed proof those are the steps
+of $P_{\mathit{last}}$.
+
+\subsection{Contexts and Metaterms}
+
+We now direct our attention to subproofs with \index{context}contexts.
+It is useful to give a precise semantic
+to contexts to have the tools to check that rules that use contexts
+are sound.
+Contexts are local in the sense that they affect only the
+proof step they are applied to.
+For the full details on contexts see~\cite{barbosa-2019}.
+The presentation here is adapted from this publication, but omits some
+details.
+
+To handle subproofs with contexts, we translate the contexts into
+λ-terms.
+%
+This allows us to
+leverage the \index{lambda calculus}λ-calculus as an existing well-understood theory of \index{binder}binders.
+%
+These λ-terms\index{term+lambda} are called \index{term+meta}\index{metaterms}{\em metaterms}.
+
+\begin{definition}[Metaterm]
+ Metaterms are expressions constructed by the grammar
+ \[
+ M \,::=\, \groundbox{$t$}\,\mid\, \lambda x.\,M\,\mid\,(\lambda \bar{x}_n.\,
+ M)\,\bar{t}_n
+ \]
+where $t$ is an ordinary term and $t_i$ and $x_i$ have matching sorts for
+all $0 \leq i \leq 1$.
+\end{definition}
+
+According to this definition, a metaterm is either a boxed term, a
+\index{abstraction+lambda}λ-abstraction, or an application to an uncurried λ-term.
+The annotation $\groundbox{$t$}$ delimits terms from the context, a simple
+λ-abstraction is used to express fixed variables, and the
+application expresses simulations substitution of $n$ terms.\footnote{
+ The box annotation used here is unrelated to the boxes
+ within the SMT solver discussed in the introduction.}
+
+We use $=_{\alpha\beta}$ to denote syntactic equivalence modulo
+α-equivalence and β-reduction.
+
+Proof steps with contexts can be encoded into proof steps with empty
+contexts, but with metaterms. A proof step
+
+\begin{AletheS}
+i. & $\Gamma$ & \ctxsep & $t ≈ u$ & $(\ruleType{rule}\; \bar{p}_n)\;[\bar{a}_m]$ \\
+\end{AletheS}
+
+\noindent
+is encoded into
+
+\begin{AletheS}
+i. & & \ctxsep & $L(\Gamma)[t] \simeq R(\Gamma)[u]$ & $(\ruleType{rule}\; \bar{p}_n)\;[\bar{a}_m]$ \\
+\end{AletheS}
+
+\noindent
+where
+\begin{align*}
+ L(\emptyset)[t] &= \groundbox{t} & R(\emptyset)[u] &= \groundbox{u} \\
+ L(x, \bar{c}_m)[t] &= \lambda x.\,L(\bar{c}_m)[t] & R(x, \bar{c}_m)[u] &= \lambda x.\,R(\bar{c}_m)[u] \\
+ L(\bar{x}_n\mapsto\bar{s}_n, \bar{c}_m)[t] &= (\lambda \bar{x}_n.\,L(\bar{c}_m)[t]) \bar{s}_n
+ & R(\bar{x}_n\mapsto\bar{s}_n, \bar{c}_m)[u] &= R(\bar{c}_m)[u] \\
+\end{align*}
+
+To achieve the same effect as using the $\subst()$ function described above, we
+can translate the terms into metaterms, perform β-reduction, and rename
+bound variables if necessary~\cite[Lemma~11]{barbosa-2019}.
+
+\begin{example}
+The example on page~\pageref{ex:alethe:substctx} becomes
+\begin{flalign*}
+\quad & L(x\mapsto 7, x \mapsto g(x))[x] = (\lambda x.\,(\lambda x.\,\groundbox{x})\,(g(x)))\, 7
+=_{\alpha\beta} \groundbox{g(7)} &\\
+& L(x\mapsto 7, x, x \mapsto g(x))[x] = (\lambda x.\,\lambda x.\,(\lambda x.\,\groundbox{x})\,(g(x)))\, 7
+=_{\alpha\beta} \lambda x.\,\groundbox{g(x)}
+\end{flalign*}
+\end{example}
+
+Most proof rules that operate with contexts can easily be translated into
+proof rules using metaterms. The exception are the tautologous rules,
+such as \proofRule{refl} and the $\cdots{}${\ruleType{_simplify}} rules.
+
+Steps that use such rules always encode a judgment
+$\vDash \Gamma\,\vartriangleright\,t ≈ u$. With the encoding described above
+we get $L(\Gamma)[t] ≈ R(\Gamma)[u]
+=_{\alpha\beta} \lambda \bar{x}_n.\,\groundbox{t'} ≈
+\lambda \bar{x}_n.\,\groundbox{u'}$ with some terms $t'$, $u'$.
+To handle those terms, we use the $\reify()$ function.
+This function is defined as
+\[
+\reify(\lambda \bar{x}_n.\,\groundbox{t} ≈
+\lambda \bar{x}_n.\,\groundbox{u}) = \forall \bar{x}_n.\,(t ≈ u).
+\]
+Therefore,
+all tautological rules with contexts represent a judgment\\
+$\vDash \reify(T ≈ U)$
+where $T =_{\alpha\beta} L(\Gamma)[t]$ and $U =_{\alpha\beta} R(\Gamma)[u]$.
+
+\begin{example}
+ Consider the step
+
+\begin{AletheS}
+i. & $y, x \mapsto y$ & \ctxsep
+& $x + 0 ≈ y$ & $\proofRule{sum_simplify}$ \\
+\end{AletheS}
+
+\noindent
+Translating the context into metaterms leads to
+
+\begin{AletheS}
+i. & \phantom{$y, x \mapsto y$} & \ctxsep
+& $(\lambda y.\,(\lambda x.\,\groundbox{$x + 0$})\, y) ≈
+ (\lambda y.\,\groundbox{$y$})$ & $\proofRule{sum_simplify}$ \\
+\end{AletheS}
+
+\noindent
+Applying β-reduction leads to
+
+\begin{AletheS}
+i. & \phantom{$y, x \mapsto y$} & \ctxsep
+& $(\lambda y.\,\groundbox{$y + 0$}) ≈
+ (\lambda y.\,\groundbox{$y$}) $ & $\proofRule{sum_simplify}$ \\
+\end{AletheS}
+
+\noindent
+Finally, using $\reify()$ leads to
+
+\begin{AletheS}
+i. & \phantom{$y, x \mapsto y$} & \ctxsep
+& $\forall y.\,(y + 0 ≈ y)$ & $\proofRule{sum_simplify}$ \\
+\end{AletheS}
+
+\noindent
+This obviously holds in the theory of linear arithmetic.
+\end{example}
+
+\subsection{Soundness}
+\label{sec:alethe:soundness-eh}
+
+Any proof calculus should be sound. In the case of Alethe, most proof
+rules are
+standard rules, or simple tautologies. The rules that use context
+are unusual, but those proof rules were previously shown to be
+sound~\cite{barbosa-2019}.
+Alethe does not use any rules that are merely satisfiability preserving.
+The skolemization rules replace the bound variables with choice terms
+instead of fresh symbols.\footnote{The \inlineAlethe{define-fun} function
+can introduce fresh symbols, but we will assume here that those
+commands have been eliminated by unfolding the definition.}
+All Alethe rules express semantic implications.
+Overall, we assume in this document that the proof rules and proofs
+written in the abstract notation are sound.
+
+Nevertheless, a modest gap remains. The concrete, command-based
+syntax does not precisely correspond to the abstract notation.
+In this section we will address the soundness of concrete Alethe
+proofs.
+
+\begin{theorem}[Soundness of Concrete Alethe Proofs]
+ \label{thm:sound}
+ If there is a valid Alethe proof $P = [C_1, \dots, C_n]$ that has the formulas
+ $\varphi_1, \dots, \varphi_m$ as the conclusions of the outermost \proofRule{assume}
+ steps, then
+ \[
+ \varphi_1, \dots, \varphi_m \vDash \bot.
+ \]
+\end{theorem}
+
+Here, $\vDash$ represents
+semantic consequence in the many-sorted first order logic of {\smtlib}
+with the theories of uninterpreted functions and linear arithmetic extended
+to clauses.
+
+To show the soundness of a valid Alethe proof $P = [C_1, \dots, C_n]$,
+we can use the same approach as for the definition of validity: consider
+first-innermost subproof first and then replace them by holes.
+%
+Since valid proofs do not contain holes, we have to generalize the induction
+to allow holes that were introduced by the elimination of subproofs.
+%
+We start with simple subproofs with empty contexts and without
+nested subproofs.
+
+\begin{lemma}
+ \label{lem:sound_subproof}
+ Let $P$\, be a proof that contains a valid first-innermost subproof where
+ $C_{\mathit{end}}$ is a \proofRule{subproof} step. Let
+ $\psi$ be the conclusion of $C_{\mathit{end}}$.
+ Then $\vDash \psi$ holds.
+\end{lemma}
+\begin{proof}
+ First, we use induction on the number of steps $n$ after
+ $C_{\mathit{start}}$. Let $\psi_n$ be the conclusion
+ of $C_{\mathit{start}+n}$ and $V_n$ the conclusions of
+ the \proofRule{assume} steps in $[C_{\mathit{start}}, \dots,
+ C_{\mathit{start}+n}]$.
+ Assumptions always introduce unit clauses. We will identify
+ unit clauses with their single literal.
+ We will
+ show $V_n \vDash \psi_n$ if $\mathit{start}+n < \mathit{end}$.
+
+ If $n = 1$, then $C_{\mathit{start}+n} = C_{\mathit{start}+1}$ must
+ either be a tautology, or an \proofRule{assume} step. In the first case,
+ $\vDash \psi_{\mathit{start}+1}$ holds, and in the second case
+ $\psi_{\mathit{start}+1} \vDash \psi_{\mathit{start}+1}$ holds.
+
+ For subsequent $n$, $C_{\mathit{start}+n}$ is
+ either an ordinary step, or an \proofRule{assume} step. In the second case,
+ $\psi_{\mathit{start}+n} \vDash \psi_{\mathit{start}+n}$ which can
+ be weakened to $V_n \vDash \psi_{\mathit{start}+n}$.
+ In the first case, the step $C_{\mathit{start}+n}$ has a set of
+ premises $S$.
+ For each step $C_{\mathit{start}+i} \in S$ we have $i < n$ and
+ $V_i \vDash \psi_{\mathit{start}+i}$ due to the induction
+ hypothesis. Since $i < n$, the premises $V_i$ are a subset of $V_n$ and
+ we can weaken $V_i \vDash \psi_{\mathit{start}+i}$
+ to $V_n \vDash \psi_{\mathit{start}+i}$. Since all premises of
+ $C_{\mathit{start}+n}$ are the consequence of $V_n$ we get
+ $V_n \vDash \psi_n$.
+
+ The step $C_{\mathit{end}-1}$ is the last step of the subproof that
+ does not use a concluding rule.
+ At this step we have $V_{\mathit{end}-1} \vDash \psi_{\mathit{end}-1}$.
+ Since $C_{\mathit{end}}$ is not an \proofRule{assume} step, the
+ set $V_{\mathit{end}-1} = \{\varphi_1, \dots, \varphi_m\}$ contains
+ all assumptions in the subproof.
+ By the deduction theorem we get
+ \[
+ \vDash \varphi_1 \land \cdots \land \varphi_m → \psi_{\mathit{end}-1}.
+ \]
+ This can be transformed into the clause
+ \[
+ \vDash \neg\varphi_1, \cdots, \neg\varphi_m, l_1, \dots, l_o.
+ \]
+ where $l_1, \dots, l_o$ are the literals of $\psi_{\mathit{end}-1}$.
+ This clause is exactly the conclusion of the
+ step $C_{\mathit{end}}$
+ according to the definition of the \proofRule{subproof} rule.
+\end{proof}
+
+\noindent
+We can do the same reasoning as for Lemma~\ref{lem:sound_subproof} for
+subproofs with contexts. This is slightly complicated by the
+\proofRule{let} rule that can use extra premises.
+
+\begin{lemma}\label{lem:sound_subproof_context}
+ Let $P$ be a proof that contains a
+ valid first-innermost subproof where
+ $C_{\mathit{end}}$ is a step using one of:
+ \proofRule{bind}, \proofRule{sko_ex}, \proofRule{sko_forall},
+ \proofRule{onepoint}, \proofRule{let}.
+
+ Then $V \vDash \Gamma \vartriangleright \psi$ where $\Gamma$ is the
+ calculated context of $C_{\mathit{start}}$ and $\psi$ is the conclusion
+ of $C_{\mathit{end}}$. The set $V$\, is empty if $C_{\mathit{end}}$
+ does not use the \proofRule{let} rule. Otherwise, it contains all
+ conclusions of the
+ \proofRule{assume} steps among $[C_{δ}, \dots,
+ C_{\mathit{start}}]$ where $δ$ is either the largest index
+ $δ < {\mathit{start}}$ such
+ that $s_{δ}$ is an anchor, or $1$ if no such index exist.
+ Hence, there is no anchor between $C_{δ}$ and $C_{\mathit{start}}$.
+\end{lemma}
+\begin{proof}
+ The step $C_{\mathit{start}}$ is an anchor due to the definition
+ of innermost-first subproof.
+ Let $c_1, \dots, c_n$ be the context introduced by the anchor
+ $C_{\mathit{start}}$, and let $\Gamma$ be the calculated context
+ of $C_{\mathit{start}}$.
+ $\Gamma' = \Gamma, c_1, \dots, c_n$.
+ is the calculated context of the steps in the subproof after
+ $C_{\mathit{start}}$.
+
+ The step $C_{\mathit{end}}$ is a step
+
+\begin{AletheS}
+& \spctx{} & & \cdots & \\
+$\mathit{end}-1$. & \spctx{} $\Gamma'$ & \ctxsep
+& $\,\psi'$ & $(\dots)$ \\
+\spsep
+$\mathit{end}$. & $\Gamma$ & \ctxsep & $\psi$ & $(\ruleType{rule}\;i_1, \dots, i_n)$ \\
+\end{AletheS}
+
+ Since we assume the step $C_{\mathit{end}}$ is correctly employed,
+ $\vDash \Gamma \vartriangleright \psi$ holds, as long as
+ $\vDash \Gamma' \vartriangleright \psi'$ holds.
+
+ We perform the same induction as for
+ Lemma~\ref{lem:sound_subproof} over the steps in
+ $[C_{\mathit{start}}, \dots, C_{\mathit{end}}]$.
+ %
+ Since $C_{\mathit{end}}$ does not use the \proofRule{subproof} rule,
+ the subproof does not contain any assumptions and
+ $V_i$ stays empty.
+ %
+ Again, we are interested in the step $C_{\mathit{end}-1}$. At this step we
+ get $\vDash \Gamma' \vartriangleright \psi'$.
+
+ Only the \proofRule{let} rule uses additional premises
+ $C_{i_1}, \dots, C_{i_n}$. Hence, for all other rules, the conclusion
+ cannot depend on any step outside the subproof and $V$\, is empty.
+ % TODO: this is ugly, let is ugly
+ Due to the definition of first-innermost subproof, all steps $C_{i_1},
+ \dots, C_{i_n}$ are in the same subproof that starts at $C_{δ}$.
+
+ The steps $C_{i_1}, \dots, C_{i_n}$ might
+ depend on some \proofRule{assume} steps that appear before them
+ in their subproof. This is the case if the steps are outermost steps, or
+ if the subproof that starts at $C_{δ}$ concludes with
+ a \proofRule{subproof} step.
+ %
+ In this case we can, as we saw in the proof of
+ Lemma~\ref{lem:sound_subproof}, weaken their judgments to include
+ all assumptions in $[C_{δ}, \dots, C_{\mathit{start}}]$.
+
+ If the subproof that starts at $C_{δ}$ concludes with
+ any other rule, then there cannot be any assumptions and $V$\, is empty.
+\end{proof}
+
+By using Lemma~\ref{lem:sound_subproof} and
+Lemma~\ref{lem:sound_subproof_context} we can now show that
+a valid, concrete Alethe proof is sound. That is, we can show
+Theorem~\ref{thm:sound}.
+
+\begin{proof}
+ Since $P =[C_1, \dots, C_n]$ is valid, all steps that do not use the
+ \proofRule{hole} rule adhere to their rule. Since we assume that the
+ abstract notation and the rules are sound, we only have to
+ worry about the steps using the \proofRule{hole} rule.
+ Those should be sound, i.e., for a \proofRule{hole} step with the conclusion
+ $\psi$, premises $V$, and context $\Gamma$
+ the judgment $V \vDash \Gamma \vartriangleright \psi$ must hold.
+
+ Since $P$\, is a valid proof there is a sequence
+ $[P_0, \dots, P_{\mathit{last}}]$ as discussed in Section~\ref{sec:alethe:semantic}.
+ For $i < \mathit{last}$, $E(P_i) = P_{i+1}$ replaces the
+ first-innermost subproof in $P_i$ by a hole with the conclusion
+ $\psi$. Furthermore, the context of the introduced hole
+ corresponds to the context $\Gamma$ of the start of the subproof.
+ Since $P$ is a valid proof, the first-innermost subproof eliminated by $E$ is
+ always valid.
+ Therefore,
+ we can apply Lemma~\ref{lem:sound_subproof}
+ or Lemma~\ref{lem:sound_subproof_context} to conclude that the hole introduced
+ by $E$ is sound.
+
+ Since $P_0$ does not contain any holes, the holes in each proof
+ $P_i$ are all introduced by innermost-first subproof elimination.
+ Therefore, they are sound. In consequence, all holes in $P_{\mathit{last}}$ are
+ sound and we can perform the same
+ argument as
+ in the proof of Lemma~\ref{lem:sound_subproof} to the proof
+ $P_{\mathit{last}}$.
+
+ Let $j$ be the index of the step in $P_{\mathit{last}}$ that concludes
+ with the empty clause.
+ Let $\mathit{start} = 1$
+ and $\mathit{end} = j$ in the argument of Lemma~\ref{lem:sound_subproof}.
+ This shows that $V \vDash \bot$, where $V$ is the
+ conclusion of the \proofRule{assume} steps in the sublist $[C_1, \dots, C_j]$
+ of $P_{\mathit{last}}$. We can weaken
+ this by adding the conclusions of the \proofRule{assume} steps in
+ $[C_j, \dots, C_n]$ of $P_{\mathit{last}}$
+ to get $\varphi_1, \dots, \varphi_m \vDash \bot$.
+\end{proof}
+
+
+\section{The Alethe Rules}
+\label{sec:alethe:rules-generic}
+
+Together with the language, the Alethe format also includes a set
+of proof rule.
+Section~\ref{apx:rules}
+gives a full list of all
+proof rules. Currently, the proof rules correspond to the rules
+that the solver {\verit} can emit. For the rest of this section, we will discuss some
+general concepts related to the rules.
+
+\paragraph{Tautologous Rules and Simple Deduction.}
+Most rules introduce tautologies. One example is
+the \proofRule{and_pos} rule: $\neg (\varphi_1 \land \varphi_2 \land
+\dots \land \varphi_n), \varphi_i$.
+%
+Other rules derive their conclusion from a single premise.
+%
+Those rules are primarily used to simplify Boolean
+connectives during preprocessing. For example, the \proofRule{implies}
+rule eliminates an implication: From $\varphi_1 → \varphi_2$,
+it deduces $\neg \varphi_1, \varphi_2$.
+
+
+\paragraph{Resolution.}
+{\cdclt}-based SMT solvers, and especially their {\sat} solvers,
+are fundamentally based on resolution of clauses.
+Hence, Alethe also has dedicated clauses and a resolution proof
+rule. However, since SMT solvers do not enforce a strict
+clausal normal form, ordinary disjunction is also used.
+Keeping clauses and disjunctions distinct simplifies rule checking.
+For example, in the case of
+resolution there is a clear distinction between unit clauses where
+the sole literal starts with a disjunction and non-unit clauses. The
+syntax for clauses uses the \inlineAlethe{cl} operator, while disjunctions
+use the standard {\smtlib} \inlineAlethe{or} operator. The \proofRule{or}
+\emph{rule} is responsible for converting disjunctions into clauses.
+
+The Alethe proofs use a generalized propositional
+resolution rule with the name \proofRule{resolution} or
+\proofRule{th_resolution}. Both names denote the same rule. The
+difference only serves to distinguish if the rule was introduced by
+the {\sat} solver or by a theory solver. The resolution step is purely
+propositional; there is no notion of a unifier. The resolution
+rules also implicitly simplifies repeated negations at the head
+of literals.
+
+The premises of a resolution step are clauses, and the conclusion
+is a clause that has been derived from the premises by some binary
+resolution steps.
+
+\paragraph[reference=rule:forall_inst,title={Quantifier Instantiation.}]
+To express quantifier instantiation, the rule \proofRule{forall_inst}
+is used. It produces a formula of the form $(\neg \forall \bar
+x_n.\,\varphi) \lor \varphi[\bar t_n]$, where $\varphi$ is
+a term containing the free variables $\bar x_n$, and for each $i$ the
+ground term $t_i$ is a new term with the same sort as $x_i$.\footnote{
+ For historical reasons, \proofRule{forall} has a unit clause with a disjunction
+ as its conclusion and not the clause $(\neg \forall \bar x_n.\,\varphi), \varphi[\bar t_n]$.
+}
+
+The arguments of a \proofRule{forall_inst} step is the list $(x_1 , t_1),
+\dots, (x_n, t_n)$. While this information can be recovered from the term,
+providing it explicitly helps reconstruction because the implicit reordering of
+equalities obscures which terms have been used as instances.
+Existential quantifiers are handled by skolemization.
+
+
+\paragraph{Linear Arithmetic.}
+Proofs for linear arithmetic use a number of straightforward rules,
+such as \proofRule{la_totality} ($t_1 \leq t_2 \lor t_2 \leq t_1$)\footnote{
+ This rule also has a unit clause with a disjunction as its conclusion.}
+and the main rule \proofRule{la_generic}. The conclusion of an
+\proofRule{la_generic} step is a tautology $\neg \varphi_1, \neg
+\varphi_2, \dots, \neg \varphi_n$ where the $\varphi_i$ are linear
+(in)equalities. Checking the validity of this clause amounts to
+checking the unsatisfiability of the system of linear equations
+$\varphi_1, \varphi_2, \dots, \varphi_n$. The annotation of an
+\proofRule{la_generic} step contains a coefficient for each (in)equality.
+The result of forming the linear combination of the literals with
+the coefficients is a trivial inequality between constants.
+
+\begin{example}
+The following example is the proof for the unsatisfiability
+of $(x+y<1) \lor$ $(3<x)$, $x≈ 2$, and $0≈ y$.
+
+\begin{Alethe}
+1.& \ctxsep & $(3 < x) \lor (x + y < 1) $ & $ \proofRule{assume}$ \\
+2.& \ctxsep & $x≈ 2 $ & $ \proofRule{assume}$ \\
+3.& \ctxsep & $0≈ y $ & $ \proofRule{assume}$ \\
+4.& \ctxsep & $(3 < x), (x + y < 1) $ & $ (\proofRule{or}\,1)$ \\
+5.& \ctxsep & $\neg (3<x), \neg (x≈ 2) $ & $ \proofRule{la_generic}\, [1.0, 1.0]$ \\
+6.& \ctxsep & $\neg (3<x) $ & $ (\proofRule{resolution}\, 2, 5)$ \\
+7.& \ctxsep & $x + y < 1 $ & $ (\proofRule{resolution}\, 4, 6)$ \\
+8.& \ctxsep & $\neg (x + y < 1), \neg (x≈ 2) \lor \neg (0 ≈ y)$ & $\proofRule{la_generic}\,[1.0, -1.0, 1.0]$ \\
+9.& \ctxsep & $\bot $ & $ (\proofRule{resolution}\, 8, 7, 2, 3)$ \\
+\end{Alethe}
+\end{example}
+
+\paragraph{Skolemization and Other Preprocessing Steps.}
+One typical example for a rule with context is the \proofRule{sko_ex}
+rule that is used to express skolemization of an existentially
+quantified variable.
+%
+The conclusion of a step that uses this rules is an equality.
+The left-hand side is a formula starting with an existential quantifier
+over some variable $x$. In the formula on the right-hand side, the
+variable is replaced by the appropriate Skolem term.
+To provide a proof for the replacement, the \proofRule{sko_ex} step
+uses one premise.
+The premise
+has a context that maps the existentially quantified variables
+to the appropriate Skolem term.
+
+\begin{AletheS}
+i. & \spctx{$\Gamma, x\mapsto (\varepsilon x.\,\varphi)$} & \ctxsep
+& $\varphi ≈ \psi$ & $(\dots)$ \\
+\spsep
+j. & $\Gamma$ & \ctxsep & $(\exists x.\,\varphi) ≈ \psi$ & $(\proofRule{sko_ex})$ \\
+\end{AletheS}
+
+\begin{example}
+To illustrate how such a rule is applied, consider the following example
+taken from~\cite{barbosa-2019}. Here the term $\neg p(\varepsilon x.\neg
+p(x))$ is skolemized. The \proofRule{refl} rule expresses
+a simple tautology on the equality (reflexivity in this case), \proofRule{cong}
+is functional congruence, and \proofRule{sko_forall} works like
+\proofRule{sko_ex}, except that the choice term is $\varepsilon x.\neg\varphi$.
+
+\begin{AletheS}
+1. & \spctx{$x\mapsto (\varepsilon x.\,\neg (p\,x))$}
+ & \ctxsep
+ & $x ≈ \varepsilon x.\,\neg (p\,x) $ &
+ $\proofRule{refl}$ \\
+2. & \spctx{$x\mapsto (\varepsilon x.\,\neg (p\,x))$} & \ctxsep & $ (p\,x) ≈ p(\varepsilon x.\,\neg (p\,x))$ & $(\proofRule{cong}\, 1)$ \\
+ \spsep
+3. & & \ctxsep & $( \forall x.\,(p\,x))≈ (p\,(\varepsilon x.\,\neg (p\,x)))$ & $(\proofRule{sko_forall}\, 2)$ \\
+4. & & \ctxsep & $(\neg\forall x.\,(p\,x))≈ \neg (p\,(\varepsilon x.\,\neg (p\,x)))$ & $(\proofRule{cong}\, 3)$ \\
+\end{AletheS}
+
+\section{Bibliography}
+\bibliographystyle{plain}
+\bibliography{publications}
+\end{document}
+