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
@@ -713,8 +719,10 @@ problem file or, if the incremental solving commands of {\smtlib}
 are used, the implicit problem constructed at the invocation of a
 \inlineAlethe{get-proof} command.
 In this document, we will call this {\smtlib} problem the {\em input problem}.
+An Alethe proof inherits the namespace of its {\smtlib} problem.
 All symbols declared or defined in the input problem remain declared or
-defined, respectively.  Furthermore, the symbolic names introduced
+defined, respectively.
+Furthermore, the symbolic names introduced
 by the \inlineAlethe{:named} annotation also stay valid and can be used
 in the script.  For the purpose of the proof rules, terms are treated
 as if proxy names introduced by \inlineAlethe{:named} annotations have been
@@ -864,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}};
@@ -954,7 +962,8 @@ Overall, the following aspects are treated implicitly by Alethe.
         non-empty context.
   \item The order of literals in the clauses.
   \item The unfolding of names introduced by
-     \inlineAlethe{(!}\,$t$\,\inlineAlethe{:named }\;$s$\,\inlineAlethe{)}.
+     \inlineAlethe{(!}\,$t$\,\inlineAlethe{:named }\;$s$\,\inlineAlethe{)} in the
+     original {\smtlib} problem or in the proof.
   \item The removal of other {\smtlib} annotations of the form
      \inlineAlethe{(!}\,$t$\,\dots\,\inlineAlethe{)}.
   \item The unfolding of function symbols introduced by
@@ -974,10 +983,13 @@ In this section we present an abstract procedure to check if an Alethe
 proof is \index{well-formed}well-formed and valid.  An Alethe proof is
 well-formed only if its anchors and steps are balanced.  To check that
 this is the case, we replace innermost subproofs by holes until there is
-no subproof left.  If the resulting proof is free of anchors and steps
-that use concluding rules, then the proof is well-formed.
-If all the steps in the subproofs adhere to the conditions of
-their rules, the subproof is valid.  If all subproofs are valid,
+no subproof left.  If the resulting reduced proof is free of anchors and steps
+that use concluding rules, then the overall proof is well-formed.
+To check if a proof is valid we have to check if all steps of a subproof
+adhere to the conditions of
+their rules before replacing the subproof by a hole.
+If all subproofs are valid and all steps in the reduced
+proof adhere to the conditions of their rule,
 then the entire proof is valid.
 
 Formally, an Alethe proof $P$ is a list $[C_1, \dots, C_n]$ of steps
@@ -1077,8 +1089,9 @@ Section~\ref{apx:rules}.
   \end{itemize}
 \end{definition}
 
-Since the \proofRule{assume} rule expects an empty context, an admissible
-subproof can contain assumptions only if the rule used by $C_{\mathit{end}}$
+The only rule that can discharge assumptions in a subproof is the
+\proofRule{subproof} rule.  Therefore, an admissible subproof can only
+contain \proofRule{assume} step if $C_{\mathit{end}}$
 is the \proofRule{subproof} rule.
 
 To eliminate a subproof we can replace the subproof with a hole that has
@@ -1212,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