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

@@ -104,7 +104,7 @@
 \renewcommand\spsep{\cline{2-4}}
 \setlength{\arrayrulewidth}{0.8pt}
 \addtolength{\tabcolsep}{-4pt}
-\begin{xltabular}{\linewidth}{l c Y l}
+\begin{xltabular}{\linewidth}{l c Y r}
   \BODY
 \end{xltabular}
 \addtolength{\tabcolsep}{+4pt}
@@ -113,7 +113,7 @@
 \renewcommand\spsep{\cline{2-5}}
 \setlength{\arrayrulewidth}{0.8pt}
 \addtolength{\tabcolsep}{-4pt}
-\begin{xltabular}{\linewidth}{l l c Y l}
+\begin{xltabular}{\linewidth}{l l c Y r}
   \BODY
 \end{xltabular}
 \addtolength{\tabcolsep}{+4pt}
@@ -126,7 +126,7 @@
 \setlength{\arrayrulewidth}{0.8pt}%
 \addtolength{\tabcolsep}{-4pt}%
 \noindent
-\begin{tabularx}{\linewidth}{l c Y l}
+\begin{tabularx}{\linewidth}{l c Y r}
   \BODY
 \end{tabularx}
 \addtolength{\tabcolsep}{+4pt}
@@ -136,7 +136,7 @@
 \setlength{\arrayrulewidth}{0.8pt}%
 \addtolength{\tabcolsep}{-4pt}%
 \noindent
-\begin{tabularx}{\linewidth}{l l c Y l}
+\begin{tabularx}{\linewidth}{l l c Y r}
   \BODY
 \end{tabularx}
 \addtolength{\tabcolsep}{+4pt}
@@ -1329,7+1329,7 @@
 first-innermost subproof first and then replace them by holes.
 %
 Since valid proofs do not contain holes, we have to generalize the induction
 to allow holes that were introduced by the elimination of subproofs.
 %
 We start with simple subproofs with empty contexts and without
 nested subproofs.