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

@@ -286,10 +286,10 @@ break
 \and Hans-Jörg Schurr\textsuperscript{4}}
 \date{}
 \publishers{
-\textsuperscript{1} Universidade Federal de Minas Gerais\\
-\textsuperscript{2} Johannes Kepler University Linz\\
-\textsuperscript{3} Université de Liège\\
-\textsuperscript{4} University of Lorraine, CNRS, Inria, and LORIA, Nancy\\
+  \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 Iowa, Iowa City, USA\\
 }
 
 \makeatletter
@@ -1329,7+1329,7 @@
 resolution rule with the rule name \proofRule{resolution} or
 \proofRule{th_resolution}. Both names denote the same rule. The
 difference only serves to distinguish if the rule was introduced by
 the SAT solver or by a theory solver. The resolution step is purely
 propositional; there is no notion of a unifier.  The resolution
 rules also implicitly simplifies repeated negations at the head
 of literals.