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/changelog.tex

-\subsection*{0.3 --- Unreleased}
+\subsection*{0.3 --- \DTMdisplaydate{2023}{02}{10}{-1}}
 
 This release overhauls the entire document, but introduces only few
 changes to the proof format itself.
@@ -7,23 +7,21 @@ The standard now specifies that \texttt{assume} commands can only be
 issued at the start of the proof or right after an \texttt{anchor}
 command.
 
-Beyond many smaller clarifications and typographic improvments, the
-following changes were implemented in this release.
+Beyond many smaller clarifications and typographic improvements, the
+following changes are implemented in this release.
 \begin{itemize}
-	\item An abstract proof checking procedure to clarify
-	the semantics of the proof format was added.
-	\item A description of the semantics of contexts based on λ-terms
-	was added.
-  \item The document now lists all transformations that are
-  implicit in Alethe proofs.
-  \item The notation used for terms from first-order style
-   (e.g., $f(x,g(y))$) was changed to higher-order style (e.g.,
+	\item Add an abstract proof checking procedure to clarify
+	the semantics of the proof format.
+	\item Add a description of the semantics of contexts based on λ-terms.
+  \item List all transformations that are implicit in Alethe proofs.
+  \item Change the notation used for terms from first-order style
+   (e.g., $f(x,g(y))$) to higher-order style (e.g.,
    $(f\;x\;(g\;y))$).  This is only a change in notation -- the used logic
    remains many-sorted first-order logic.
-  \item There is no longer a distinction between if-and-only-if and
-   equaltiy.  Instead equality (the symbol $≈$) is used with appropiate
+  \item Eliminate the distinction between if-and-only-if and
+  equality.  Instead, use equality (the symbol $≈$) with appropriate
    sorts.
-  \item An index that lists all proof rules was added.
+  \item Add an index that lists all proof rules.
 \end{itemize}
 
 Proof rules:
@@ -46,7 +44,7 @@ The language has a formal definition and a proof of soundness.  The syntax
 describes how proofs are encoded in the text file.
 
 The syntax was extended to allow extra annotations.  Tools consuming Alethe
-proofs must be able to ignore such extra annotations. 
+proofs must be able to ignore such extra annotations.
 
 List of rules:
 \begin{itemize}