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

@@ -41,6 +41,34 @@
 
 \usepackage{cite}
 \usepackage{url}
+\usepackage[useregional]{datetime2}
+\usepackage{xltabular} % Gives us stretchable, breakable tables. for proofs
+\usepackage{longtable} % Gives us longtables for proof
+\usepackage{environ} % Gives us NewEnviron to define environements with tables
+\usepackage{fancyvrb} % Gives us \Verb which can be used in footnotes
+\usepackage{amsthm}
+\usepackage{thmtools}
+\usepackage{ccicons} % Gives us CC icons for title page
+\usepackage[nottoc,notlot,notlof]{tocbibind}
+
+\usepackage{imakeidx}
+\makeindex
+\makeindex[name=rules,options= -s rule_index_style.ist]
+% We provide a command that discards the argument to the index.  This
+% allows us to do the sectioning of the index manually and give different
+% sectin levels to the rule index and the overall index
+\newcommand\indexsection[1]{}
+\indexsetup{level=\indexsection,firstpagestyle=headings,noclearpage}
+
+% Must come after imakeidx
+\usepackage[hidelinks=true]{hyperref}
+\usepackage{breakurl}
+
+\usepackage{tikz}
+\usetikzlibrary{tikzmark,positioning}
+\usetikzlibrary{shapes,arrows,fit, scopes}
+\usetikzlibrary{arrows.meta}
+\usetikzlibrary{svg.path}
 
 \usepackage{bussproofs}
 \EnableBpAbbreviations
@@ -1329,7+1357,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.