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

@@ -36,7 +36,7 @@
 \indexsetup{level=\indexsection,firstpagestyle=headings,noclearpage}
 
 % Must come after imakeidx
-\usepackage{hyperref}
+\usepackage[hidelinks=true]{hyperref}
 \usepackage{breakurl}
 
 \usepackage{tikz}
@@ -213,7 +213,7 @@ break
   \textsuperscript{1} Universidade Federal de Minas Gerais, Brazil\\
   \textsuperscript{2} Albert-Ludwig-Universität Freiburg, Germany\\
   \textsuperscript{3} Université de Liège, Belgium\\
-  \textsuperscript{4} University of Lorraine, CNRS, Inria, and LORIA, Nancy, France\\
+  \textsuperscript{4} University of Iowa, Iowa City, USA\\
 }
 
 
@@ -471,7 +471,9 @@ t_i)$ where $x_i$ is a variable and $t_i$ is a term. The interpretation
 of the arguments is rule specific.  The list $c_1, \dots, c_j$ is
 the \index{context}{\em context} of the step.  Contexts are discussed below.
 Every proof ends with a step that has the empty clause as the conclusion
-and an empty context.  The list of proof rules in the appendix also uses
+and an empty context.  The list of proof rules
+in Section~\ref{apx:rules}
+also uses
 this notation to define the proof rules.
 
 The example above consists of five steps. Step~4 and~5 use premises.
@@ -580,7 +582,11 @@ i. & $\Gamma$ & \ctxsep & $t ≈ u$ & ($\ruleType{rule}$, …) \\
 
 where the term $t$\, is the original term, and $u$ is the term after
 preprocessing.  Tautologies with contexts correspond to judgments
-$\vDash_T \subst(\Gamma)(t) ≈ u$.
+$\vDash_T \subst(\Gamma)(t) ≈ u$.   Note that, some proof rules require
+an empty context.  In the list of proof rules
+in Section~\ref{apx:rules}
+this is indicated by omitting
+the $\Gamma$.
 
 Since the substitution induced by a context is capture-avoiding,
 applying it might rename bound variables to avoid binding variables
@@ -866,7 +872,7 @@ expressed as a concrete proof.
      system/.style={draw, thin, rounded corners},
 }
 
-  \begin{figure}[t]
+\begin{figure}[h]
 \center
 \begin{tikzpicture}[node distance=2cm, auto,>=latex', thick,scale=0.8]
     \node[solver] (unsat) {\textsf{Unsat mode}};
@@ -1219,7 +1225,7 @@ i. & $\Gamma$ & \ctxsep & $t ≈ u$ & $(\ruleType{rule}\; \bar{p}_n)\;[\bar{a}_m
 is encoded into
 
 \begin{AletheS}
-i. &  & \ctxsep & $L(\Gamma)[t] \simeq R(\Gamma)[u]$ & $(\ruleType{rule}\; \bar{p}_n)\;[\bar{a}_m]$ \\
+i. &  & \ctxsep & $L(\Gamma)[t] ≈ R(\Gamma)[u]$ & $(\ruleType{rule}\; \bar{p}_n)\;[\bar{a}_m]$ \\
 \end{AletheS}
 
 \noindent