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 --- \DTMdisplaydate{2023}{02}{10}{-1}}
+
+This release overhauls the entire document, but introduces only few
+changes to the proof format itself.
+
+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 improvements, the
+following changes are implemented in this release.
+\begin{itemize}
+	\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 Eliminate the distinction between if-and-only-if and
+  equality.  Instead, use equality (the symbol $≈$) with appropriate
+   sorts.
+  \item Add an index that lists all proof rules.
+\end{itemize}
+
+Proof rules:
+\begin{itemize}
+  \item The rule \proofRule{implies_simplify} is no longer allowed to
+  perform the simplification $(\varphi_1\rightarrow \varphi_2)\rightarrow \varphi_2
+  ⇒  \varphi_1\lor \varphi_2$.  This is now covered by \proofRule{bool_simplify}.
+\end{itemize}
+
 \subsection*{0.2 --- \DTMdisplaydate{2022}{12}{19}{-1}}
 
 This is an intermediate release.  It collects all changes to the original
@@ -11,12 +44,12 @@ 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}
     \item Improve description of \proofRule{sko_ex}.
-    \item Add \proofRule{hole} rule to allow holes.  A proof that contains
+    \item Add {\proofRule{hole}} rule to allow holes.  A proof that contains
     steps that use this rule is not valid.
 \end{itemize}
 \noindent
@@ -36,7 +69,7 @@ Clarifications:
 \end{itemize}
 
 
-\subsection*{0.1 --- \DTMdisplaydate{2021}{07}{10}{-1}}
+\subsection*{0.1 -- \DTMdisplaydate{2021}{07}{10}{-1}}
 
 This is the first public release of this document.  It coincides with
 the seventh PxTP Workshop.