Backport specification from my PhD thesis

This replaces the text of the specification and the rule list with the text in my PhD thesis.

Most importantly this adds an abstract proof checking procedure that specifies the semantic of an Altehe proof (modulo the proof rules).

Furthermore, it adapts the notation more to SMT-LIB: everything is in λ-application style ((f x) instead of f(x)) and we no longer have a distinct connective. Instead we use the equality predicate everywhere.

On the technical side this now requires lualatex for Unicode math.

spec/spec.tex

@@ -210,6 +210,7 @@ break
 
 \maketitle
 \tableofcontents
+\thispagestyle{empty}
 \clearpage
 
 \begin{abstract}
@@ -259,6 +260,7 @@ get in touch!
 \hspace*{\fill}The authors.
 \end{abstract}
 
+\section{Introduction}
 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
@@ -269,15 +271,19 @@ 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
+The Alethe proof format 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:semantic} then discusses an abstract procedure
+to check Alethe proofs.  This abstract checking procedure specifies
+the semantic of Alethe proofs.
 %
-Section~\ref{sec:alethe:rules-generic} discusses the core
-concepts behind the Alethe proof rules.
+The Alethe proof rules are discussed in two sections.
+First, Section~\ref{sec:alethe:rules-generic} discusses the core
+concepts behind the rules.
 %
-The Section~\ref{apx:rules} presents a list of
+Second, 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
@@ -291,25 +297,24 @@ 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
+The Alethe format was originally developed for 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 SMT solver {\cvcfive}~\cite{barbosa-2022} (the successor of
+{\cvcfour}) supports Alethe experimentally as one of its multiple proof
+output formats.
 %
-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
+Alethe proofs can be reconstructed by the \tactic{smt} tactic of
+the proof assistant {\isabelle}~\cite{fleury-2019,schurr-2021}.
+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
+Furthermore, \tool{Carcara} is an experimental
+high-performance \index{proof chcker}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
@@ -322,6 +327,49 @@ 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}.
 
+\subsection{Notations}
+
+The notation used in this document is similar to the notation
+used by the SMT-LIB standard.  The Alethe proof format uses precisely
+the SMT-LIB logic.  Since the SMT-LIB language is based on
+S-expressions\index{S-expression}, SMT-LIB formulas are written using
+a λ-calculus style.  That is, instead of $f(1,2)$, we write $(f\,1\,2)$.
+However, connectives that a usually written using infix notation, also
+use infix notation here.  That is, we write $t_1 \lor t_2$, not
+$(\lor\,t_1\,t_2)$.
+
+We use $x, y, z$ to indicate variables,
+$f, g$ for functions, and $P, Q$ for predicates (functions with co-domain
+sort $\lsymb{Bool}$.  To indicate terms we use $t, u$ and to indicate
+formulas (terms of sort $\lsymb{Bool}$) we use $\varphi, \psi$.
+To distinguish syntactic equality and the SMT-LIB equality predicate,
+we write $=$ for the former, and $≈$ for the later.
+We will write pre-defined SMT-LIB symbols, such as sorts and functions,
+in bold (e.g., $\lsymb{Bool}$, $\lsymb{ite}$).
+
+We will use $θ$ to denote a
+substitution\index{substitution}.
+The notation $[x₁ ↦ t₁, …, x_n ↦ t_n]$ denotes the substitution
+that maps $x_i$ to $t_i$ for $1 ≤ i ≤ n$ and corresponds to the
+identity function for all other variables.  If $θ$ and $η$ are two
+substitutions, then $θη$ denotes the result of first applying $θ$
+and then $η$ (i.e., $η(θ(.))$).  A substitution can naturally be extended
+to a function that maps terms to terms by replacing the occurrences of
+free variables.
+%
+We write $t[\,]$ for a term with a hole\index{hole} and $t[u]$ for the term where
+the hole has been replaced by $u$. Any term has at most one hole.
+%
+We also use holes with multiple variables.
+%
+The notation $t[x_1, \dots, x_n]$ stands for a term that may depend on distinct
+variables $x_1, \dots, x_n$.
+%
+$t[s_1,\dots, s_n]$ is the respective term where the variables $x_1,\dots, x_n$ are
+simultaneously substituted by $s_1,\dots, s_n$.
+
+Note that we will introduce the Alethe specific notation to write proof steps
+in the following sections.
 
 \section{The Alethe Language}
 \label{sec:alethe:language}
@@ -353,8 +401,7 @@ understand the proof step by step.
 \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!
+This includes its many-sorted first-order logic.
 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.
@@ -1467,7 +1514,7 @@ 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.
 
-\subsection{Tautologous Rules and Simple Deduction}
+\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$.
@@ -1480,7 +1527,7 @@ rule eliminates an implication: From $\varphi_1 → \varphi_2$,
 it deduces $\neg \varphi_1, \varphi_2$.
 
 
-\subsection{Resolution.}
+\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
@@ -1507,7 +1554,7 @@ 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.
 
-\subsection{Quantifier Instantiation}
+\paragraph{Quantifier Instantiation}
 \label{reference=rule:forall_inst}
 To express quantifier instantiation, the rule \proofRule{forall_inst}
 is used. It produces a formula of the form $(\neg \forall \bar
@@ -1525,7 +1572,7 @@ equalities obscures which terms have been used as instances.
 Existential quantifiers are handled by skolemization.
 
 
-\subsection{Linear Arithmetic}
+\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.}
@@ -1556,7 +1603,7 @@ of $(x+y<1) \lor$ $(3<x)$, $x≈ 2$, and $0≈ y$.
 \end{Alethe}
 \end{example}
 
-\subsection{Skolemization and Other Preprocessing Steps}
+\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.