diff --git a/spec/publications.bib b/spec/publications.bib
index 405318a65d85bf99fd26ad569ddbd5e0f76e4463..5921fdca299dcb250b46d3f97367ae3439395ab8 100644
--- a/spec/publications.bib
+++ b/spec/publications.bib
@@ -1,1437 +1,115 @@
-@misc{smtcomp21-rules,
- title = "16th International Satisfiability Modulo Theories Competition ({SMT-COMP 2021}): Rules and Procedures",
- author = "Barbosa, Haniel and Hoenicke, Jochen and Hyvarinen Antti",
- howpublished = "\href{https://smt-comp.github.io/2021/rules.pdf}",
- year = 2021,
- note = "Accessed: 2021-08-08"
-}
-
-@inproceedings{pulp,
- title={{PuLP} : A Linear Programming Toolkit for {Python}},
- author={Stuart Mitchell and Michael O'Sullivan and Iain Dunning},
- year={2011}
-}
-
-@misc{par2,
- author = {Marijn Heule and Matti Järvisalo and Martin Suda},
- title = {{SAT} Race 2019},
- howpublished = {\href{http://sat-race-2019.ciirc.cvut.cz/}},
- year = 2019,
- note = "Accessed: 2022-02-28"
-}
-
-@inproceedings{gridtpt,
- TITLE = {{GridTPT}: a distributed platform for Theorem Prover Testing},
- AUTHOR = {Bouton, Thomas and Caminha B. De Oliveira, Diego and D{\'e}harbe, David and Fontaine, Pascal},
- BOOKTITLE = {PAAR 2},
- ADDRESS = {Edinburgh, United Kingdom},
- YEAR = {2010},
- pages={33--39},
- MONTH = jul,
-}
-
-@inbook{manzano-1993,
- author = {Manzano, Mar\'{\i}a},
- title = {Introduction to Many-Sorted Logic},
- year = {1993},
- isbn = {0471934852},
- publisher = {John Wiley & Sons, Inc.},
- address = {USA},
- booktitle = {Many-Sorted Logic and Its Applications},
- pages = {3--86},
- month=jan,
- numpages = {84}
-}
-
-@inproceedings{wolf-1998,
- author = {Wolf, Andreas and Letz, Reinhold},
- title = {Strategy Parallelism in Automated Theorem Proving},
- year = {1998},
- doi = {10.5555/646811.706867},
- publisher = {AAAI Press},
- booktitle = {Proceedings of the Eleventh International Florida Artificial Intelligence Research Society Conference},
- pages = {142--146},
- numpages = {5}
-}
-
-@article{blanchette-2013,
- author = {Jasmin Christian Blanchette and
- Sascha B{\"{o}}hme and
- Lawrence C. Paulson},
- title = {Extending Sledgehammer with {SMT} Solvers},
- journal = {Journal of Automated Reasoning},
- volume = {51},
- number = {1},
- pages = {109--128},
- year = {2013},
- doi = {10.1007/s10817-013-9278-5},
-}
-
-@article{tamel-1997,
- author = {Tammet, Tanel},
- title = {Gandalf},
- year = {1997},
- doi = {10.1023/A:1005887414560},
- journal = {Journal of Automated Reasoning},
- pages = {199--204},
- volume = {18},
- number = {2},
-}
-
-
-@article{kuehlwein-2015,
- author = {K\"{u}hlwein, Daniel and Urban, Josef},
- title = {{MaLeS}: A Framework for Automatic Tuning of Automated Theorem Provers},
- year = {2015},
- publisher = {Springer},
- address = {Berlin, Heidelberg},
- volume = {55},
- number = {2},
- doi = {10.1007/s10817-015-9329-1},
- journal = {Journal of Automated Reasoning},
- month = {aug},
- pages = {91-–116},
- numpages = {26},
-}
-
-@incollection{rice-1976,
- title = {The Algorithm Selection Problem},
- editor = {Morris Rubinoff and Marshall C. Yovits},
- series = {Advances in Computers},
- publisher = {Elsevier},
- volume = {15},
- pages = {65--118},
- year = {1976},
- doi = {10.1016/S0065-2458(08)60520-3},
- author = {John R. Rice},
-}
-
-@article{hutter-2009,
- author = {Hutter, Frank and Hoos, Holger H. and Leyton-Brown, Kevin and St\"{u}tzle, Thomas},
- title = {{ParamILS}: An Automatic Algorithm Configuration Framework},
- year = {2009},
- publisher = {AI Access Foundation},
- address = {El Segundo, CA, USA},
- volume = {36},
- number = {1},
- doi = {10.5555/1734953.1734959},
- journal = {Journal of Artificial Intelligence Research},
- month = {sep},
- pages = {267--306},
- numpages = {40}
-}
-
-@inproceedings{urban-2015,
- author = {Josef Urban},
- title = {{BliStr}: The Blind Strategymaker},
- booktitle = {GCAI 2015},
- editor = {Georg Gottlob and Geoff Sutcliffe and Andrei Voronkov},
- series = {EPiC Series in Computing},
- volume = {36},
- pages = {312--319},
- year = {2015},
- publisher = {EasyChair},
- issn = {2398-7340},
- doi = {10.29007/8n7m}
-}
-
-@misc{casc-15-gandalf,
- author = {Tanel Tammet},
- title = {Gandalf c-1.1},
- howpublished = {\href{http://www.tptp.org/CASC/15/SystemDescriptions.html#Gandalf}},
- year = 1998,
- note = "Accessed: 2022-03-24"
-}
-
-@article{riazanov-2003,
- author = {Riazanov, Alexandre and Voronkov, Andrei},
- title = {Limited Resource Strategy in Resolution Theorem Proving},
- year = {2003},
- issue_date = {July 2003},
- publisher = {Academic Press, Inc.},
- address = {USA},
- volume = {36},
- number = {1–2},
- doi = {10.1016/S0747-7171(03)00040-3},
- journal = {Journal of Symbolic Computation},
- month = {jul},
- pages = {101--115},
- numpages = {15}
-}
-
-@InProceedings{wenzel-2013,
- author="Wenzel, Makarius",
- editor="Blazy, Sandrine
- and Paulin-Mohring, Christine
- and Pichardie, David",
- title="Shared-Memory Multiprocessing for Interactive Theorem Proving",
- booktitle="ITP 4",
- year="2013",
- publisher="Springer Berlin Heidelberg",
- pages="418--434",
- doi="10.1007/978-3-642-39634-2_30"
-}
-
-@InProceedings{desharnais-2022,
- author = {Desharnais, Martin and Vukmirovi\'{c}, Petar and Blanchette, Jasmin and Wenzel, Makarius},
- title = {{Seventeen Provers Under the Hammer}},
- booktitle = {ITP 13},
- pages = {8:1--8:18},
- series = {Leibniz International Proceedings in Informatics (LIPIcs)},
- year = {2022},
- volume = {237},
- editor = {Andronick, June and de Moura, Leonardo},
- publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
- address = {Dagstuhl, Germany},
- doi = {10.4230/LIPIcs.ITP.2022.8},
-}
-
-@misc{weber-2018,
- author = {Tjark Weber},
- title = {{Par4}},
- howpublished = {\href{http://smt2019.galois.com/papers/tool_paper_9.pdf}},
- year = 2018,
- note = "SMT-COMP 2018 system description. Accessed: 2022-03-30"
-}
-
-@inproceedings{balunovic-2018,
- author = {Balunovi\'{c}, Mislav and Bielik, Pavol and Vechev, Martin},
- title = {Learning to Solve {SMT} Formulas},
- year = {2018},
- publisher = {Curran Associates Inc.},
- booktitle = {NIPS 32},
- pages = {10338--10349},
- doi = {10.5555/3327546.3327694},
- numpages = {12},
- location = {Montr\'{e}al, Canada},
-}
-
-@inbook{demoura-2013,
- author="de Moura, Leonardo
- and Passmore, Grant Olney",
- editor="Bonacina, Maria Paola
- and Stickel, Mark E.",
- title="The Strategy Challenge in {SMT} Solving",
- bookTitle="Automated Reasoning and Mathematics: Essays in Memory of William W. McCune",
- year="2013",
- publisher="Springer",
- address="Berlin, Heidelberg",
- pages="15--44",
- doi="10.1007/978-3-642-36675-8_2",
-}
-
-@inproceedings{ReyEtAl-FROCOS-17,
- author = {Andrew Reynolds and
- Cesare Tinelli and
- Dejan Jovanovic and
- Clark W. Barrett},
- title = {Designing Theory Solvers with Extensions},
- booktitle = {FroCoS 11},
- pages = {22--40},
- doi = {10.1007/978-3-319-66167-4\_2},
- editor = {Clare Dixon and
- Marcelo Finger},
- series = {Lecture Notes in Computer Science},
- volume = {10483},
- publisher = {Springer},
- year = {2017},
-}
-
-@InProceedings{scott-2021,
- author="Scott, Joseph
- and Niemetz, Aina
- and Preiner, Mathias
- and Nejati, Saeed
- and Ganesh, Vijay",
- editor="Groote, Jan Friso
- and Larsen, Kim Guldstrand",
- title="MachSMT: A Machine Learning-based Algorithm Selector for {SMT} Solvers",
- booktitle="TACAS 27",
- year="2021",
- doi="10.1007/978-3-030-72013-1_16",
- publisher="Springer International Publishing",
- address="Cham",
- pages="303--325"
-}
-
-@article{burel-2020,
- author = {Guillaume Burel and
- Guillaume Bury and
- Rapha{\"{e}}l Cauderlier and
- David Delahaye and
- Pierre Halmagrand and
- Olivier Hermant},
- title = {First-Order Automated Reasoning with Theories: When Deduction Modulo
- Theory Meets Practice},
- journal = {Journal of Automated Reasoning},
- volume = {64},
- number = {6},
- pages = {1001--1050},
- year = {2020},
- doi = {10.1007/s10817-019-09533-z},
-}
-
-@article{dowek-2015,
- author = {Gilles Dowek},
- title = {Deduction modulo theory},
- journal = {CoRR},
- volume = {abs/1501.06523},
- year = {2015},
- url = {http://arxiv.org/abs/1501.06523},
- eprinttype = {arXiv},
- eprint = {1501.06523},
- timestamp = {Mon, 13 Aug 2018 16:47:14 +0200},
- biburl = {https://dblp.org/rec/journals/corr/Dowek15a.bib},
- bibsource = {dblp computer science bibliography, https://dblp.org}
-}
-
-@article{xu-2008,
- author = {Xu, Lin and Hutter, Frank and Hoos, Holger H. and Leyton-Brown, Kevin},
- title = {{SATzilla}: Portfolio-Based Algorithm Selection for {SAT}},
- year = {2008},
- issue_date = {May 2008},
- publisher = {AI Access Foundation},
- address = {El Segundo, CA, USA},
- volume = {32},
- number = {1},
- journal = {Journal of Artificial Intelligence Research},
- month = {jun},
- doi = {10.5555/1622673.1622687},
- pages = {565--606},
- numpages = {42}
-}
-
-@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{barbosa-2017,
- author = "Barbosa, Haniel
- and Fontaine, Pascal
- and Reynolds, Andrew",
- editor = "Legay, Axel
- and Margaria, Tiziana",
- title = "Congruence Closure with Free Variables",
- booktitle = "TACAS 23",
- year = "2017",
- series = {Lecture Notes in Computer Science},
- volume = "10206",
- publisher = "Springer Berlin Heidelberg",
- pages = "214--230",
- doi = {10.1007/978-3-662-54580-5\_13}
-}
-
-@phdthesis{barbosa-2017-phd,
- author = {Haniel Barbosa},
- title = {New techniques for instantiation and proof production in {SMT} solving.
- (Nouvelles techniques pour l'instanciation et la production des preuves
- dans {SMT)}},
- school = {University of Lorraine, Nancy, France},
- year = {2017},
- url = {https://tel.archives-ouvertes.fr/tel-01591108},
-}
-
-@InProceedings{vampire,
-author="Kov{\'a}cs, Laura
-and Voronkov, Andrei",
-editor="Sharygina, Natasha
-and Veith, Helmut",
-title="First-Order Theorem Proving and {Vampire}",
-booktitle="CAV 25",
-year="2013",
-publisher="Springer Berlin Heidelberg",
-pages="1--35",
-isbn="978-3-642-39799-8",
-doi={10.1007/978-3-642-39799-8\_1}
-}
-
-@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}
-}
-
-@INPROCEEDINGS{reynolds-2014,
- author={Andrew {Reynolds} and Cesare {Tinelli} and Leonardo {de Moura}},
- booktitle={{FMCAD} 14},
- title={Finding conflicting instances of quantified formulas in {SMT}},
- doi = {10.1109/FMCAD.2014.6987613},
- year = {2014},
- publisher = {IEEE},
- pages = {195-202},
-}
-
-@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 22",
- pages = {151--156},
- year = {2009},
- editor = {Renate A. Schmidt},
- series = {Lecture Notes in Computer Science},
- volume = {5663},
- publisher = "Springer Berlin Heidelberg",
- 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 23",
- year = "2011",
- series = {Lecture Notes in Computer Science},
- volume = {6806},
- publisher = "Springer Berlin Heidelberg",
- pages = "171--177",
- doi = {10.1007/978-3-642-22110-1_14}
-}
-
-@inproceedings{reynolds-2018,
- author = {Andrew Reynolds and
- Haniel Barbosa and
- Pascal Fontaine},
- title = {Revisiting Enumerative Instantiation},
- booktitle = {TACAS 24},
- pages = {112--131},
- year = {2018},
- doi = {10.1007/978-3-319-89963-3_7},
- editor = {Dirk Beyer and
- Marieke Huisman},
- series = {Lecture Notes in Computer Science},
- volume = {10806},
- publisher = {Springer International Publishing}
-}
-
-@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 14",
- volume = {4963},
- series = {Lecture Notes in Computer Science},
- year = "2008",
- publisher = "Springer Berlin Heidelberg",
- pages = "337--340",
- doi = {10.1007/978-3-540-78800-3_24}
-}
-
-@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}}
-}
-
-
-@incollection{barrett-2021,
- author={Clark W. Barrett and Roberto Sebastiani and Sanjit A. Seshia and Cesare Tinelli},
- editor = {Biere, Armin and Heule, Marijn and van Maaren, Hans and Walsh, Toby},
- title = {Satisfiability Modulo Theories},
- booktitle = {Handbook of Satisfiability},
- title = {Satisfiability Modulo Theories},
- booktitle = {Handbook of Satisfiability -- Second Edition},
- series = {Frontiers in Artificial Intelligence and Applications},
- volume = {336},
- pages = {1267--1329},
- publisher = {{IOS} Press},
- year = {2021},
- doi = {10.3233/FAIA201017},
-}
-
-@InProceedings{yeting-2007,
- author="Ge, Yeting
- and Barrett, Clark
- and Tinelli, Cesare",
- editor="Pfenning, Frank",
- title="Solving Quantified Verification Conditions Using Satisfiability Modulo Theories",
- booktitle="CADE 21",
- year="2007",
- publisher="Springer Berlin Heidelberg",
- pages="167--182",
- doi={10.1007/978-3-540-73595-3_12}
-}
-
-@InProceedings{demoura-2007,
- author="de Moura, Leonardo
- and Bj{\o}rner, Nikolaj",
- editor="Pfenning, Frank",
- title="Efficient {E}-Matching for {SMT} Solvers",
- booktitle="CADE 21",
- year="2007",
- publisher="Springer Berlin Heidelberg",
- pages="183--198",
- doi={10.1007/978-3-540-73595-3\_13}
-}
-
-@article{detlefs-2005,
- author = {Detlefs, David and Nelson, Greg and Saxe, James B.},
- title = {{Simplify}: A Theorem Prover for Program Checking},
- year = {2005},
- publisher = {Association for Computing Machinery},
- address = {New York, NY, USA},
- volume = {52},
- number = {3},
- issn = {0004-5411},
- doi = {10.1145/1066100.1066102},
- journal = {Journal of the ACM},
- month = may,
- pages = {365–473},
- numpages = {109},
-}
-
-@article{nelson-1979,
-author = {Nelson, Greg and Oppen, Derek C.},
-title = {Simplification by Cooperating Decision Procedures},
-year = {1979},
-publisher = {Association for Computing Machinery},
-address = {New York, NY, USA},
-volume = {1},
-number = {2},
-doi = {10.1145/357073.357079},
-journal = {ACM Transactions on Programming Languages and Systems},
-month = {oct},
-pages = {245--257},
-numpages = {13}
-}
-
-@InProceedings{yeting-2009,
- author="Ge, Yeting
- and de Moura, Leonardo",
- editor="Bouajjani, Ahmed
- and Maler, Oded",
- title="Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories",
- booktitle="CAV 21",
- year="2009",
- publisher="Springer Berlin Heidelberg",
- pages="306--320",
- doi={10.1007/978-3-642-02658-4_25}
-}
-
-@inbook{sekar-2001,
- author = {Sekar, R. and Ramakrishnan, I. V. and Voronkov, Andrei},
- title = {Term Indexing},
- year = {2001},
- isbn = {0444508120},
- publisher = {Elsevier Science Publishers B. V.},
- address = {Amsterdam, Netherlands},
- booktitle = {Handbook of Automated Reasoning},
- pages = {1853--1964},
- numpages = {112},
- doi={10.5555/778522.778535}
-}
-
-@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}
-}
-
-
-@article{martelli-1982,
- author = {Martelli, Alberto and Montanari, Ugo},
- title = {An Efficient Unification Algorithm},
- year = {1982},
- publisher = {Association for Computing Machinery},
- address = {New York, NY, USA},
- volume = {4},
- number = {2},
- doi = {10.1145/357162.357169},
- journal = {ACM Transactions on Programming Languages and Systems},
- month = apr,
- pages = {258-–282},
- numpages = {25}
-}
-
-@incollection{baaz-2001,
- title = {Chapter 5 -- Normal Form Transformations},
- editor = {Alan Robinson and Andrei Voronkov},
- booktitle = {Handbook of Automated Reasoning},
- publisher = {North-Holland},
- address = {Amsterdam},
- pages = {273--333},
- year = {2001},
- series = {Handbook of Automated Reasoning},
- doi = {10.1016/B978-044450813-3/50007-2},
- author = {Matthias Baaz and Uwe Egly and Alexander Leitsch and Jean Goubault-Larrecq and David Plaisted}
-}
-
-@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}
-}
-
-@inproceedings{schurr-2021a,
- author = "Fontaine, Pascal
- and Schurr, Hans-J{\"o}rg",
- editor = "Konev, Boris and Reger, Giles",
- title = "Quantifier Simplification by Unification in SMT",
- booktitle = "FroCoS 13",
- year = "2021",
- publisher = "Springer International Publishing",
- address = "Cham",
- pages = "232--249",
- doi = "10.1007/978-3-030-86205-3_13",
-}
-
-
-@article{robinson-1965,
-author = {Robinson, John Alan},
-title = {A Machine-Oriented Logic Based on the Resolution Principle},
-year = {1965},
-publisher = {Association for Computing Machinery},
-address = {New York, NY, USA},
-volume = {12},
-number = {1},
-doi = {10.1145/321250.321253},
-journal = {Journal of the ACM},
-month = jan,
-pages = {23–41},
-numpages = {19}
-}
-
-@article{bonacina-2011,
- author = {Bonacina, Maria Paola and Lynch, Christopher and de Moura, Leonardo},
- year = {2011},
- month = {08},
- pages = {161-189},
- title = {On Deciding Satisfiability by Theorem Proving with Speculative Inferences},
- volume = {47},
- journal = {Journal of Automated Reasoning},
- doi = {10.1007/s10817-010-9213-y}
-}
-
-@InProceedings{demoura-2008,
-author="de Moura, Leonardo
-and Bj{\o}rner, Nikolaj",
-editor="Armando, Alessandro
-and Baumgartner, Peter
-and Dowek, Gilles",
-title="Engineering {DPLL(T)} + Saturation",
-year="2008",
-publisher="Springer Berlin Heidelberg",
-pages="475--490",
-doi={10.1007/978-3-540-71070-7\_40},
-booktitle="IJCAR 4",
-}
-
-@InProceedings{voronkov-2014,
-author="Voronkov, Andrei",
-editor="Biere, Armin
-and Bloem, Roderick",
-title="{AVATAR}: The Architecture for First-Order Theorem Provers",
-booktitle="CAV 26",
-year="2014",
-publisher="Springer International Publishing",
-pages="696--710",
-doi={10.1007/978-3-319-08867-9\_46},
-isbn="978-3-319-08867-9"
-}
-
-@proceedings{zenodo,
- title = {Quantifier Simplification by Unification in {SMT}},
- author = {Pascal Fontaine and Hans-Jörg Schurr},
- year = 2021,
- publisher = {Zenodo},
- month = jul,
- doi = {10.5281/zenodo.5088868},
-}
-
-
-@misc{ip-tutorial,
- title = "A Tutorial on Integer Programming",
- author = "Gérard Cornuéjols and Michael A. Trick and Matthew J. Saltzman",
- howpublished = "\href{https://www.math.clemson.edu/~mjs/courses/mthsc.440/integer.pdf}",
- year = 1995,
- note = "Accessed: 2022-04-07"
-}
-
-@inproceedings{fontaine-21,
- author = "Fontaine, Pascal
- and Schurr, Hans-J{\"o}rg",
- editor = "Konev, Boris and Reger, Giles",
- title = "Quantifier Simplification by Unification in {SMT}",
- booktitle = "Frontiers of Combining Systems",
- year = "2021",
- publisher = "Springer International Publishing",
- address = "Cham",
- pages = "232--249",
- doi = "10.1007/978-3-030-86205-3_13",
-}
-
-@misc{tange_2021_5123056,
- author = {Tange, Ole},
- title = {{GNU} Parallel 20210722 ('Blue Unity')},
- month = jul,
- year = 2021,
- note = {{GNU Parallel is a general parallelizer to run
- multiple serial command line programs in parallel
- without changing them.}},
- publisher = {Zenodo},
- doi = {10.5281/zenodo.5123056},
- url = {https://doi.org/10.5281/zenodo.5123056}
-}
-
-@article{nieuwenhuis-06,
- author = {Nieuwenhuis, Robert and Oliveras, Albert and Tinelli, Cesare},
- title = {Solving {SAT} and {SAT} Modulo Theories: From an Abstract Davis--Putnam--Logemann--Loveland Procedure to DPLL(T)},
- year = {2006},
- issue_date = {November 2006},
- publisher = {Association for Computing Machinery},
- address = {New York, NY, USA},
- volume = {53},
- number = {6},
- doi = {10.1145/1217856.1217859},
- journal = {Journal of the ACM},
- month = {nov},
- pages = {937--977},
- numpages = {41},
-}
-
-@phdthesis{dross-2014,
- author = {Claire Dross},
- title = {Generic Decision Procedures for Axiomatic First-Order Theories},
- school = {Universit{\'e} Paris-Sud},
- year = 2014,
- month = apr
-}
-
-@InProceedings{leino-2016,
-author="Leino, K. R. M.
-and Pit-Claudel, Cl{\'e}ment",
-editor="Chaudhuri, Swarat
-and Farzan, Azadeh",
-title="Trigger Selection Strategies to Stabilize Program Verifiers",
-booktitle="Computer Aided Verification",
-year="2016",
-publisher="Springer International Publishing",
-address="Cham",
-pages="361--381",
-doi="10.1007/978-3-319-41528-4_20"
-}
-
-@inproceedings{reynolds-2016,
- author = {Andrew Reynolds},
- title = {Conflicts, Models and Heuristics for Quantifier Instantiation in {SMT}},
- booktitle = {Vampire 3},
- editor = {Laura Kovacs and Andrei Voronkov},
- series = {EPiC Series in Computing},
- volume = {44},
- pages = {1--15},
- year = {2017},
- publisher = {EasyChair},
- doi = {10.29007/jmd3}
-}
-
-@InProceedings{blanchette-2011,
- author = "Blanchette, Jasmin Christian and B{\"o}hme, Sascha and
- Paulson, Lawrence C.",
- editor = "Bj{\o}rner, Nikolaj and Sofronie-Stokkermans, Viorica",
- title = "Extending {Sledgehammer} with {SMT} Solvers",
- booktitle = "CADE 23",
- year = "2011",
- series = {Lecture Notes in Computer Science},
- volume = {6803},
- publisher = "Springer Berlin Heidelberg",
- pages = "116--130",
- doi = {10.1007/978-3-642-22438-6\_11}
-}
-
-@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 1",
- series = {Lecture Notes in Computer Science},
- volume = "6172",
- year = "2010",
- publisher = "Springer Berlin Heidelberg",
- pages = "179--194",
- doi = {10.1007/978-3-642-14052-5\_14}
-}
-
-@article{Blanchette2016-isar,
- author = {Blanchette, Jasmin C. and
- B{\"{o}}hme, Sascha and
- Fleury, Mathias and
- Smolka, Steffen J. and
- Albert Steckermeier},
- title = {Semi-intelligible {I}sar Proofs from Machine-Generated Proofs},
- journal = jar,
- volume = {56},
- number = {2},
- pages = {155--200},
- year = {2016},
- doi = {10.1007/s10817-015-9335-3},
-}
-
-@InProceedings{ebner-2021,
- author="Ebner, Gabriel
- and Blanchette, Jasmin
- and Tourret, Sophie",
- editor="Platzer, Andr{\'e}
- and Sutcliffe, Geoff",
- title="A Unifying Splitting Framework",
- booktitle="CADE 28",
- year="2021",
- publisher="Springer International Publishing",
- address="Cham",
- doi = {10.1007/978-3-030-79876-5_20},
- pages="344--360",
-}
-
-@inproceedings{mikolas-2021,
- author="Janota, Mikoláš and Barbosa, Haniel and Fontaine, Pascal and Reynolds, Andrew",
- editor="Piskac, Ruzica and Whalen, Michael W.",
- title="Fair and Adventurous Enumeration of Quantifier Instantiations",
- booktitle="FMCAD 21",
- year=2021,
- publisher="TU Wien Academic Press",
- address="Vienna, Austria",
- doi={10.34727/2021/isbn.978-3-85448-046-4},
- pages="256-–260"
-}
-
-@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},
-}
-
-@book{gordon-1979-lcf,
- author = {Michael J. C. Gordon and
- Robin Milner and
- Christopher P. Wadsworth},
- title = {Edinburgh {LCF}: A Mechanised Logic of Computation},
- series = {Lecture Notes in Computer Science},
- volume = {78},
- publisher = {Springer Berlin Heidelberg},
- year = {1979},
- doi = {10.1007/3-540-09724-4}
-}
-
-@inproceedings{verit-ho,
- author = {Haniel Barbosa and
- Andrew Reynolds and
- Daniel El Ouraoui and
- Cesare Tinelli and
- Clark W. Barrett},
- editor = {Pascal Fontaine},
- title = {Extending {SMT} Solvers to Higher-Order Logic},
- booktitle = {CADE 27},
- series = {Lecture Notes in Computer Science},
- volume = {11716},
- pages = {35--54},
- publisher = {Springer International Publishing},
- year = {2019},
- doi = {10.1007/978-3-030-29436-6\_3},
-}
-
-@techreport{SRI:simplex:dpllt,
- author = { Bruno Dutertre and Leonardo de Moura},
- title = { Integrating Simplex with {DPLL(T)} },
- year = {2006},
- month = may,
- url = {http://www.csl.sri.com/users/bruno/publis/sri-csl-06-01.pdf},
- institution = { {SRI International} },
-}
-
-@article{schulz-2002,
- author = {Stephan Schulz},
- title = {{E} -- a brainiac theorem prover},
- journal = {{AI} Communications},
- volume = {15},
- number = {2-3},
- pages = {111--126},
- year = {2002},
- publisher = {IOS Press},
-}
-
-@article{green-jar,
- author = {Mohammad Abdulaziz and
- Lawrence C. Paulson},
- title = {An {Isabelle/HOL} Formalisation of {Green}'s Theorem},
- journal = jar,
- volume = {63},
- number = {3},
- pages = {763--786},
- year = {2019},
- month = nov,
- doi = {10.1007/s10817-018-9495-z},
-}
-
-@article{Prime_Distribution_Elementary-AFP,
- author = {Manuel Eberl},
- title = {Elementary Facts About the Distribution of Primes},
- journal = {Archive of Formal Proofs},
- month = feb,
- url = {https://isa-afp.org/entries/Prime_Distribution_Elementary.html},
- year = 2019,
- note = {Formal proof development},
- ISSN = {2150-914x},
-}
-
-@article{Simplex-AFP,
- author = {Filip Marić and Mirko Spasić and René Thiemann},
- title = {An Incremental Simplex Algorithm with Unsatisfiable Core Generation},
- journal = {Archive of Formal Proofs},
- month = aug,
- year = 2018,
- url = {https://isa-afp.org/entries/Simplex.html},
- note = {Formal proof development},
- ISSN = {2150-914x},
-}
-
-@misc{bug-report,
- author = {Fabian Immler},
- year = {2019},
- month = may,
- title = {{Re: [isabelle] Isabelle2019-RC2 sporadic smt failures}},
- howpublished = {Email},
- url = {https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2019-May/msg00130.html}
-}
-
-
-@article{Ordered_Resolution_Prover-AFP,
- author = {Schlichtkrull, Anders and Blanchette, Jasmin C. and Traytel, Dmitriy and Waldmann, Uwe},
- title = {Formalization of {B}achmair and {G}anzinger's Ordered Resolution Prover},
- journal = {Archive of Formal Proofs},
- month = jan,
- year = 2018,
- url = {https://isa-afp.org/entries/Ordered_Resolution_Prover.html},
- note = {Formal proof development},
- ISSN = {2150-914x},
-}
-
-
-@inproceedings{barbosa-2016,
- author = {Haniel Barbosa},
- title = {Efficient Instantiation Techniques in {SMT} (Work In Progress)},
- pages = {1--10},
- year = {2016},
- month = jul,
- url = {http://ceur-ws.org/Vol-1635/#paper-01},
- editor = {Pascal Fontaine and
- Stephan Schulz and
- Josef Urban},
- title = {{PAAR} 5},
- volume = {1635},
- publisher = {CEUR-WS.org},
-}
-
-@article{Prime_Number_Theorem-AFP,
- author = {Manuel Eberl and Lawrence C. Paulson},
- title = {The Prime Number Theorem},
- journal = {Archive of Formal Proofs},
- month = sep,
- year = 2018,
- url = {https://isa-afp.org/entries/Prime_Number_Theorem.html},
- note = {Formal proof development},
- ISSN = {2150-914x},
-}
-
-
-@article{Lambda_Free_KBOs-AFP,
- author = {Heiko Becker and Jasmin Christian Blanchette and Uwe Waldmann and Daniel Wand},
- title = {Formalization of {Knuth–Bendix} Orders for Lambda-Free Higher-Order Terms},
- journal = {Archive of Formal Proofs},
- month = nov,
- year = 2016,
- url = {https://isa-afp.org/entries/Lambda_Free_KBOs.html},
- note = {Formal proof development},
- ISSN = {2150-914x},
-}
-
-
-@article{green-afp,
- author = {Mohammad Abdulaziz and Lawrence C. Paulson},
- title = {An {Isabelle/HOL} formalisation of {Green}'s Theorem},
- journal = {Archive of Formal Proofs},
- month = jan,
- year = 2018,
- url = {https://isa-afp.org/entries/Green.html},
- note = {Formal proof development},
- ISSN = {2150-914x},
-}
-@article{meng-2009,
- author = {Jia Meng and
- Paulson, Lawrence C. },
- title = {Lightweight relevance filtering for machine-generated resolution problems},
- doi = {10.1016/j.jal.2007.07.004},
- journal = {Journal of Applied Logic},
- volume = {7},
- number = {1},
- pages = {41--57},
- year = {2009}
+@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"
}
-
-@inproceedings{kuehlwein-2013,
- author = {K{\"{u}}hlwein, Daniel and
- Blanchette, Jasmin Christian and
- Kaliszyk, Cezary and
- Urban, Josef},
- title = {{MaSh}: Machine Learning for {Sledgehammer}},
- booktitle = {{ITP} 4},
- series = {{LNCS}},
- volume = {7998},
- pages = {35--50},
- publisher = {Springer},
- year = {2013},
- doi = {10.1007/978-3-642-39634-2_6}
-}
-
-@InProceedings{judgementday,
- author = "B{\"o}hme, Sascha and Nipkow, Tobias",
- editor = "Giesl, J{\"u}rgen and H{\"a}hnle, Reiner",
- title = "{Sledgehammer}: Judgement Day",
- booktitle = "IJCAR 5",
- year = "2010",
- publisher = "Springer Berlin Heidelberg",
- pages = "107--121",
- doi = {10.1007/978-3-642-14203-1_9}
-}
-
-@proceedings{schurr_hans_jorg_2021_4727349,
- title = {{Reliable Reconstruction of Fine-Grained Proofs in
- a Proof Assistant}},
- author = {Hans-Jörg Schurr
- and Mathias Fleury
- and Martin Desharnais},
- year = 2021,
- publisher = {Zenodo},
- month = apr,
- doi = {10.5281/zenodo.4727349},
-}
-
-@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 Berlin Heidelberg",
- SERIES = lncs,
- VOLUME = {7316},
- PAGES = {194-207},
- YEAR = {2012},
- MONTH = Jun,
- doi = {10.1007/978-3-642-30885-7_14}
-}
-
-@inproceedings{interpolants,
- author = {Kenneth L. McMillan},
- title = {Interpolants from {Z3} proofs},
- booktitle = {{FMCAD} 11},
- isbn = {9780983567813},
- publisher = {FMCAD Inc},
- address = {Austin, Texas},
- pages = {19--27},
- year = {2011},
-}
-
-@article{mclaughlin-2006,
- author = {Sean McLaughlin and
- Clark Barrett and
- Yeting Ge},
- title = {Cooperating Theorem Provers: {A} Case Study Combining {HOL-Light} and
- {CVC} {L}ite},
- journal = {Electronic Notes in Theoretical Computer Science},
- volume = {144},
- number = {2},
- pages = {43--51},
- year = {2006},
- doi = {10.1016/j.entcs.2005.12.005}
-}
-
-@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~1},
- pages = {135--150},
- editor = {Jean-Pierre Jouannaud and
- Zhong Shao},
- publisher = {Springer Berlin Heidelberg},
- series = lncs,
- volume = {7086},
- year = {2011},
- doi = {10.1007/978-3-642-25379-9_12}
-}
-
-@inproceedings{ekici-2017,
- author = {Burak Ekici and
- Alain Mebsout and
- Cesare Tinelli and
- Chantal Keller and
- Guy Katz and
- Andrew Reynolds and
- Clark W. Barrett},
- title = {{SMTCoq}: {A} Plug-In for Integrating {SMT} Solvers into {Coq}},
- booktitle = {CAV 29},
- pages = {126--133},
- year = {2017},
- doi = {10.1007/978-3-319-63390-9_7},
- editor = {Rupak Majumdar and
- Viktor Kuncak},
- series = lncs,
- volume = {10427},
- publisher = {Springer International Publishing},
-}
-
-@phdthesis{bohme-thesis,
- author = {Sascha B\"ohme},
- title = {Proving Theorems of Higher-Order Logic with {SMT} Solvers},
- school = {Technische Universit\"at M\"unchen},
- year = 2012,
- url = {http://mediatum.ub.tum.de/node?id=1084525}
-}
-
-@article{stump-2013,
- author = {Stump, Aaron and Oe, Duckki and Reynolds, Andrew and Hadarean,
- Liana and Tinelli, Cesare},
- title = {{SMT} Proof Checking Using a Logical Framework},
- journal = {Formal Methods in System Design},
- volume = {42},
- number = {1},
- month = feb,
- year = {2013},
- issn = {0925-9856},
- pages = {91--118},
- numpages = {28},
- publisher = {Kluwer Academic Publishers},
- doi = {10.1007/s10703-012-0163-3}
-}
-
-@inproceedings{christ-2012,
- author = {J{\"{u}}rgen Christ and
- Jochen Hoenicke and
- Alexander Nutz},
- editor = {Alastair F. Donaldson and
- David Parker},
- title = {SMTInterpol: An Interpolating {SMT} Solver},
- booktitle = {SPIN 19},
- series = {Lecture Notes in Computer Science},
- volume = {7385},
- pages = {248--254},
- publisher = {Springer},
- year = {2012},
- doi = {10.1007/978-3-642-31759-0_19},
-}
-
-@InProceedings{hyvarinen-2016,
- author="Hyv{\"a}rinen, Antti E. J.
- and Marescotti, Matteo
- and Alt, Leonardo
- and Sharygina, Natasha",
- editor="Creignou, Nadia
- and Le Berre, Daniel",
- title="{OpenSMT2}: An {SMT} Solver for Multi-core and Cloud Computing",
- booktitle="SAT 19",
- year="2016",
- publisher="Springer International Publishing",
- address="Cham",
- pages="547--553",
- isbn="978-3-319-40970-2"
-}
-
-@InProceedings{barbosa-2022a,
- author="Barbosa, Haniel
- and Reynolds, Andrew
- and Kremer, Gereon
- and Lachnitt, Hanna
- and Niemetz, Aina
- and N{\"o}tzli, Andres
- and Ozdemir, Alex
- and Preiner, Mathias
- and Viswanathan, Arjun
- and Viteri, Scott
- and Zohar, Yoni
- and Tinelli, Cesare
- and Barrett, Clark",
- editor="Blanchette, Jasmin
- and Kov{\'a}cs, Laura
- and Pattinson, Dirk",
- title="Flexible Proof Production in an Industrial-Strength SMT Solver",
- booktitle="IJCAR 11",
- year="2022",
- publisher="Springer International Publishing",
- address="Cham",
- pages="15--35",
- doi={10.1007/978-3-031-10769-6_3}
-}
-
-
-@inproceedings{hoenicke-2022,
- author = {Jochen Hoenicke and
- Tanja Schindler},
- editor = {David D{\'{e}}harbe and
- Antti E. J. Hyv{\"{a}}rinen},
- title = {A Simple Proof Format for {SMT}},
- booktitle = {SMT 20},
- series = {{CEUR} Workshop Proceedings},
- volume = {3185},
- pages = {54--70},
- publisher = {CEUR-WS.org},
- year = {2022},
-}
-
-@inproceedings{schurr-2022,
- author = {Hans-Jörg Schurr},
- editor = {Boris Konev and
- Claudia Schon and
- Alexander Steen},
- title = {Optimal Strategy Schedules for Everyone},
- booktitle = {PAAR 8},
- series = {{CEUR} Workshop Proceedings},
- volume = {3201},
- publisher = {CEUR-WS.org},
- year = {2022},
-}
-
-@inproceedings{otoni-2021,
- title = {Theory-Specific Proof Steps Witnessing Correctness of {SMT} Executions},
- booktitle = {DAC 58},
- year = {2021},
- month = {11},
- publisher = {IEEE},
- organization = {IEEE},
- address = {San Francisco, CA, USA},
- doi = {10.1109/DAC18074.2021.9586272},
- author = {Rodrigo Otoni and Martin Blicha and Patrick Eugster and Antti E. J. Hyv{\"a}rinen and Natasha Sharygina}
-}
-
-@inproceedings{assaf-2016,
- TITLE = {Expressing theories in the λΠ-calculus modulo theory and in the {Dedukti} system},
- AUTHOR = {Assaf, Ali and Burel, Guillaume and Cauderlier, Raphal and Delahaye, David and Dowek, Gilles and Dubois, Catherine and Gilbert, Fr{\'e}d{\'e}ric and Halmagrand, Pierre and Hermant, Olivier and Saillard, Ronan},
- BOOKTITLE = {{TYPES}: Types for Proofs and Programs},
- ADDRESS = {Novi SAd, Serbia},
- YEAR = {2016},
- MONTH = May,
-}
-
-
-@article{Downey1980,
- author = {Downey, Peter J. and Sethi, Ravi and Tarjan, Robert Endre},
- title = {Variations on the Common Subexpression Problem},
- journal = {Journal of the ACM},
- volume = {27},
- number = {4},
- month = oct,
- year = {1980},
- issn = {0004-5411},
- pages = {758--771},
- numpages = {14},
- doi = {10.1145/322217.322228},
- acmid = {322228},
- publisher = {ACM},
- address = {New York, NY, USA}
-}
-
-@article{Nelson1980,
- author = {Nelson, Greg and Oppen, Derek C.},
- title = {Fast Decision Procedures Based on Congruence Closure},
- journal = {Journal of the ACM},
- month = apr,
- volume = {27},
- number = {2},
- year = {1980},
- pages = {356--364},
- numpages = {9},
- doi = {10.1145/322186.322198},
- publisher = {ACM}
-}
-
-@inproceedings{biere-2020,
- title={CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling Entering the {SAT} Competition 2020},
- author={Armin Biere and Katalin Fazekas and Mathias Fleury and Maximilian Heisinger},
- year={2020}
-}
-
-@inproceedings{barbosa-2019a,
- author = {Haniel Barbosa and
- Andrew Reynolds and
- Daniel El Ouraoui and
- Cesare Tinelli and
- Clark W. Barrett},
- editor = {Pascal Fontaine},
- title = {Extending {SMT} Solvers to Higher-Order Logic},
- booktitle = {{CADE 27}},
- series = {Lecture Notes in Computer Science},
- volume = {11716},
- pages = {35--54},
- publisher = {Springer},
- year = {2019},
- doi = {10.1007/978-3-030-29436-6\_3},
-}
-
-@misc{aguirre-2016,
- author = {Alejandro Aguirre},
- title = {Towards a Provably Correct Encoding from {F*} to {SMT}},
- howpublished = {Inria Internship Report},
- month = aug,
- year = {2016},
- url = {http://prosecco.gforge.inria.fr/personal/hritcu/students/alejandro/report.pdf},
-}
-
-@misc{matryoshka,
- author = {Jasmin Blanchette},
- title = {Matryoshka},
- howpublished = {Project Webpage},
- note = "Accessed: 2022-07-14",
- month = july,
- year = {2022},
- url = {https://matryoshka-project.github.io/#},
-}
-
-@inproceedings{defourne-2021,
- TITLE = {Improving Automation for Higher-Order Proof Steps},
- AUTHOR = {Defourn{\'e}, Rosalie},
- BOOKTITLE = {FroCos 13},
- ADDRESS = {Birmingham, United Kingdom},
- EDITOR = {Boris Konev and Giles Reger},
- PUBLISHER = {{Springer}},
- SERIES = {FroCoS 13},
- VOLUME = {12941},
- PAGES = {139--153},
- YEAR = {2021},
- MONTH = Sep,
- DOI = {10.1007/978-3-030-86205-3_8},
-}
-
-@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"
-}
-
-@inproceedings{claessen-2003,
-author = {Claessen, Koen and Sorensson, Niklas},
-year = {2003},
-month = {08},
-pages = {},
-title = {New Techniques that Improve {MACE}-style Finite Model Finding},
- BOOKTITLE = {MODEL},
-}
-