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

@@ -18,9 +18,9 @@ following changes were implemented in this release.
   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.,
-   $(f\;x\;(g\;y))$).  This only a change in notation -- the used logic
+   $(f\;x\;(g\;y))$).  This is only a change in notation -- the used logic
    remains many-sorted first-order logic.
-  \item The is no longer a distinction between if-and-only-if and
+  \item There is no longer a distinction between if-and-only-if and
    equaltiy.  Instead equality (the symbol $≈$) is used with appropiate
    sorts.
   \item An index that lists all proof rules was added.
@@ -30,7 +30,7 @@ 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 covered by \proofRule{bool_simplify}.
+  ⇒  \varphi_1\lor \varphi_2$.  This is now covered by \proofRule{bool_simplify}.
 \end{itemize}
 
 \subsection*{0.2 --- \DTMdisplaydate{2022}{12}{19}{-1}}