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/publications.bib

+
+@InProceedings{	  barbosa-2022,
+  author	= "Barbosa, Haniel and Barrett, Clark and Brain, Martin and
+		  Kremer, Gereon and Lachnitt, Hanna and Mann, Makai and
+		  Mohamed, Abdalrhman and Mohamed, Mudathir and Niemetz, Aina
+		  and N{\"o}tzli, Andres and Ozdemir, Alex and Preiner,
+		  Mathias and Reynolds, Andrew and Sheng, Ying and Tinelli,
+		  Cesare and Zohar, Yoni",
+  editor	= "Fisman, Dana and Rosu, Grigore",
+  title		= "{cvc5}: A Versatile and Industrial-Strength {SMT} Solver",
+  booktitle	= "TACAS 28",
+  year		= "2022",
+  publisher	= "Springer International Publishing",
+  address	= "Cham",
+  pages		= "415--442",
+  doi		= "10.1007/978-3-030-99524-9_24"
+}
+
+@InProceedings{	  smtcoq,
+  author	= "Ekici, Burak and Mebsout, Alain and Tinelli, Cesare and
+		  Keller, Chantal and Katz, Guy and Reynolds, Andrew and
+		  Barrett, Clark",
+  editor	= "Majumdar, Rupak and Kun{\v{c}}ak, Viktor",
+  title		= "{SMTC}oq: A Plug-In for Integrating {SMT} Solvers into
+		  {C}oq",
+  booktitle	= "CAV 29",
+  series	= {Lecture Notes in Computer Science},
+  volume	= {10426},
+  year		= "2017",
+  publisher	= "Springer",
+  pages		= "126--133",
+  isbn		= "978-3-319-63390-9",
+  doi		= {10.1007/978-3-319-63390-9\_7}
+}
+
+@TechReport{	  smtlib,
+  author	= {Clark Barrett and Pascal Fontaine and Cesare Tinelli},
+  title		= {{The SMT-LIB Standard: Version 2.6}},
+  institution	= {Department of Computer Science, The University of Iowa},
+  year		= 2017,
+  note		= {Available at \texttt{www.SMT-LIB.org}}
+}
+
+@InProceedings{	  besson-2011,
+  title		= {A Flexible Proof Format for {SMT}: A Proposal},
+  author	= {Besson, Fr{\'e}d{\'e}ric and Fontaine, Pascal and
+		  Th{\'e}ry, Laurent},
+  editor	= "Pascal Fontaine and Aaron Stump",
+  booktitle	= {PxTP 1},
+  year		= {2011},
+  pages		= "15--26",
+  url		= {https://hal.inria.fr/hal-00642544/},
+  month		= aug
+}
+
+@InProceedings{	  deharbe-2011,
+  title		= {Quantifier Inference Rules for {SMT} Proofs},
+  author	= {D{\'e}harbe, David and Fontaine, Pascal and Woltzenlogel
+		  Paleo, Bruno},
+  editor	= "Pascal Fontaine and Aaron Stump",
+  booktitle	= {PxTP 1},
+  year		= {2011},
+  pages		= "33--39",
+  month		= aug,
+  url		= {https://hal.inria.fr/hal-00642535}
+}
+
+@InProceedings{	  schurr-2021,
+  author	= "Schurr, Hans-J{\"o}rg and Fleury, Mathias and Desharnais,
+		  Martin",
+  editor	= "Platzer, Andr{\'e} and Sutcliffe, Geoff",
+  title		= "Reliable Reconstruction of Fine-grained Proofs in a Proof
+		  Assistant",
+  booktitle	= "CADE 28",
+  year		= "2021",
+  publisher	= "Springer International Publishing",
+  address	= "Cham",
+  pages		= "450--467",
+  series	= {Lecture Notes in Computer Science},
+  doi		= {10.1007/978-3-030-79876-5_26}
+}
+
+@Article{	  barbosa-2019,
+  title		= "Scalable Fine-Grained Proofs for Formula Processing",
+  journal	= "Journal of Automated Reasoning",
+  year		= {2019},
+  month		= jan,
+  author	= "Barbosa, Haniel and Blanchette, Jasmin C. and Fleury,
+		  Mathias and Fontaine, Pascal",
+  publisher	= "Springer",
+  doi		= {10.1007/s10817-018-09502-y},
+  volume	= {64},
+  number	= {3},
+  pages		= {485--510}
+}
+
+@InProceedings{	  fleury-2019,
+  author	= {Mathias Fleury and Hans{-}J{\"{o}}rg Schurr},
+  editor	= {Giselle Reis and Haniel Barbosa},
+  title		= {Reconstructing {veriT} Proofs in {Isabelle/HOL}},
+  booktitle	= {PxTP 6},
+  series	= {{EPTCS}},
+  volume	= {301},
+  pages		= {36--50},
+  year		= {2019},
+  doi		= {10.4204/EPTCS.301.6}
+}
+
+@Misc{		  wp:alethe,
+  author	= "{Wikipedia contributors}",
+  title		= "Alethe (bird) -- {Wikipedia}{,} The Free Encyclopedia",
+  year		= "2022",
+  url		= "https://en.wikipedia.org/w/index.php?title=Alethe_(bird)&oldid=1064503766",
+  note		= "Online; accessed 2022-09-02"
+}