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

@@ -11,8 +11,8 @@ Beyond many smaller clarifications and typographic improvments, the
 following changes were implemented in this release.
 \begin{itemize}
 	\item An abstract proof checking procedure to clarify
-	the semantic of the proof format was added.
-	\item A description of the semantic of contexts based on λ-terms
+	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.