bartefil.bib

% Web page entries are formatted by BibItNow!: https://addons.mozilla.org/en-US/firefox/addon/bibitnow/

% 2020 PAAR
@inproceedings{DBLP:conf/cade/Bartek020,
	author       = {Filip B{\'{a}}rtek and
	Martin Suda},
	title        = {Learning Precedences from Simple Symbol Features},
	booktitle    = {Joint Proceedings of the 7th Workshop on Practical Aspects of Automated
	Reasoning {(PAAR)} and the 5th Satisfiability Checking and Symbolic
	Computation Workshop (SC-Square) Workshop, 2020 co-located with the
	10th International Joint Conference on Automated Reasoning {(IJCAR}
	2020), Paris, France, June-July, 2020 (Virtual)},
	pages        = {21--33},
	year         = {2020},
	crossref     = {DBLP:conf/cade/2020paar},
	url          = {https://ceur-ws.org/Vol-2752/paper2.pdf},
	timestamp    = {Fri, 10 Mar 2023 16:23:14 +0100},
	biburl       = {https://dblp.org/rec/conf/cade/Bartek020.bib},
	bibsource    = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/cade/2020paar,
	editor       = {Pascal Fontaine and
	Konstantin Korovin and
	Ilias S. Kotsireas and
	Philipp R{\"{u}}mmer and
	Sophie Tourret},
	title        = {Joint Proceedings of the 7th Workshop on Practical Aspects of Automated
	Reasoning {(PAAR)} and the 5th Satisfiability Checking and Symbolic
	Computation Workshop (SC-Square) Workshop, 2020 co-located with the
	10th International Joint Conference on Automated Reasoning {(IJCAR}
	2020), Paris, France, June-July, 2020 (Virtual)},
	series       = {{CEUR} Workshop Proceedings},
	volume       = {2752},
	publisher    = {CEUR-WS.org},
	year         = {2020},
	url          = {https://ceur-ws.org/Vol-2752},
	urn          = {urn:nbn:de:0074-2752-0},
	timestamp    = {Thu, 04 Apr 2024 12:46:47 +0200},
	biburl       = {https://dblp.org/rec/conf/cade/2020paar.bib},
	bibsource    = {dblp computer science bibliography, https://dblp.org}
}

% 2021 CADE
@inproceedings{DBLP:conf/cade/Bartek021,
  author       = {Filip B{\'{a}}rtek and
                  Martin Suda},
  title        = {Neural Precedence Recommender},
  booktitle    = {Automated Deduction - {CADE} 28 - 28th International Conference on
                  Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings},
  pages        = {525--542},
  year         = {2021},
  crossref     = {DBLP:conf/cade/2021},
  url          = {https://doi.org/10.1007/978-3-030-79876-5_30},
  doi          = {10.1007/978-3-030-79876-5_30},
  timestamp    = {Thu, 29 Jul 2021 13:42:16 +0200},
  biburl       = {https://dblp.org/rec/conf/cade/Bartek021.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

% 2023 LPAR
@inproceedings{DBLP:conf/lpar/Bartek023,
  author       = {Filip B{\'{a}}rtek and
                  Martin Suda},
  title        = {How Much Should This Symbol Weigh? {A} {GNN}-Advised Clause Selection},
  booktitle    = {{LPAR} 2023: Proceedings of 24th International Conference on Logic
                  for Programming, Artificial Intelligence and Reasoning, Manizales,
                  Colombia, 4-9th June 2023},
  pages        = {96--111},
  year         = {2023},
  crossref     = {DBLP:conf/lpar/2023},
  url          = {https://doi.org/10.29007/5f4r},
  doi          = {10.29007/5F4R},
  timestamp    = {Sat, 30 Sep 2023 09:52:10 +0200},
  biburl       = {https://dblp.org/rec/conf/lpar/Bartek023.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/lpar/2023,
	editor       = {Ruzica Piskac and
	Andrei Voronkov},
	title        = {{LPAR} 2023: Proceedings of 24th International Conference on Logic
	for Programming, Artificial Intelligence and Reasoning, Manizales,
	Colombia, 4-9th June 2023},
	series       = {EPiC Series in Computing},
	volume       = {94},
	publisher    = {EasyChair},
	year         = {2023},
	url          = {https://www.easychair.org/publications/volume/LPAR_2023},
	timestamp    = {Fri, 23 Feb 2024 20:09:43 +0100},
	biburl       = {https://dblp.org/rec/conf/lpar/2023.bib},
	bibsource    = {dblp computer science bibliography, https://dblp.org}
}

% 2024 IJCAR
@inproceedings{DBLP:conf/ijcar/BartekCS24,
  author       = {Filip B{\'{a}}rtek and
                  Karel Chvalovsk{\'{y}} and
                  Martin Suda},
  title        = {Regularization in {S}pider-Style Strategy Discovery and Schedule Construction},
  booktitle    = {Automated Reasoning - 12th International Joint Conference, {IJCAR}
                  2024, Nancy, France, July 3-6, 2024, Proceedings, Part {I}},
  pages        = {194--213},
  year         = {2024},
  crossref     = {DBLP:conf/ijcar/2024-1},
  url          = {https://doi.org/10.1007/978-3-031-63498-7_12},
  doi          = {10.1007/978-3-031-63498-7_12},
  timestamp    = {Sat, 20 Jul 2024 10:59:46 +0200},
  biburl       = {https://dblp.org/rec/conf/ijcar/BartekCS24.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

% 2024 IJCAR - preprint
@article{DBLP:journals/corr/abs-2403-12869,
  author       = {Filip B{\'{a}}rtek and
                  Karel Chvalovsk{\'{y}} and
                  Martin Suda},
  title        = {Regularization in {S}pider-Style Strategy Discovery and Schedule Construction},
  journal      = {CoRR},
  volume       = {abs/2403.12869},
  year         = {2024},
  url          = {https://doi.org/10.48550/arXiv.2403.12869},
  doi          = {10.48550/ARXIV.2403.12869},
  eprinttype    = {arXiv},
  eprint       = {2403.12869},
  timestamp    = {Mon, 08 Apr 2024 18:24:51 +0200},
  biburl       = {https://dblp.org/rec/journals/corr/abs-2403-12869.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

% 2024 IJCAR - dataset
@misc{bartek10814478,
	author       = {Bártek, Filip and
	Suda, Martin},
	title        = {Vampire strategy performance measurements},
	day          = 14,
	month        = mar,
	year         = 2024,
	publisher    = {Zenodo},
	version      = {1.0},
	doi          = {10.5281/zenodo.10814478},
	url          = {https://zenodo.org/records/10814478}
}

% 2024 PAAR
@inproceedings{DBLP:conf/paar/BartekC024,
  author       = {Filip B{\'{a}}rtek and
                  Karel Chvalovsk{\'{y}} and
                  Martin Suda},
  title        = {Cautious Specialization of Strategy Schedules (Extended Abstract)},
  booktitle    = {Joint Proceedings of the 9th Workshop on Practical Aspects of Automated
                  Reasoning {(PAAR)} and the 9th Satisfiability Checking and Symbolic
                  Computation Workshop (SC-Square), 2024 co-located with the 12th International
                  Joint Conference on Automated Reasoning {(IJCAR} 2024), Nancy, France,
                  July 2, 2024},
  pages        = {28--36},
  year         = {2024},
  crossref     = {DBLP:conf/paar/2024},
  url          = {https://ceur-ws.org/Vol-3717/short2.pdf},
  timestamp    = {Wed, 03 Jul 2024 23:09:04 +0200},
  biburl       = {https://dblp.org/rec/conf/paar/BartekC024.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/paar/2024,
  editor       = {Christopher W. Brown and
                  Daniela Kaufmann and
                  Cl{\'{a}}udia Nalon and
                  Alexander Steen and
                  Martin Suda},
  title        = {Joint Proceedings of the 9th Workshop on Practical Aspects of Automated
                  Reasoning {(PAAR)} and the 9th Satisfiability Checking and Symbolic
                  Computation Workshop (SC-Square), 2024 co-located with the 12th International
                  Joint Conference on Automated Reasoning {(IJCAR} 2024), Nancy, France,
                  July 2, 2024},
  series       = {{CEUR} Workshop Proceedings},
  volume       = {3717},
  publisher    = {CEUR-WS.org},
  year         = {2024},
  url          = {https://ceur-ws.org/Vol-3717},
  urn          = {urn:nbn:de:0074-3717-7},
  timestamp    = {Wed, 24 Jul 2024 13:08:45 +0200},
  biburl       = {https://dblp.org/rec/conf/paar/2024.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

% https://is.muni.cz/th/324945/fi_b/?lang=en#panelbiblatex
@misc{Bartek2012thesis,
	AUTHOR = {Bártek, Filip},
	TITLE = {Realizace Rabinovy hry na konečných grafech},
	YEAR = {2012},
	TYPE = {Bachelor's thesis},
	INSTITUTION = {Masaryk University, Faculty of Informatics},
	LOCATION = {Brno},
	SUPERVISOR = {Ivana Černá},
	URL = {https://is.muni.cz/th/u1ehd/},
	URL_DATE = {2024-04-04},
}

% https://dspace.cuni.cz/handle/20.500.11956/62638
% https://www.citacepro.com/dokument/8pPhJ9buUYe41Daa
phdthesis{bartek2015, address={Praha}, type={diplomová práce}, title={Minimální reprezentace víceintervalových booleovských funkcí}, url={http://hdl.handle.net/20.500.11956/62638}, author={Bártek, Filip}, year={2015} }
@mastersthesis{bartek2015, address={Praha}, type={Master's thesis}, title={Minimum representations of Boolean functions defined by multiple intervals}, url={http://hdl.handle.net/20.500.11956/62638}, author={Bártek, Filip}, year={2015}, school={Charles University} }

% Preprint: https://arxiv.org/abs/2403.04017
@inproceedings{DBLP:conf/birthday/BlaauwbroekCGJK24,
  author       = {Lasse Blaauwbroek and
                  David M. Cerna and
                  Thibault Gauthier and
                  Jan Jakubův and
                  Cezary Kaliszyk and
                  Martin Suda and
                  Josef Urban},
  title        = {Learning Guided Automated Reasoning: {A} Brief Survey},
  booktitle    = {Logics and Type Systems in Theory and Practice - Essays Dedicated
                  to Herman Geuvers on The Occasion of His 60th Birthday},
  pages        = {54--83},
  year         = {2024},
  crossref     = {DBLP:conf/birthday/2024geuvers},
  url          = {https://arxiv.org/abs/2403.04017},
  doi          = {10.1007/978-3-031-61716-4_4},
  timestamp    = {Thu, 27 Jun 2024 17:04:11 +0200},
  biburl       = {https://dblp.org/rec/conf/birthday/BlaauwbroekCGJK24.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/birthday/2024geuvers,
  editor       = {Venanzio Capretta and
                  Robbert Krebbers and
                  Freek Wiedijk},
  title        = {Logics and Type Systems in Theory and Practice - Essays Dedicated
                  to Herman Geuvers on The Occasion of His 60th Birthday},
  series       = {Lecture Notes in Computer Science},
  volume       = {14560},
  publisher    = {Springer},
  year         = {2024},
  url          = {https://doi.org/10.1007/978-3-031-61716-4},
  doi          = {10.1007/978-3-031-61716-4},
  isbn         = {978-3-031-61715-7},
  timestamp    = {Thu, 08 Aug 2024 14:43:57 +0200},
  biburl       = {https://dblp.org/rec/conf/birthday/2024geuvers.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{Sut16,
	author       = {Geoff Sutcliffe},
	title        = {The {CADE} {ATP} System Competition - {CASC}},
	journal      = {{AI} Mag.},
	volume       = {37},
	number       = {2},
	pages        = {99--101},
	year         = {2016},
	url          = {https://doi.org/10.1609/aimag.v37i2.2620},
	doi          = {10.1609/AIMAG.V37I2.2620},
	timestamp    = {Fri, 09 Apr 2021 18:26:24 +0200},
	biburl       = {https://dblp.org/rec/journals/aim/Sutcliffe16.bib},
	bibsource    = {dblp computer science bibliography, https://dblp.org}
}

% Vampire
@inproceedings{DBLP:conf/cav/KovacsV13,
  author       = {Laura Kov{\'{a}}cs and
                  Andrei Voronkov},
  title        = {First-Order Theorem Proving and {Vampire}},
  booktitle    = {Computer Aided Verification - 25th International Conference, {CAV}
                  2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings},
  pages        = {1--35},
  year         = {2013},
  crossref     = {DBLP:conf/cav/2013},
  url          = {https://doi.org/10.1007/978-3-642-39799-8_1},
  doi          = {10.1007/978-3-642-39799-8_1},
  timestamp    = {Wed, 07 Dec 2022 23:12:58 +0100},
  biburl       = {https://dblp.org/rec/conf/cav/KovacsV13.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/cav/2013,
  editor       = {Natasha Sharygina and
                  Helmut Veith},
  title        = {Computer Aided Verification - 25th International Conference, {CAV}
                  2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {8044},
  publisher    = {Springer},
  year         = {2013},
  url          = {https://doi.org/10.1007/978-3-642-39799-8},
  doi          = {10.1007/978-3-642-39799-8},
  isbn         = {978-3-642-39798-1},
  timestamp    = {Fri, 05 May 2023 17:37:21 +0200},
  biburl       = {https://dblp.org/rec/conf/cav/2013.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

% SInE (Sumo Inference Engine)
% Axiom selection, premise selection
% http://www.cs.man.ac.uk/~hoderk/sine/
@inproceedings{DBLP:conf/cade/HoderV11,
  author       = {Kryštof Hoder and
                  Andrei Voronkov},
  title        = {Sine Qua Non for Large Theory Reasoning},
  booktitle    = {Automated Deduction - {CADE-23} - 23rd International Conference on
                  Automated Deduction, Wroclaw, Poland, July 31 - August 5, 2011. Proceedings},
  pages        = {299--314},
  year         = {2011},
  crossref     = {DBLP:conf/cade/2011},
  url          = {https://doi.org/10.1007/978-3-642-22438-6_23},
  doi          = {10.1007/978-3-642-22438-6_23},
  timestamp    = {Mon, 28 Aug 2023 21:17:45 +0200},
  biburl       = {https://dblp.org/rec/conf/cade/HoderV11.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/cade/2011,
  editor       = {Nikolaj S. Bj{\o}rner and
                  Viorica Sofronie{-}Stokkermans},
  title        = {Automated Deduction - {CADE-23} - 23rd International Conference on
                  Automated Deduction, Wroclaw, Poland, July 31 - August 5, 2011. Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {6803},
  publisher    = {Springer},
  year         = {2011},
  url          = {https://doi.org/10.1007/978-3-642-22438-6},
  doi          = {10.1007/978-3-642-22438-6},
  isbn         = {978-3-642-22437-9},
  timestamp    = {Mon, 10 Jun 2024 18:05:14 +0200},
  biburl       = {https://dblp.org/rec/conf/cade/2011.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

% Premise selection
@inproceedings{DBLP:conf/cade/KuhlweinLTUH12,
  author       = {Daniel K{\"{u}}hlwein and
                  Twan van Laarhoven and
                  Evgeni Tsivtsivadze and
                  Josef Urban and
                  Tom Heskes},
  title        = {Overview and Evaluation of Premise Selection Techniques for Large
                  Theory Mathematics},
  booktitle    = {Automated Reasoning - 6th International Joint Conference, {IJCAR}
                  2012, Manchester, UK, June 26-29, 2012. Proceedings},
  pages        = {378--392},
  year         = {2012},
  crossref     = {DBLP:conf/cade/2012},
  url          = {https://doi.org/10.1007/978-3-642-31365-3\_30},
  doi          = {10.1007/978-3-642-31365-3\_30},
  timestamp    = {Tue, 29 Dec 2020 18:38:28 +0100},
  biburl       = {https://dblp.org/rec/conf/cade/KuhlweinLTUH12.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/cade/2012,
  editor       = {Bernhard Gramlich and
                  Dale Miller and
                  Uli Sattler},
  title        = {Automated Reasoning - 6th International Joint Conference, {IJCAR}
                  2012, Manchester, UK, June 26-29, 2012. Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {7364},
  publisher    = {Springer},
  year         = {2012},
  url          = {https://doi.org/10.1007/978-3-642-31365-3},
  doi          = {10.1007/978-3-642-31365-3},
  isbn         = {978-3-642-31364-6},
  timestamp    = {Mon, 17 Feb 2025 12:59:03 +0100},
  biburl       = {https://dblp.org/rec/conf/cade/2012.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@book{DBLP:series/faia/336,
  editor       = {Armin Biere and
                  Marijn Heule and
                  Hans van Maaren and
                  Toby Walsh},
  title        = {Handbook of Satisfiability - Second Edition},
  series       = {Frontiers in Artificial Intelligence and Applications},
  volume       = {336},
  publisher    = {{IOS} Press},
  year         = {2021},
  url          = {https://doi.org/10.3233/FAIA336},
  doi          = {10.3233/FAIA336},
  isbn         = {978-1-64368-160-3},
  timestamp    = {Fri, 06 May 2022 08:03:54 +0200},
  biburl       = {https://dblp.org/rec/series/faia/336.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/cade/SchulzM16,
  author       = {Stephan Schulz and
                  Martin M{\"{o}}hrmann},
  title        = {Performance of Clause Selection Heuristics for Saturation-Based Theorem
                  Proving},
  booktitle    = {Automated Reasoning - 8th International Joint Conference, {IJCAR}
                  2016, Coimbra, Portugal, June 27 - July 2, 2016, Proceedings},
  pages        = {330--345},
  year         = {2016},
  crossref     = {DBLP:conf/cade/2016},
  url          = {https://doi.org/10.1007/978-3-319-40229-1_23},
  doi          = {10.1007/978-3-319-40229-1_23},
  timestamp    = {Mon, 26 Jun 2023 20:45:22 +0200},
  biburl       = {https://dblp.org/rec/conf/cade/SchulzM16.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

% E prover
@inproceedings{DBLP:conf/cade/0001CV19,
  author       = {Stephan Schulz and
                  Simon Cruanes and
                  Petar Vukmirović},
  title        = {Faster, Higher, Stronger: {E} 2.3},
  booktitle    = {Automated Deduction - {CADE} 27 - 27th International Conference on
                  Automated Deduction, Natal, Brazil, August 27-30, 2019, Proceedings},
  pages        = {495--507},
  year         = {2019},
  crossref     = {DBLP:conf/cade/2019},
  url          = {https://doi.org/10.1007/978-3-030-29436-6_29},
  doi          = {10.1007/978-3-030-29436-6_29},
  timestamp    = {Sat, 19 Oct 2019 20:28:03 +0200},
  biburl       = {https://dblp.org/rec/conf/cade/0001CV19.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

% E User Manual
% E 2.6 User Manual: http://wwwlehre.dhbw-stuttgart.de/~sschulz/WORK/E_DOWNLOAD/V_2.6/eprover.pdf
@Booklet{E-manual,
address = {Manchester},
author = {Schulz, Stephan},
issn = {2516-2314},
publisher = {EasyChair},
series = {EasyChair preprint},
title = {{E} 2.4 User Manual},
url = {https://easychair.org/publications/preprint/8dss},
year = {2020},
howpublished = {EasyChair preprint no. 2272},
number = 2272
}

@inproceedings{DBLP:conf/cade/WeidenbachDFKSW09,
  author       = {Christoph Weidenbach and
                  Dilyana Dimova and
                  Arnaud Fietzke and
                  Rohit Kumar and
                  Martin Suda and
                  Patrick Wischnewski},
  title        = {{SPASS} Version 3.5},
  booktitle    = {Automated Deduction - CADE-22, 22nd International Conference on Automated
                  Deduction, Montreal, Canada, August 2-7, 2009. Proceedings},
  pages        = {140--145},
  year         = {2009},
  crossref     = {DBLP:conf/cade/2009},
  url          = {https://doi.org/10.1007/978-3-642-02959-2_10},
  doi          = {10.1007/978-3-642-02959-2_10},
  timestamp    = {Mon, 03 Jan 2022 22:34:50 +0100},
  biburl       = {https://dblp.org/rec/conf/cade/WeidenbachDFKSW09.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/cade/2009,
  editor       = {Renate A. Schmidt},
  title        = {Automated Deduction - CADE-22, 22nd International Conference on Automated
                  Deduction, Montreal, Canada, August 2-7, 2009. Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {5663},
  publisher    = {Springer},
  year         = {2009},
  url          = {https://doi.org/10.1007/978-3-642-02959-2},
  doi          = {10.1007/978-3-642-02959-2},
  isbn         = {978-3-642-02958-5},
  timestamp    = {Wed, 31 Jul 2024 18:32:41 +0200},
  biburl       = {https://dblp.org/rec/conf/cade/2009.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/logcom/BachmairG94,
  author       = {Leo Bachmair and
                  Harald Ganzinger},
  title        = {Rewrite-Based Equational Theorem Proving with Selection and Simplification},
  journal      = {J. Log. Comput.},
  volume       = {4},
  number       = {3},
  pages        = {217--247},
  year         = {1994},
  url          = {https://doi.org/10.1093/logcom/4.3.217},
  doi          = {10.1093/LOGCOM/4.3.217},
  timestamp    = {Wed, 17 May 2017 14:25:56 +0200},
  biburl       = {https://dblp.org/rec/journals/logcom/BachmairG94.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/bsl/Ferreiros01,
  author       = {Jos{\'{e}} Ferreir{\'{o}}s},
  title        = {The road to modern logic - An interpretation},
  journal      = {Bull. Symb. Log.},
  volume       = {7},
  number       = {4},
  pages        = {441--484},
  year         = {2001},
  url          = {https://doi.org/10.2307/2687794},
  doi          = {10.2307/2687794},
  timestamp    = {Fri, 03 Jul 2020 17:55:57 +0200},
  biburl       = {https://dblp.org/rec/journals/bsl/Ferreiros01.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@incollection{DBLP:books/el/RV01/NonnengartW01,
  author       = {Andreas Nonnengart and
                  Christoph Weidenbach},
  title        = {Computing Small Clause Normal Forms},
  booktitle    = {Handbook of Automated Reasoning (in 2 volumes)},
  pages        = {335--367},
  year         = {2001},
  crossref     = {DBLP:books/el/RobinsonV01},
  url          = {https://doi.org/10.1016/b978-044450813-3/50008-4},
  doi          = {10.1016/B978-044450813-3/50008-4},
  timestamp    = {Thu, 25 Jul 2019 12:26:00 +0200},
  biburl       = {https://dblp.org/rec/books/el/RV01/NonnengartW01.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
@book{DBLP:books/el/RobinsonV01,
  editor       = {John Alan Robinson and
                  Andrei Voronkov},
  title        = {Handbook of Automated Reasoning (in 2 volumes)},
  publisher    = {Elsevier and {MIT} Press},
  year         = {2001},
  url          = {https://www.sciencedirect.com/book/9780444508133/handbook-of-automated-reasoning},
  isbn         = {0-444-50813-9},
  timestamp    = {Thu, 11 Jul 2024 16:27:25 +0200},
  biburl       = {https://dblp.org/rec/books/el/RobinsonV01.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/gcai/Urban15,
  author       = {Josef Urban},
  title        = {{BliStr}: The Blind Strategymaker},
  booktitle    = {Global Conference on Artificial Intelligence, {GCAI} 2015, Tbilisi,
                  Georgia, October 16-19, 2015},
  pages        = {312--319},
  year         = {2015},
  crossref     = {DBLP:conf/gcai/2015},
  url          = {https://doi.org/10.29007/8n7m},
  doi          = {10.29007/8n7m},
  timestamp    = {Sun, 15 Aug 2021 00:16:53 +0200},
  biburl       = {https://dblp.org/rec/conf/gcai/Urban15.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/gcai/SchaferS15,
  author       = {Simon Sch{\"{a}}fer and
                  Stephan Schulz},
  title        = {Breeding Theorem Proving Heuristics with Genetic Algorithms},
  booktitle    = {Global Conference on Artificial Intelligence, {GCAI} 2015, Tbilisi,
                  Georgia, October 16-19, 2015},
  pages        = {263--274},
  year         = {2015},
  crossref     = {DBLP:conf/gcai/2015},
  url          = {https://doi.org/10.29007/gms9},
  doi          = {10.29007/gms9},
  timestamp    = {Sun, 15 Aug 2021 00:16:53 +0200},
  biburl       = {https://dblp.org/rec/conf/gcai/SchaferS15.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/gcai/2015,
  editor       = {Georg Gottlob and
                  Geoff Sutcliffe and
                  Andrei Voronkov},
  title        = {Global Conference on Artificial Intelligence, {GCAI} 2015, Tbilisi,
                  Georgia, October 16-19, 2015},
  series       = {EPiC Series in Computing},
  volume       = {36},
  publisher    = {EasyChair},
  year         = {2015},
  url          = {https://easychair.org/publications/volume/GCAI_2015},
  timestamp    = {Sun, 07 May 2023 16:08:09 +0200},
  biburl       = {https://dblp.org/rec/conf/gcai/2015.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/cpp/JakubuvU17,
  author       = {Jan Jakubův and
                  Josef Urban},
  title        = {{BliStrTune}: hierarchical invention of theorem proving strategies},
  booktitle    = {Proceedings of the 6th {ACM} {SIGPLAN} Conference on Certified Programs
                  and Proofs, {CPP} 2017, Paris, France, January 16-17, 2017},
  pages        = {43--52},
  year         = {2017},
  crossref     = {DBLP:conf/cpp/2017},
  url          = {https://doi.org/10.1145/3018610.3018619},
  doi          = {10.1145/3018610.3018619},
  timestamp    = {Sun, 02 Jun 2019 21:18:45 +0200},
  biburl       = {https://dblp.org/rec/conf/cpp/JakubuvU17.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/cpp/2017,
  editor       = {Yves Bertot and
                  Viktor Vafeiadis},
  title        = {Proceedings of the 6th {ACM} {SIGPLAN} Conference on Certified Programs
                  and Proofs, {CPP} 2017, Paris, France, January 16-17, 2017},
  publisher    = {{ACM}},
  year         = {2017},
  url          = {https://doi.org/10.1145/3018610},
  doi          = {10.1145/3018610},
  isbn         = {978-1-4503-4705-1},
  timestamp    = {Fri, 11 Aug 2023 12:03:39 +0200},
  biburl       = {https://dblp.org/rec/conf/cpp/2017.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/jar/KuhlweinU15,
  author       = {Daniel K{\"{u}}hlwein and
                  Josef Urban},
  title        = {{MaLeS}: {A} Framework for Automatic Tuning of Automated Theorem Provers},
  journal      = {J. Autom. Reason.},
  volume       = {55},
  number       = {2},
  pages        = {91--116},
  year         = {2015},
  url          = {https://doi.org/10.1007/s10817-015-9329-1},
  doi          = {10.1007/s10817-015-9329-1},
  timestamp    = {Wed, 02 Sep 2020 13:30:01 +0200},
  biburl       = {https://dblp.org/rec/journals/jar/KuhlweinU15.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

% HOS-ML
@inproceedings{DBLP:conf/mkm/HoldenK21,
  author       = {Edvard K. Holden and
                  Konstantin Korovin},
  title        = {Heterogeneous Heuristic Optimisation and Scheduling for First-Order
                  Theorem Proving},
  booktitle    = {Intelligent Computer Mathematics - 14th International Conference,
                  {CICM} 2021, Timisoara, Romania, July 26-31, 2021, Proceedings},
  pages        = {107--123},
  year         = {2021},
  crossref     = {DBLP:conf/mkm/2021},
  url          = {https://doi.org/10.1007/978-3-030-81097-9_8},
  doi          = {10.1007/978-3-030-81097-9_8},
  timestamp    = {Thu, 29 Jul 2021 13:42:12 +0200},
  biburl       = {https://dblp.org/rec/conf/mkm/HoldenK21.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/mkm/2021,
  editor       = {Fairouz Kamareddine and
                  Claudio Sacerdoti Coen},
  title        = {Intelligent Computer Mathematics - 14th International Conference,
                  {CICM} 2021, Timisoara, Romania, July 26-31, 2021, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {12833},
  publisher    = {Springer},
  year         = {2021},
  url          = {https://doi.org/10.1007/978-3-030-81097-9},
  doi          = {10.1007/978-3-030-81097-9},
  isbn         = {978-3-030-81096-2},
  timestamp    = {Fri, 05 May 2023 18:07:50 +0200},
  biburl       = {https://dblp.org/rec/conf/mkm/2021.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@phdthesis{DBLP:books/daglib/0002958,
  author       = {Stephan Schulz},
  title        = {Learning search control knowledge for equational deduction},
  school       = {Technical University Munich, Germany},
  year         = {2000},
  url          = {https://d-nb.info/95899126X},
  isbn         = {978-3-89838-230-4},
  timestamp    = {Sat, 17 Jul 2021 09:02:06 +0200},
  biburl       = {https://dblp.org/rec/books/daglib/0002958.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/mkm/JakubuvU17,
  author       = {Jan Jakubův and
                  Josef Urban},
  title        = {{ENIGMA:} Efficient Learning-Based Inference Guiding Machine},
  booktitle    = {Intelligent Computer Mathematics - 10th International Conference,
                  {CICM} 2017, Edinburgh, UK, July 17-21, 2017, Proceedings},
  pages        = {292--302},
  year         = {2017},
  crossref     = {DBLP:conf/mkm/2017},
  url          = {https://doi.org/10.1007/978-3-319-62075-6_20},
  doi          = {10.1007/978-3-319-62075-6_20},
  timestamp    = {Mon, 31 Jan 2022 07:36:54 +0100},
  biburl       = {https://dblp.org/rec/conf/mkm/JakubuvU17.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/mkm/2017,
  editor       = {Herman Geuvers and
                  Matthew England and
                  Osman Hasan and
                  Florian Rabe and
                  Olaf Teschke},
  title        = {Intelligent Computer Mathematics - 10th International Conference,
                  {CICM} 2017, Edinburgh, UK, July 17-21, 2017, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {10383},
  publisher    = {Springer},
  year         = {2017},
  url          = {https://doi.org/10.1007/978-3-319-62075-6},
  doi          = {10.1007/978-3-319-62075-6},
  isbn         = {978-3-319-62074-9},
  timestamp    = {Thu, 15 Aug 2024 16:27:35 +0200},
  biburl       = {https://dblp.org/rec/conf/mkm/2017.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

% Includes recursive NNs
@inproceedings{DBLP:conf/cade/ChvalovskyJ0U19,
  author       = {Karel Chvalovsk{\'{y}} and
                  Jan Jakubův and
                  Martin Suda and
                  Josef Urban},
  title        = {{ENIGMA-NG:} Efficient Neural and Gradient-Boosted Inference Guidance
                  for {E}},
  booktitle    = {Automated Deduction - {CADE} 27 - 27th International Conference on
                  Automated Deduction, Natal, Brazil, August 27-30, 2019, Proceedings},
  pages        = {197--215},
  year         = {2019},
  crossref     = {DBLP:conf/cade/2019},
  url          = {https://doi.org/10.1007/978-3-030-29436-6_12},
  doi          = {10.1007/978-3-030-29436-6_12},
  timestamp    = {Fri, 09 Apr 2021 18:50:53 +0200},
  biburl       = {https://dblp.org/rec/conf/cade/ChvalovskyJ0U19.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/cade/JakubuvCOP0U20,
  author       = {Jan Jakubův and
                  Karel Chvalovsk{\'{y}} and
                  Miroslav Olš{\'{a}}k and
                  Bartosz Piotrowski and
                  Martin Suda and
                  Josef Urban},
  title        = {{ENIGMA} Anonymous: Symbol-Independent Inference Guiding Machine (System
                  Description)},
  booktitle    = {Automated Reasoning - 10th International Joint Conference, {IJCAR}
                  2020, Paris, France, July 1-4, 2020, Proceedings, Part {II}},
  pages        = {448--463},
  year         = {2020},
  crossref     = {DBLP:conf/cade/2020-2},
  url          = {https://doi.org/10.1007/978-3-030-51054-1_29},
  doi          = {10.1007/978-3-030-51054-1_29},
  timestamp    = {Fri, 09 Apr 2021 18:50:52 +0200},
  biburl       = {https://dblp.org/rec/conf/cade/JakubuvCOP0U20.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/cade/2020-2,
  editor       = {Nicolas Peltier and
                  Viorica Sofronie{-}Stokkermans},
  title        = {Automated Reasoning - 10th International Joint Conference, {IJCAR}
                  2020, Paris, France, July 1-4, 2020, Proceedings, Part {II}},
  series       = {Lecture Notes in Computer Science},
  volume       = {12167},
  publisher    = {Springer},
  year         = {2020},
  url          = {https://doi.org/10.1007/978-3-030-51054-1},
  doi          = {10.1007/978-3-030-51054-1},
  isbn         = {978-3-030-51053-4},
  timestamp    = {Thu, 15 Aug 2024 16:38:30 +0200},
  biburl       = {https://dblp.org/rec/conf/cade/2020-2.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/iclr/EvansSAKG18,
  author       = {Richard Evans and
                  David Saxton and
                  David Amos and
                  Pushmeet Kohli and
                  Edward Grefenstette},
  title        = {Can Neural Networks Understand Logical Entailment?},
  booktitle    = {6th International Conference on Learning Representations, {ICLR} 2018,
                  Vancouver, BC, Canada, April 30 - May 3, 2018, Conference Track Proceedings},
  year         = {2018},
  crossref     = {DBLP:conf/iclr/2018},
  url          = {https://openreview.net/forum?id=SkZxCk-0Z},
  timestamp    = {Mon, 27 Jan 2020 16:21:19 +0100},
  biburl       = {https://dblp.org/rec/conf/iclr/EvansSAKG18.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/iclr/2018,
  title        = {6th International Conference on Learning Representations, {ICLR} 2018,
                  Vancouver, BC, Canada, April 30 - May 3, 2018, Conference Track Proceedings},
  publisher    = {OpenReview.net},
  year         = {2018},
  url          = {https://openreview.net/group?id=ICLR.cc/2018/Conference},
  timestamp    = {Thu, 15 Aug 2024 16:37:11 +0200},
  biburl       = {https://dblp.org/rec/conf/iclr/2018.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/nn/Schmidhuber15,
  author       = {J{\"{u}}rgen Schmidhuber},
  title        = {Deep learning in neural networks: An overview},
  journal      = {Neural Networks},
  volume       = {61},
  pages        = {85--117},
  year         = {2015},
  url          = {https://doi.org/10.1016/j.neunet.2014.09.003},
  doi          = {10.1016/J.NEUNET.2014.09.003},
  timestamp    = {Wed, 14 Nov 2018 10:30:16 +0100},
  biburl       = {https://dblp.org/rec/journals/nn/Schmidhuber15.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@book{DBLP:books/lib/HastieTF09,
  author       = {Trevor Hastie and
                  Robert Tibshirani and
                  Jerome H. Friedman},
  title        = {The Elements of Statistical Learning: Data Mining, Inference, and
                  Prediction, 2nd Edition},
  series       = {Springer Series in Statistics},
  publisher    = {Springer},
  year         = {2009},
  url          = {https://doi.org/10.1007/978-0-387-84858-7},
  doi          = {10.1007/978-0-387-84858-7},
  isbn         = {9780387848570},
  timestamp    = {Fri, 17 Jul 2020 16:12:43 +0200},
  biburl       = {https://dblp.org/rec/books/lib/HastieTF09.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/lpar/LoosISK17,
  author       = {Sarah M. Loos and
                  Geoffrey Irving and
                  Christian Szegedy and
                  Cezary Kaliszyk},
  title        = {Deep Network Guided Proof Search},
  booktitle    = {LPAR-21, 21st International Conference on Logic for Programming, Artificial
                  Intelligence and Reasoning, Maun, Botswana, May 7-12, 2017},
  pages        = {85--105},
  year         = {2017},
  crossref     = {DBLP:conf/lpar/2017},
  url          = {https://doi.org/10.29007/8mwc},
  doi          = {10.29007/8MWC},
  timestamp    = {Wed, 16 Mar 2022 23:55:58 +0100},
  biburl       = {https://dblp.org/rec/conf/lpar/LoosISK17.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/lpar/2017,
  editor       = {Thomas Eiter and
                  David Sands},
  title        = {LPAR-21, 21st International Conference on Logic for Programming, Artificial
                  Intelligence and Reasoning, Maun, Botswana, May 7-12, 2017},
  series       = {EPiC Series in Computing},
  volume       = {46},
  publisher    = {EasyChair},
  year         = {2017},
  url          = {https://easychair.org/publications/volume/LPAR-21},
  timestamp    = {Tue, 27 Aug 2024 17:00:50 +0200},
  biburl       = {https://dblp.org/rec/conf/lpar/2017.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/cade/000121a,
  author       = {Martin Suda},
  title        = {Improving {ENIGMA}-style Clause Selection while Learning From History},
  booktitle    = {Automated Deduction - {CADE} 28 - 28th International Conference on
                  Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings},
  pages        = {543--561},
  year         = {2021},
  crossref     = {DBLP:conf/cade/2021},
  url          = {https://doi.org/10.1007/978-3-030-79876-5_31},
  doi          = {10.1007/978-3-030-79876-5_31},
  timestamp    = {Thu, 29 Jul 2021 13:42:16 +0200},
  biburl       = {https://dblp.org/rec/conf/cade/000121a.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/frocos/Suda21,
  author       = {Martin Suda},
  title        = {Vampire with a Brain Is a Good {ITP} Hammer},
  booktitle    = {Frontiers of Combining Systems - 13th International Symposium, FroCoS
                  2021, Birmingham, UK, September 8-10, 2021, Proceedings},
  pages        = {192--209},
  year         = {2021},
  crossref     = {DBLP:conf/frocos/2021},
  url          = {https://doi.org/10.1007/978-3-030-86205-3_11},
  doi          = {10.1007/978-3-030-86205-3_11},
  timestamp    = {Thu, 16 Sep 2021 18:07:37 +0200},
  biburl       = {https://dblp.org/rec/conf/frocos/Suda21.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/frocos/2021,
  editor       = {Boris Konev and
                  Giles Reger},
  title        = {Frontiers of Combining Systems - 13th International Symposium, FroCoS
                  2021, Birmingham, UK, September 8-10, 2021, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {12941},
  publisher    = {Springer},
  year         = {2021},
  url          = {https://doi.org/10.1007/978-3-030-86205-3},
  doi          = {10.1007/978-3-030-86205-3},
  isbn         = {978-3-030-86204-6},
  timestamp    = {Tue, 27 Aug 2024 17:04:58 +0200},
  biburl       = {https://dblp.org/rec/conf/frocos/2021.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/jar/McCune97,
  author       = {William McCune},
  title        = {Solution of the Robbins Problem},
  journal      = {J. Autom. Reason.},
  volume       = {19},
  number       = {3},
  pages        = {263--276},
  year         = {1997},
  url          = {https://doi.org/10.1023/A:1005843212881},
  doi          = {10.1023/A:1005843212881},
  timestamp    = {Wed, 02 Sep 2020 13:29:54 +0200},
  biburl       = {https://dblp.org/rec/journals/jar/McCune97.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/birthday/KinyonVV13,
  author       = {Michael K. Kinyon and
                  Robert Veroff and
                  Petr Vojtechovsk{\'{y}}},
  title        = {Loops with Abelian Inner Mapping Groups: An Application of Automated
                  Deduction},
  booktitle    = {Automated Reasoning and Mathematics - Essays in Memory of William
                  W. McCune},
  pages        = {151--164},
  year         = {2013},
  crossref     = {DBLP:conf/birthday/2013mccune},
  url          = {https://doi.org/10.1007/978-3-642-36675-8\_8},
  doi          = {10.1007/978-3-642-36675-8\_8},
  timestamp    = {Sat, 19 Oct 2019 20:29:08 +0200},
  biburl       = {https://dblp.org/rec/conf/birthday/KinyonVV13.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/birthday/2013mccune,
  editor       = {Maria Paola Bonacina and
                  Mark E. Stickel},
  title        = {Automated Reasoning and Mathematics - Essays in Memory of William
                  W. McCune},
  series       = {Lecture Notes in Computer Science},
  volume       = {7788},
  publisher    = {Springer},
  year         = {2013},
  url          = {https://doi.org/10.1007/978-3-642-36675-8},
  doi          = {10.1007/978-3-642-36675-8},
  isbn         = {978-3-642-36674-1},
  timestamp    = {Tue, 03 Sep 2024 17:49:40 +0200},
  biburl       = {https://dblp.org/rec/conf/birthday/2013mccune.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@book{DBLP:series/lncs/10001,
  editor       = {Wolfgang Ahrendt and
                  Bernhard Beckert and
                  Richard Bubel and
                  Reiner H{\"{a}}hnle and
                  Peter H. Schmitt and
                  Mattias Ulbrich},
  title        = {Deductive Software Verification - The KeY Book - From Theory to Practice},
  series       = {Lecture Notes in Computer Science},
  volume       = {10001},
  publisher    = {Springer},
  year         = {2016},
  url          = {https://doi.org/10.1007/978-3-319-49812-6},
  doi          = {10.1007/978-3-319-49812-6},
  isbn         = {978-3-319-49811-9},
  timestamp    = {Tue, 14 May 2019 10:00:55 +0200},
  biburl       = {https://dblp.org/rec/series/lncs/10001.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/tcad/DSilvaKW08,
  author       = {Vijay Victor D'Silva and
                  Daniel Kroening and
                  Georg Weissenbacher},
  title        = {A Survey of Automated Techniques for Formal Software Verification},
  journal      = {{IEEE} Trans. Comput. Aided Des. Integr. Circuits Syst.},
  volume       = {27},
  number       = {7},
  pages        = {1165--1178},
  year         = {2008},
  url          = {https://doi.org/10.1109/TCAD.2008.923410},
  doi          = {10.1109/TCAD.2008.923410},
  timestamp    = {Tue, 16 Nov 2021 13:04:27 +0100},
  biburl       = {https://dblp.org/rec/journals/tcad/DSilvaKW08.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/logcom/PrakkenWBA15,
  author       = {Henry Prakken and
                  Adam Z. Wyner and
                  Trevor J. M. Bench{-}Capon and
                  Katie Atkinson},
  title        = {A formalization of argumentation schemes for legal case-based reasoning
                  in {ASPIC+}},
  journal      = {J. Log. Comput.},
  volume       = {25},
  number       = {5},
  pages        = {1141--1166},
  year         = {2015},
  url          = {https://doi.org/10.1093/logcom/ext010},
  doi          = {10.1093/LOGCOM/EXT010},
  timestamp    = {Fri, 30 Nov 2018 13:21:02 +0100},
  biburl       = {https://dblp.org/rec/journals/logcom/PrakkenWBA15.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/atal/LibalN21,
  author       = {Tomer Libal and
                  Tereza Novotn{\'{a}}},
  title        = {Towards Transparent Legal Formalization},
  booktitle    = {Explainable and Transparent {AI} and Multi-Agent Systems - Third International
                  Workshop, {EXTRAAMAS} 2021, Virtual Event, May 3-7, 2021, Revised
                  Selected Papers},
  pages        = {296--313},
  year         = {2021},
  crossref     = {DBLP:conf/atal/2021extraamas},
  url          = {https://doi.org/10.1007/978-3-030-82017-6\_18},
  doi          = {10.1007/978-3-030-82017-6\_18},
  timestamp    = {Mon, 05 Feb 2024 20:34:11 +0100},
  biburl       = {https://dblp.org/rec/conf/atal/LibalN21.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/atal/2021extraamas,
  editor       = {Davide Calvaresi and
                  Amro Najjar and
                  Michael Winikoff and
                  Kary Fr{\"{a}}mling},
  title        = {Explainable and Transparent {AI} and Multi-Agent Systems - Third International
                  Workshop, {EXTRAAMAS} 2021, Virtual Event, May 3-7, 2021, Revised
                  Selected Papers},
  series       = {Lecture Notes in Computer Science},
  volume       = {12688},
  publisher    = {Springer},
  year         = {2021},
  url          = {https://doi.org/10.1007/978-3-030-82017-6},
  doi          = {10.1007/978-3-030-82017-6},
  isbn         = {978-3-030-82016-9},
  timestamp    = {Wed, 04 Sep 2024 18:24:02 +0200},
  biburl       = {https://dblp.org/rec/conf/atal/2021extraamas.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/lp/BrandAAHS15,
  author       = {Amy Brand and
                  Liz Allen and
                  Micah Altman and
                  Marjorie M. K. Hlava and
                  Jo Scott},
  title        = {Beyond authorship: attribution, contribution, collaboration, and credit},
  journal      = {Learn. Publ.},
  volume       = {28},
  number       = {2},
  pages        = {151--155},
  year         = {2015},
  url          = {https://doi.org/10.1087/20150211},
  doi          = {10.1087/20150211},
  timestamp    = {Thu, 16 Jul 2020 16:39:10 +0200},
  biburl       = {https://dblp.org/rec/journals/lp/BrandAAHS15.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/cav/Voronkov14,
  author       = {Andrei Voronkov},
  title        = {{AVATAR:} The Architecture for First-Order Theorem Provers},
  booktitle    = {Computer Aided Verification - 26th International Conference, {CAV}
                  2014, Held as Part of the Vienna Summer of Logic, {VSL} 2014, Vienna,
                  Austria, July 18-22, 2014. Proceedings},
  pages        = {696--710},
  year         = {2014},
  crossref     = {DBLP:conf/cav/2014},
  url          = {https://doi.org/10.1007/978-3-319-08867-9\_46},
  doi          = {10.1007/978-3-319-08867-9\_46},
  timestamp    = {Mon, 03 Jan 2022 22:13:44 +0100},
  biburl       = {https://dblp.org/rec/conf/cav/Voronkov14.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/cav/2014,
  editor       = {Armin Biere and
                  Roderick Bloem},
  title        = {Computer Aided Verification - 26th International Conference, {CAV}
                  2014, Held as Part of the Vienna Summer of Logic, {VSL} 2014, Vienna,
                  Austria, July 18-22, 2014. Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {8559},
  publisher    = {Springer},
  year         = {2014},
  url          = {https://doi.org/10.1007/978-3-319-08867-9},
  doi          = {10.1007/978-3-319-08867-9},
  isbn         = {978-3-319-08866-2},
  timestamp    = {Mon, 07 Oct 2024 12:39:19 +0200},
  biburl       = {https://dblp.org/rec/conf/cav/2014.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

% Penalized average runtime (PAR)
@article{DBLP:journals/ai/BischlKKLMFHHLT16,
  author       = {Bernd Bischl and
                  Pascal Kerschke and
                  Lars Kotthoff and
                  Marius Lindauer and
                  Yuri Malitsky and
                  Alexandre Fr{\'{e}}chette and
                  Holger H. Hoos and
                  Frank Hutter and
                  Kevin Leyton{-}Brown and
                  Kevin Tierney and
                  Joaquin Vanschoren},
  title        = {{ASlib}: {A} benchmark library for algorithm selection},
  journal      = {Artif. Intell.},
  volume       = {237},
  pages        = {41--58},
  year         = {2016},
  url          = {https://doi.org/10.1016/j.artint.2016.04.003},
  doi          = {10.1016/J.ARTINT.2016.04.003},
  timestamp    = {Sat, 30 Sep 2023 10:00:51 +0200},
  biburl       = {https://dblp.org/rec/journals/ai/BischlKKLMFHHLT16.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/nips/KaliszykUMO18,
  author       = {Cezary Kaliszyk and
                  Josef Urban and
                  Henryk Michalewski and
                  Miroslav Ols{\'{a}}k},
  title        = {Reinforcement Learning of Theorem Proving},
  booktitle    = {Advances in Neural Information Processing Systems 31: Annual Conference
                  on Neural Information Processing Systems 2018, NeurIPS 2018, December
                  3-8, 2018, Montr{\'{e}}al, Canada},
  pages        = {8836--8847},
  year         = {2018},
  crossref     = {DBLP:conf/nips/2018},
  url          = {https://proceedings.neurips.cc/paper/2018/hash/55acf8539596d25624059980986aaa78-Abstract.html},
  timestamp    = {Mon, 16 May 2022 15:41:51 +0200},
  biburl       = {https://dblp.org/rec/conf/nips/KaliszykUMO18.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/nips/2018,
  editor       = {Samy Bengio and
                  Hanna M. Wallach and
                  Hugo Larochelle and
                  Kristen Grauman and
                  Nicol{\`{o}} Cesa{-}Bianchi and
                  Roman Garnett},
  title        = {Advances in Neural Information Processing Systems 31: Annual Conference
                  on Neural Information Processing Systems 2018, NeurIPS 2018, December
                  3-8, 2018, Montr{\'{e}}al, Canada},
  year         = {2018},
  url          = {https://proceedings.neurips.cc/paper/2018},
  timestamp    = {Tue, 08 Oct 2024 16:07:52 +0200},
  biburl       = {https://dblp.org/rec/conf/nips/2018.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

% SMBO
% SMAC
@inproceedings{DBLP:conf/lion/HutterHL11,
  author       = {Frank Hutter and
                  Holger H. Hoos and
                  Kevin Leyton{-}Brown},
  title        = {Sequential Model-Based Optimization for General Algorithm Configuration},
  booktitle    = {Learning and Intelligent Optimization - 5th International Conference,
                  {LION} 5, Rome, Italy, January 17-21, 2011. Selected Papers},
  pages        = {507--523},
  year         = {2011},
  crossref     = {DBLP:conf/lion/2011},
  url          = {https://doi.org/10.1007/978-3-642-25566-3\_40},
  doi          = {10.1007/978-3-642-25566-3\_40},
  timestamp    = {Sun, 02 Jun 2019 21:10:54 +0200},
  biburl       = {https://dblp.org/rec/conf/lion/HutterHL11.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/lion/2011,
  editor       = {Carlos A. Coello Coello},
  title        = {Learning and Intelligent Optimization - 5th International Conference,
                  {LION} 5, Rome, Italy, January 17-21, 2011. Selected Papers},
  series       = {Lecture Notes in Computer Science},
  volume       = {6683},
  publisher    = {Springer},
  year         = {2011},
  url          = {https://doi.org/10.1007/978-3-642-25566-3},
  doi          = {10.1007/978-3-642-25566-3},
  isbn         = {978-3-642-25565-6},
  timestamp    = {Tue, 08 Oct 2024 16:15:03 +0200},
  biburl       = {https://dblp.org/rec/conf/lion/2011.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

% https://tptp.org/CASC/J12/WWWFiles/DivisionSummary1.html
@article{doi:10.1177/30504554241305110,
author = {Geoff Sutcliffe},
title ={The 12th {IJCAR} Automated Theorem Proving System Competition--{CASC-J12}},
journal = {The European Journal on Artificial Intelligence},
volume = {38},
number = {1},
pages = {3-20},
year = {2025},
doi = {10.1177/30504554241305110},
URL = {https://doi.org/10.1177/30504554241305110},
eprint = {https://doi.org/10.1177/30504554241305110}
}

@article{DBLP:journals/aicom/SutcliffeD23,
  author       = {Geoff Sutcliffe and
                  Martin Desharnais},
  title        = {The 11th {IJCAR} automated theorem proving system competition - {CASC-J11}},
  journal      = {{AI} Commun.},
  volume       = {36},
  number       = {2},
  pages        = {73--91},
  year         = {2023},
  url          = {https://doi.org/10.3233/AIC-220244},
  doi          = {10.3233/AIC-220244},
  timestamp    = {Sun, 22 Oct 2023 11:16:06 +0200},
  biburl       = {https://dblp.org/rec/journals/aicom/SutcliffeD23.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@book{DBLP:books/daglib/0072413,
  author       = {Christos H. Papadimitriou},
  title        = {Computational complexity},
  publisher    = {Addison-Wesley},
  year         = {1994},
  isbn         = {978-0-201-53082-7},
  timestamp    = {Fri, 08 Apr 2011 18:21:01 +0200},
  biburl       = {https://dblp.org/rec/books/daglib/0072413.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@book{DBLP:books/daglib/0082098,
  author       = {Melvin Fitting},
  title        = {First-Order Logic and Automated Theorem Proving, Second Edition},
  series       = {Graduate Texts in Computer Science},
  publisher    = {Springer},
  year         = {1996},
  url          = {https://doi.org/10.1007/978-1-4612-2360-3},
  doi          = {10.1007/978-1-4612-2360-3},
  isbn         = {978-1-4612-7515-2},
  timestamp    = {Tue, 16 May 2017 14:01:34 +0200},
  biburl       = {https://dblp.org/rec/books/daglib/0082098.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@book{DBLP:books/daglib/0022394,
  author       = {John Harrison},
  title        = {Handbook of Practical Logic and Automated Reasoning},
  publisher    = {Cambridge University Press},
  year         = {2009},
  isbn         = {978-0-521-89957-4},
  timestamp    = {Thu, 05 Sep 2019 14:51:32 +0200},
  biburl       = {https://dblp.org/rec/books/daglib/0022394.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/ijcar/BhayatS24,
  author       = {Ahmed Bhayat and
                  Martin Suda},
  title        = {A Higher-Order {V}ampire (Short Paper)},
  booktitle    = {Automated Reasoning - 12th International Joint Conference, {IJCAR}
                  2024, Nancy, France, July 3-6, 2024, Proceedings, Part {I}},
  pages        = {75--85},
  year         = {2024},
  crossref     = {DBLP:conf/ijcar/2024-1},
  url          = {https://doi.org/10.1007/978-3-031-63498-7\_5},
  doi          = {10.1007/978-3-031-63498-7\_5},
  timestamp    = {Fri, 02 Aug 2024 21:41:23 +0200},
  biburl       = {https://dblp.org/rec/conf/ijcar/BhayatS24.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/jfrea/GrabowskiKN10,
  author       = {Adam Grabowski and
                  Artur Kornilowicz and
                  Adam Naumowicz},
  title        = {Mizar in a Nutshell},
  journal      = {J. Formaliz. Reason.},
  volume       = {3},
  number       = {2},
  pages        = {153--245},
  year         = {2010},
  url          = {https://doi.org/10.6092/issn.1972-5787/1980},
  doi          = {10.6092/ISSN.1972-5787/1980},
  timestamp    = {Thu, 24 Sep 2020 13:05:55 +0200},
  biburl       = {https://dblp.org/rec/journals/jfrea/GrabowskiKN10.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/jar/Urban06,
  author       = {Josef Urban},
  title        = {{MPTP} 0.2: Design, Implementation, and Initial Experiments},
  journal      = {J. Autom. Reason.},
  volume       = {37},
  number       = {1-2},
  pages        = {21--43},
  year         = {2006},
  url          = {https://doi.org/10.1007/s10817-006-9032-3},
  doi          = {10.1007/S10817-006-9032-3},
  timestamp    = {Wed, 02 Sep 2020 13:30:02 +0200},
  biburl       = {https://dblp.org/rec/journals/jar/Urban06.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/DesharnaisVBW22,
  author       = {Martin Desharnais and
                  Petar Vukmirovic and
                  Jasmin Blanchette and
                  Makarius Wenzel},
  title        = {Seventeen Provers Under the Hammer},
  booktitle    = {13th International Conference on Interactive Theorem Proving, {ITP}
                  2022, August 7-10, 2022, Haifa, Israel},
  pages        = {8:1--8:18},
  year         = {2022},
  crossref     = {DBLP:conf/itp/2022},
  url          = {https://doi.org/10.4230/LIPIcs.ITP.2022.8},
  doi          = {10.4230/LIPICS.ITP.2022.8},
  timestamp    = {Wed, 21 Aug 2024 22:46:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/DesharnaisVBW22.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/itp/2022,
  editor       = {June Andronick and
                  Leonardo de Moura},
  title        = {13th International Conference on Interactive Theorem Proving, {ITP}
                  2022, August 7-10, 2022, Haifa, Israel},
  series       = {LIPIcs},
  volume       = {237},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2022},
  url          = {https://www.dagstuhl.de/dagpub/978-3-95977-252-5},
  isbn         = {978-3-95977-252-5},
  timestamp    = {Wed, 04 Dec 2024 18:54:03 +0100},
  biburl       = {https://dblp.org/rec/conf/itp/2022.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/mkm/BlanchetteHMN15,
  author       = {Jasmin Christian Blanchette and
                  Max W. Haslbeck and
                  Daniel Matichuk and
                  Tobias Nipkow},
  title        = {Mining the Archive of Formal Proofs},
  booktitle    = {Intelligent Computer Mathematics - International Conference, {CICM}
                  2015, Washington, DC, USA, July 13-17, 2015, Proceedings},
  pages        = {3--17},
  year         = {2015},
  crossref     = {DBLP:conf/mkm/2015},
  url          = {https://doi.org/10.1007/978-3-319-20615-8\_1},
  doi          = {10.1007/978-3-319-20615-8\_1},
  timestamp    = {Mon, 28 Aug 2023 21:17:42 +0200},
  biburl       = {https://dblp.org/rec/conf/mkm/BlanchetteHMN15.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/mkm/2015,
  editor       = {Manfred Kerber and
                  Jacques Carette and
                  Cezary Kaliszyk and
                  Florian Rabe and
                  Volker Sorge},
  title        = {Intelligent Computer Mathematics - International Conference, {CICM}
                  2015, Washington, DC, USA, July 13-17, 2015, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {9150},
  publisher    = {Springer},
  year         = {2015},
  url          = {https://doi.org/10.1007/978-3-319-20615-8},
  doi          = {10.1007/978-3-319-20615-8},
  isbn         = {978-3-319-20614-1},
  timestamp    = {Wed, 04 Dec 2024 19:01:18 +0100},
  biburl       = {https://dblp.org/rec/conf/mkm/2015.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/ki/Steen20,
  author       = {Alexander Steen},
  title        = {Extensional Paramodulation for Higher-Order Logic and Its Effective
                  Implementation {Leo-III}},
  journal      = {K{\"{u}}nstliche Intell.},
  volume       = {34},
  number       = {1},
  pages        = {105--108},
  year         = {2020},
  url          = {https://doi.org/10.1007/s13218-019-00628-8},
  doi          = {10.1007/S13218-019-00628-8},
  timestamp    = {Tue, 14 Jul 2020 14:25:58 +0200},
  biburl       = {https://dblp.org/rec/journals/ki/Steen20.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/jar/VukmirovicBBCNT22,
  author       = {Petar Vukmirovic and
                  Alexander Bentkamp and
                  Jasmin Blanchette and
                  Simon Cruanes and
                  Visa Nummelin and
                  Sophie Tourret},
  title        = {Making Higher-Order Superposition Work},
  journal      = {J. Autom. Reason.},
  volume       = {66},
  number       = {4},
  pages        = {541--564},
  year         = {2022},
  url          = {https://doi.org/10.1007/s10817-021-09613-z},
  doi          = {10.1007/S10817-021-09613-Z},
  timestamp    = {Mon, 05 Dec 2022 13:34:02 +0100},
  biburl       = {https://dblp.org/rec/journals/jar/VukmirovicBBCNT22.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/cade/PeaseS07,
  author       = {Adam Pease and
                  Geoff Sutcliffe},
  title        = {First Order Reasoning on a Large Ontology},
  booktitle    = {Proceedings of the {CADE-21} Workshop on Empirically Successful Automated
                  Reasoning in Large Theories, Bremen, Germany, 17th July 2007},
  year         = {2007},
  crossref     = {DBLP:conf/cade/2007esarlt},
  url          = {https://ceur-ws.org/Vol-257/07\_Pease.pdf},
  timestamp    = {Fri, 10 Mar 2023 16:23:14 +0100},
  biburl       = {https://dblp.org/rec/conf/cade/PeaseS07.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/cade/2007esarlt,
  editor       = {Geoff Sutcliffe and
                  Josef Urban and
                  Stephan Schulz},
  title        = {Proceedings of the {CADE-21} Workshop on Empirically Successful Automated
                  Reasoning in Large Theories, Bremen, Germany, 17th July 2007},
  series       = {{CEUR} Workshop Proceedings},
  volume       = {257},
  publisher    = {CEUR-WS.org},
  year         = {2007},
  url          = {https://ceur-ws.org/Vol-257},
  urn          = {urn:nbn:de:0074-257-8},
  timestamp    = {Tue, 17 Dec 2024 16:58:07 +0100},
  biburl       = {https://dblp.org/rec/conf/cade/2007esarlt.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@misc{GenAITaxonomy,
  author = {Angelo Salatino and Fabrizio Fornari and Jelena Zdravkovic},
  title = {{GenAI} Usage Taxonomy},
  year = 2024,
  month = dec,
  day = 18,
  date = {2024-12-18},
  urldate = {2024-12-20},
  note = {[Online; accessed 20. Dec. 2024]},
  url = {https://ceur-ws.org/GenAI/Taxonomy.html}
}

@article{DBLP:journals/corr/cs-SC-0310056,
  author       = {William McCune},
  title        = {{OTTER} 3.3 Reference Manual},
  journal      = {CoRR},
  volume       = {cs.SC/0310056},
  year         = {2003},
  url          = {http://arxiv.org/abs/cs/0310056},
  doi          = {arXiv:cs/0310056},
  timestamp    = {Fri, 10 Jan 2020 12:57:58 +0100},
  biburl       = {https://dblp.org/rec/journals/corr/cs-SC-0310056.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

% Forward subsumption in Vampire
@article{DBLP:journals/jar/Voronkov95,
  author       = {Andrei Voronkov},
  title        = {The Anatomy of {V}ampire Implementing Bottom-up Procedures with Code
                  Trees},
  journal      = {J. Autom. Reason.},
  volume       = {15},
  number       = {2},
  pages        = {237--265},
  year         = {1995},
  url          = {https://doi.org/10.1007/BF00881918},
  doi          = {10.1007/BF00881918},
  timestamp    = {Wed, 02 Sep 2020 13:29:59 +0200},
  biburl       = {https://dblp.org/rec/journals/jar/Voronkov95.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@misc{CoreConfRanks,
  title = {{ICORE} Conference Portal},
  year = {2025},
  month = jan,
  day = 13,
  date = {2025-01-13},
  urldate = {2025-01-13},
  note = {[Online; accessed 13. Jan. 2025]},
  url = {https://portal.core.edu.au/conf-ranks}
}

% TPTP
@article{Sutcliffe2017,
author = {Sutcliffe, Geoff},
doi = {10.1007/s10817-017-9407-7},
issn = {0168-7433},
journal = {Journal of Automated Reasoning},
number = {4},
title = {The {TPTP} Problem Library and Associated Infrastructure},
volume = {59},
year = {2017}
}

@article{DBLP:journals/jair/SchedeBTWBHT22,
  author       = {Elias Schede and
                  Jasmin Brandt and
                  Alexander Tornede and
                  Marcel Wever and
                  Viktor Bengs and
                  Eyke H{\"{u}}llermeier and
                  Kevin Tierney},
  title        = {A Survey of Methods for Automated Algorithm Configuration},
  journal      = {J. Artif. Intell. Res.},
  volume       = {75},
  pages        = {425--487},
  year         = {2022},
  url          = {https://doi.org/10.1613/jair.1.13676},
  doi          = {10.1613/JAIR.1.13676},
  timestamp    = {Sun, 19 Jan 2025 14:44:27 +0100},
  biburl       = {https://dblp.org/rec/journals/jair/SchedeBTWBHT22.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/ec/KerschkeHNT19,
  author       = {Pascal Kerschke and
                  Holger H. Hoos and
                  Frank Neumann and
                  Heike Trautmann},
  title        = {Automated Algorithm Selection: Survey and Perspectives},
  journal      = {Evol. Comput.},
  volume       = {27},
  number       = {1},
  pages        = {3--45},
  year         = {2019},
  url          = {https://doi.org/10.1162/evco\_a\_00242},
  doi          = {10.1162/EVCO\_A\_00242},
  timestamp    = {Sat, 30 Sep 2023 10:12:01 +0200},
  biburl       = {https://dblp.org/rec/journals/ec/KerschkeHNT19.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/pami/AbdelazizCMACIK23,
  author       = {Ibrahim Abdelaziz and
                  Maxwell Crouse and
                  Bassem Makni and
                  Vernon Austel and
                  Cristina Cornelio and
                  Shajith Ikbal and
                  Pavan Kapanipathi and
                  Ndivhuwo Makondo and
                  Kavitha Srinivas and
                  Michael Witbrock and
                  Achille Fokoue},
  title        = {Learning to Guide a Saturation-Based Theorem Prover},
  journal      = {{IEEE} Trans. Pattern Anal. Mach. Intell.},
  volume       = {45},
  number       = {1},
  pages        = {738--751},
  year         = {2023},
  url          = {https://doi.org/10.1109/TPAMI.2022.3140382},
  doi          = {10.1109/TPAMI.2022.3140382},
  timestamp    = {Sun, 19 Jan 2025 13:41:50 +0100},
  biburl       = {https://dblp.org/rec/journals/pami/AbdelazizCMACIK23.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/cade/HoderR0V16,
  author       = {Krystof Hoder and
                  Giles Reger and
                  Martin Suda and
                  Andrei Voronkov},
  title        = {Selecting the Selection},
  booktitle    = {Automated Reasoning - 8th International Joint Conference, {IJCAR}
                  2016, Coimbra, Portugal, June 27 - July 2, 2016, Proceedings},
  pages        = {313--329},
  year         = {2016},
  crossref     = {DBLP:conf/cade/2016},
  url          = {https://doi.org/10.1007/978-3-319-40229-1\_22},
  doi          = {10.1007/978-3-319-40229-1\_22},
  timestamp    = {Mon, 26 Jun 2023 20:45:22 +0200},
  biburl       = {https://dblp.org/rec/conf/cade/HoderR0V16.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

% Common crossrefs
@proceedings{DBLP:conf/cade/2019,
  editor       = {Pascal Fontaine},
  title        = {Automated Deduction - {CADE} 27 - 27th International Conference on
                  Automated Deduction, Natal, Brazil, August 27-30, 2019, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {11716},
  publisher    = {Springer},
  year         = {2019},
  url          = {https://doi.org/10.1007/978-3-030-29436-6},
  doi          = {10.1007/978-3-030-29436-6},
  isbn         = {978-3-030-29435-9},
  timestamp    = {Thu, 15 Aug 2024 16:35:02 +0200},
  biburl       = {https://dblp.org/rec/conf/cade/2019.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/cade/2021,
  editor       = {Andr{\'{e}} Platzer and
                  Geoff Sutcliffe},
  title        = {Automated Deduction - {CADE} 28 - 28th International Conference on
                  Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {12699},
  publisher    = {Springer},
  year         = {2021},
  url          = {https://doi.org/10.1007/978-3-030-79876-5},
  doi          = {10.1007/978-3-030-79876-5},
  isbn         = {978-3-030-79875-8},
  timestamp    = {Tue, 27 Aug 2024 17:04:19 +0200},
  biburl       = {https://dblp.org/rec/conf/cade/2021.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/ijcar/2024-1,
  editor       = {Christoph Benzm{\"{u}}ller and
                  Marijn J. H. Heule and
                  Renate A. Schmidt},
  title        = {Automated Reasoning - 12th International Joint Conference, {IJCAR}
                  2024, Nancy, France, July 3-6, 2024, Proceedings, Part {I}},
  series       = {Lecture Notes in Computer Science},
  volume       = {14739},
  publisher    = {Springer},
  year         = {2024},
  url          = {https://doi.org/10.1007/978-3-031-63498-7},
  doi          = {10.1007/978-3-031-63498-7},
  isbn         = {978-3-031-63497-0},
  timestamp    = {Wed, 24 Jul 2024 13:09:27 +0200},
  biburl       = {https://dblp.org/rec/conf/ijcar/2024-1.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/cade/2016,
  editor       = {Nicola Olivetti and
                  Ashish Tiwari},
  title        = {Automated Reasoning - 8th International Joint Conference, {IJCAR}
                  2016, Coimbra, Portugal, June 27 - July 2, 2016, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {9706},
  publisher    = {Springer},
  year         = {2016},
  url          = {https://doi.org/10.1007/978-3-319-40229-1},
  doi          = {10.1007/978-3-319-40229-1},
  isbn         = {978-3-319-40228-4},
  timestamp    = {Mon, 03 Mar 2025 15:55:32 +0100},
  biburl       = {https://dblp.org/rec/conf/cade/2016.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}