Add original proofonomicon

.gitignore

+_minted-doc/
+*.aux
+*.bbl
+*.blg
+*.fdb_latexmk
+*.fls
+*.log
+*.out
+*.pdf
+*.toc

spec/bib.bib

+@string{jar    = "Journal of Automated Reasoning"}
+@string{lncs   = "LNCS"}
+
+@inproceedings{bohme-2011,
+  title = {Designing Proof Formats: A User's Perspective---Experience Report},
+  author = {B{\"o}hme, Sascha and Weber, Tjark},
+  editor = "Pascal Fontaine and Aaron Stump",
+  url = {https://hal.inria.fr/hal-00677244},
+  booktitle = {{PxTP 2011}},
+  year = {2011},
+  pages = "27--32",
+  XXXmonth = Aug,
+}
+
+@InProceedings{bohme-2010,
+    author = "B{\"o}hme, Sascha
+        and Weber, Tjark",
+    editor = "Kaufmann, Matt
+        and Paulson, Lawrence C.",
+    title = "Fast LCF-Style Proof Reconstruction for Z3",
+    booktitle = "ITP 2010",
+    series = lncs,
+    volume = "6172",
+    year = "2010",
+    publisher = "Springer",
+    pages = "179--194",
+    isbn = "978-3-642-14052-5",
+    doi = {10.1007/978-3-642-14052-5\_14}
+}
+
+@article{barbosa-2019,
+  title = "Scalable Fine-Grained Proofs for Formula Processing",
+  journal = jar,
+  year = {2019},
+  author = "Barbosa, Haniel
+    and Blanchette, Jasmin C.
+    and Fleury, Mathias
+    and Fontaine, Pascal",
+  publisher = "Springer",
+  doi       = {10.1007/s10817-018-09502-y}
+}
+
+@phdthesis{boehme-2012,
+  author = "Sascha B{\"o}hme",
+  title = "Proving Theorems of Higher-Order Logic with {SMT} Solvers",
+  school = {Technische Universit\"at M\"unchen},
+  year = 2012,
+  url = {http://nbn-resolving.de/urn:nbn:de:bvb:91-diss-20120511-1084525-1-4}
+}
+
+@inproceedings{verit,
+  author = {Thomas Bouton
+    and Diego C. B. de Oliveira
+    and David D{\'{e}}harbe
+    and Pascal Fontaine},
+  title = {{veriT}: An Open, Trustable and Efficient {SMT}-solver},
+  booktitle = "CADE 2009",
+  pages = {151--156},
+  year = {2009},
+  editor = {Renate A. Schmidt},
+  series = lncs,
+  volume = {5663},
+  publisher = "Springer",
+  doi = {10.1007/978-3-642-02959-2\_12}
+}
+
+@inproceedings{CVC4,
+  author="Barrett, Clark
+    and Conway, Christopher L.
+    and Deters, Morgan
+    and Hadarean, Liana
+    and Jovanovi{\'{c}}, Dejan
+    and King, Tim
+    and Reynolds, Andrew
+    and Tinelli, Cesare",
+  editor = "Gopalakrishnan, Ganesh
+    and Qadeer, Shaz",
+  title = {{CVC4}},
+  booktitle = "CAV 2011",
+  year = "2011",
+  series = lncs,
+  volume = {6806},
+  publisher = "Springer",
+  pages = "171--177",
+  isbn = "978-3-642-22110-1",
+  doi = {10.1007/978-3-642-22110-1\_14}
+}
+
+@InProceedings{Z3,
+  author = "de Moura, Leonardo
+    and Bj{\o}rner, Nikolaj",
+  editor = "Ramakrishnan, C. R.
+    and Rehof, Jakob",
+  title = "Z3: An Efficient {SMT} Solver",
+  booktitle = "TACAS 2008",
+  volume = {4963},
+  series = lncs,
+  year = "2008",
+  publisher = "Springer",
+  pages = "337--340",
+  isbn = "978-3-540-78800-3",
+  doi = {10.1007/978-3-540-78800-3\_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 2017",
+  series = lncs,
+  volume = {10426},
+  year = "2017",
+  publisher = "Springer",
+  pages = "126--133",
+  isbn = "978-3-319-63390-9",
+  doi = {10.1007/978-3-319-63390-9\_7}
+}
+
+@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 2011},
+  year = {2011},
+  pages = "15--26",
+  url = {https://hal.inria.fr/hal-00642544/},
+  XXXmonth = 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 2011},
+  YEAR = {2011},
+  pages = "33--39",
+  XXXMONTH = Aug,
+  url = {https://hal.inria.fr/hal-00642535}
+}
+
+@inproceedings{paar,
+  TITLE = {Proofs in Satisfiability Modulo Theories},
+  AUTHOR = {Barrett, Clark and de Moura, Leonardo and Fontaine, Pascal},
+  EDITOR = "David Delahaye and Bruno Woltzenlogel Paleo",
+  BOOKTITLE = {{APPA 2014}},
+  volume       = {55},
+  series       = "Mathematical Logic and Foundations",
+  publisher    = {College Publications},
+  pages        = {23--44},
+  YEAR = {2014},
+}
+
+@inproceedings{rodin,
+  TITLE = {{SMT} solvers for {R}odin},
+  AUTHOR = {D{\'e}harbe, David 
+    and Fontaine, Pascal
+    and Guyot, Yoann
+    and Voisin, Laurent},
+  BOOKTITLE = {{ABZ 2012}},
+  EDITOR = {John Derrick
+    and John A. Fitzgerald
+    and Stefania Gnesi
+    and Sarfraz Khurshid
+    and Michael Leuschel
+    and Steve Reeves
+    and Elvinia Riccobene},
+  publisher = "Springer",
+  SERIES = lncs,
+  VOLUME = {7316},
+  PAGES = {194-207},
+  YEAR = {2012},
+  MONTH = Jun,
+  doi       = {10.1007/978-3-642-30885-7\_14}
+}
+
+@MISC{SMTLIB,
+  author = {Clark Barrett and Pascal Fontaine and Cesare Tinelli},
+  title = {{The Satisfiability Modulo Theories Library (SMT-LIB)}},
+  howpublished = {\url{www.SMT-LIB.org}},
+  year = 2016,
+}
+
+@incollection{barrett-2009,
+  author = {Clark Barrett
+    and Roberto Sebastiani
+    and Sanjit Seshia
+    and Cesare Tinelli},
+  editor = {Armin Biere
+    and Marijn J. H. Heule
+    and Hans van Maaren
+    and Toby Walsh},
+  title = {Satisfiability Modulo Theories},
+  booktitle = {Handbook of Satisfiability},
+  series = {Frontiers in Artificial Intelligence and Applications},
+  volume = 185,
+  chapter = 26,
+  pages = {825--885},
+  publisher = {IOS Press},
+  year = 2009,
+}
+
+@inproceedings{EkiciKKMRT16,
+  author    = {Burak Ekici and
+               Guy Katz and
+               Chantal Keller and
+               Alain Mebsout and
+               Andrew J. Reynolds and
+               Cesare Tinelli},
+  editor    = {Blanchette, Jasmin C.  and
+               Kaliszyk, Cezary },
+  title     = {Extending {SMTCoq}, a Certified Checker for {SMT} (Extended Abstract)},
+  booktitle = {HaTT 2016},
+  series    = {{EPTCS}},
+  volume    = {210},
+  pages     = {21--29},
+  year      = {2016},
+  doi       = {10.4204/EPTCS.210.5}
+}
+
+
+@inproceedings{armand-2011,
+  author    = {Micha{\"e}l Armand and
+               Germain Faure and
+               Benjamin Gr{\'e}goire and
+               Chantal Keller and
+               Laurent Th{\'e}ry and
+               Benjamin Werner},
+  title     = {A Modular Integration of {SAT}\slash{SMT} Solvers to {Coq} through
+               Proof Witnesses},
+  booktitle = {CPP~2011},
+  pages     = {135--150},
+  editor    = {Jean-Pierre Jouannaud and
+               Zhong Shao},
+  publisher = {Springer},
+  series    = lncs,
+  volume    = {7086},
+  year      = {2011},
+  doi       = {10.1007/978-3-642-25379-9\_12}
+}
+
+@Inproceedings{fleury-2019,
+  author    = {Fleury, Mathias and Schurr, Hans-J\"org},
+  year      = {2019},
+  title     = {Reconstructing veri{T} Proofs in {I}sabelle/{HOL}},
+  editor    = {Reis, Giselle and Barbosa, Haniel},
+  booktitle = {Proceedings Sixth Workshop on
+               Proof eXchange for Theorem Proving,
+               Natal, Brazil, August 26, 2019},
+  series    = {Electronic Proceedings in Theoretical Computer Science},
+  volume    = {301},
+  publisher = {Open Publishing Association},
+  pages     = {36-50},
+  doi       = {10.4204/EPTCS.301.6},
+}
+

spec/smtlib2.py

+# -*- coding: utf-8 -*-
+
+import re
+
+from pygments.lexer import Lexer, RegexLexer, bygroups, do_insertions, \
+    default, include
+from pygments.token import Text, Comment, Operator, Keyword, Name, String, \
+    Number, Punctuation, Generic
+from pygments import unistring as uni
+
+__all__ = ['Smt2Lexer']
+
+
+line_re = re.compile('.*?\n')
+
+class CustomLexer(RegexLexer):
+    """
+    A SMT-Lib 2 parser
+    """
+    name = 'Smt2'
+    aliases = ['smt2']
+    filenames = ['*.smt2']
+    mimetypes = ['text/x-smt2']
+
+    # list of known keywords and builtins taken form vim 6.4 scheme.vim
+    # syntax file.
+    keywords = (
+        'declare-const', 'declare-fun', 'declare-sort', 'define-fun', 'assert', 'check-sat',
+        'get-model', 'get-proof', 'get-value', 'echo', 'exit', 'error',
+        'sat', 'unsat', 'unknown', 'model', 'set-option', 'set-logic',
+        'anchor', 'step', 'assume'
+    )
+    sorts = (
+        'Int', 'Bool'
+    )
+    builtins = (
+        '*', '+', '-', '/', '<', '<=', '=', '>', '>=', 'and', 'or', 'distinct',
+        'not', ':=', 'forall', 'exists', 'cl'
+    )
+
+    # valid names for identifiers
+    # well, names can only not consist fully of numbers
+    # but this should be good enough for now
+    valid_name = r'[\w\.!$%&*+,/:<=>?@^~|-]+'
+
+    tokens = {
+        'root': [
+            # the comments
+            # and going to the end of the line
+            (r';.*$', Comment.Single),
+            # multi-line comment
+            (r'#\|', Comment.Multiline, 'multiline-comment'),
+            # commented form (entire sexpr folliwng)
+            (r'#;\s*\(', Comment, 'commented-form'),
+            # signifies that the program text that follows is written with the
+            # lexical and datum syntax described in r6rs
+            (r'#!r6rs', Comment),
+
+            # whitespaces - usually not relevant
+            (r'\s+', Text),
+
+            # numbers
+            (r'-?\d+\.\d+', Number.Float),
+            (r'-?\d+', Number.Integer),
+            # support for uncommon kinds of numbers -
+            # have to figure out what the characters mean
+            # (r'(#e|#i|#b|#o|#d|#x)[\d.]+', Number),
+
+            # strings, symbols and characters
+            (r'"(\\\\|\\"|[^"])*"', String),
+            (r"'" + valid_name, String.Symbol),
+            (r"#\\([()/'\"._!§$%& ?=+-]|[a-zA-Z0-9]+)", String.Char),
+
+            # constants
+            (r'(true|false)', Name.Constant),
+
+            # special operators
+            (r"('|#|`|,@|,)", Operator),
+
+            # highlight the keywords
+            ('(%s)' % '|'.join(re.escape(entry) for entry in keywords),
+             Keyword.Reserved),
+
+            # highlight the sorts
+            ('(%s)' % '|'.join(re.escape(entry) for entry in sorts),
+             Keyword.Type),
+
+            # first variable in a quoted string like
+            # '(this is syntactic sugar)
+            (r"(?<='\()" + valid_name, Name.Variable),
+            (r"(?<=#\()" + valid_name, Name.Variable),
+
+            # highlight the builtins
+            ("(?<=\()(%s)" % '|'.join(re.escape(entry) + '\s+' for entry in builtins),
+             Name.Builtin),
+
+            (r':' + valid_name, Name.Function),
+
+            # the remaining functions
+            #(r'(?<=\()' + valid_name, Name.Function),
+            # find the remaining variables
+            (valid_name, Name.Variable),
+
+            # the famous parentheses!
+            (r'(\(|\))', Punctuation),
+            (r'(\[|\])', Punctuation),
+        ],
+        'multiline-comment': [
+            (r'#\|', Comment.Multiline, '#push'),
+            (r'\|#', Comment.Multiline, '#pop'),
+            (r'[^|#]+', Comment.Multiline),
+            (r'[|#]', Comment.Multiline),
+        ],
+        'commented-form': [
+            (r'\(', Comment, '#push'),
+            (r'\)', Comment, '#pop'),
+            (r'[^()]+', Comment),
+        ],
+    }