@article(Aubin79,
 author       = {Raymond Aubin},
 year         = {1979},
 title        = {Mechanizing Structural Induction Part {II:} Strategies},
 journal      = {Theor. Comput. Sci.},
 volume       = {9},
 pages        = {347--362},
 doi          = {10.1016/0304-3975(79)90035-5},
)
@inproceedings(BakerIrelandSmaill92,
 author       = {Siani Baker and Andrew Ireland and Alan Smaill},
 year         = {1992},
 title        = {On the Use of the Constructive Omega-Rule within Automated Deduction},
 booktitle    = {LPAR'92},
 series       = {Lecture Notes in Computer Science},
 volume       = {624},
 publisher    = {Springer},
 pages        = {214--225},
 doi          = {10.1007/BFb0013063},
)
@inproceedings(Zipperposition,
 author       = {Alexander Bentkamp and Jasmin Christian Blanchette and Simon Cruanes and Uwe Waldmann},
 year         = {2018},
 title        = {Superposition for Lambda-Free Higher-Order Logic},
 booktitle    = {{IJCAR}},
 series       = {Lecture Notes in Computer Science},
 volume       = {10900},
 publisher    = {Springer},
 pages        = {28--46},
 doi          = {10.1007/978-3-319-94205-6\_3},
)
@inproceedings(BhayatR20a,
 author       = {Ahmed Bhayat and Giles Reger},
 year         = {2020},
 title        = {A Combinator-Based Superposition Calculus for Higher-Order Logic},
 booktitle    = {{IJCAR}},
 series       = {Lecture Notes in Computer Science},
 volume       = {12166},
 publisher    = {Springer},
 pages        = {278--296},
 doi          = {10.1007/978-3-030-51074-9\_16},
)
@inproceedings(BhayatR20b,
 author       = {Ahmed Bhayat and Giles Reger},
 year         = {2020},
 title        = {A Polymorphic Vampire - (Short Paper)},
 booktitle    = {{IJCAR}},
 series       = {Lecture Notes in Computer Science},
 volume       = {12167},
 publisher    = {Springer},
 pages        = {361--368},
 doi          = {10.1007/978-3-030-51054-1\_21},
)
@inproceedings(HipSpec,
 author       = {Koen Claessen and Moa Johansson and Dan Ros{\'{e}}n and Nicholas Smallbone},
 year         = {2012},
 title        = {HipSpec: Automating Inductive Proofs of Program Properties},
 booktitle    = {ATx'12/WInG'12},
 series       = {EPiC Series in Computing},
 volume       = {17},
 publisher    = {EasyChair},
 pages        = {16--25},
 url          = {https://easychair.org/publications/paper/Kb7},
)
@inproceedings(Maffei18,
 author       = {V{\'{e}}ronique Cortier and Niklas Grimm and Joseph Lallemand and Matteo Maffei},
 year         = {2018},
 title        = {Equivalence Properties by Typing in Cryptographic Branching Protocols},
 booktitle    = {{POST}},
 series       = {Lecture Notes in Computer Science},
 volume       = {10804},
 publisher    = {Springer},
 pages        = {160--187},
 doi          = {10.1007/978-3-319-89722-6\_7},
)
@inproceedings(Cruanes17,
 author       = {Simon Cruanes},
 year         = {2017},
 title        = {Superposition with Structural Induction},
 booktitle    = {FroCoS},
 series       = {Lecture Notes in Computer Science},
 volume       = {10483},
 publisher    = {Springer},
 pages        = {172--188},
 doi          = {10.1007/978-3-319-66167-4\_10},
)
@article(EchenimP20,
 author       = {Mnacho Echenim and Nicolas Peltier},
 year         = {2020},
 title        = {Combining Induction and Saturation-Based Theorem Proving},
 journal      = {J. Autom. Reason.},
 volume       = {64},
 number       = {2},
 pages        = {253--294},
 doi          = {10.1007/s10817-019-09519-x},
)
@inproceedings(Sagiv19,
 author       = {Yotam M. Y. Feldman and James R. Wilcox and Sharon Shoham and Mooly Sagiv},
 year         = {2019},
 title        = {Inferring Inductive Invariants from Phase Structures},
 booktitle    = {{CAV}},
 series       = {Lecture Notes in Computer Science},
 volume       = {11562},
 publisher    = {Springer},
 pages        = {405--425},
 doi          = {10.1007/978-3-030-25543-5\_23},
)
@article(KovacsFMCAD20,
 author       = {Pamina Georgiou and Bernhard Gleiss and Laura Kov{\'{a}}cs},
 year         = {2020},
 title        = {Trace Logic for Inductive Loop Reasoning},
 journal      = {CoRR},
 volume       = {abs/2008.01387},
 doi          = {10.34727/2020/isbn.978-3-85448-042-6\_33},
)
@inproceedings(InductionWithGeneralization20,
 author       = {M{\'{a}}rton Hajd{\'{u}} and Petra Hozzov{\'{a}} and Laura Kov{\'{a}}cs and Johannes Schoisswohl and Andrei Voronkov},
 year         = {2020},
 title        = {Induction with Generalization in Superposition Reasoning},
 booktitle    = {{CICM}},
 series       = {Lecture Notes in Computer Science},
 volume       = {12236},
 publisher    = {Springer},
 pages        = {123--137},
 doi          = {10.1007/978-3-030-53518-6\_8},
)
@inproceedings(HoderBM11,
 author       = {Krystof Hoder and Bj{\o}rner, Nikolaj and Leonardo Mendon{\c{c}}a de Moura},
 year         = {2011},
 title        = {\emph{{$\mu$}Z}- An Efficient Engine for Fixed Points with Constraints},
 booktitle    = {{CAV}},
 series       = {Lecture Notes in Computer Science},
 volume       = {6806},
 publisher    = {Springer},
 pages        = {457--462},
 doi          = {10.1007/978-3-642-22110-1\_36},
)
@inproceedings(Dedukti,
 author       = {Gabriel Hondet and Fr{\'{e}}d{\'{e}}ric Blanqui},
 year         = {2020},
 title        = {The New Rewriting Engine of Dedukti (System Description)},
 editor       = {Zena M. Ariola},
 booktitle    = {{FSCD}},
 series       = {LIPIcs},
 volume       = {167},
 publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
 pages        = {35:1--35:16},
 doi          = {10.4230/LIPIcs.FSCD.2020.35},
)
@book(Horsten11,
 author       = {Leon Horsten},
 year         = {2011},
 title        = {The Tarskian Turn: Deflationism and Axiomatic Truth},
 series       = {Mit Press},
 publisher    = {MIT Press},
 doi          = {10.7551/mitpress/9780262015868.001.0001},
)
@inproceedings(KersaniP13,
 author       = {Abdelkader Kersani and Nicolas Peltier},
 year         = {2013},
 title        = {Combining Superposition and Induction: {A} Practical Realization},
 booktitle    = {FroCoS},
 series       = {Lecture Notes in Computer Science},
 volume       = {8152},
 publisher    = {Springer},
 pages        = {7--22},
 doi          = {10.1007/978-3-642-40885-4\_2},
)
@inproceedings(FOOLKotelnikovKRV16,
 author       = {Evgenii Kotelnikov and Laura Kov{\'{a}}cs and Giles Reger and Andrei Voronkov},
 year         = {2016},
 title        = {The vampire and the {FOOL}},
 booktitle    = {CPP},
 publisher    = {{ACM}},
 pages        = {37--48},
 doi          = {10.1145/2854065.2854071},
)
@inproceedings(POPL17Kovacs,
 author       = {Laura Kov{\'{a}}cs and Simon Robillard and Andrei Voronkov},
 year         = {2017},
 title        = {Coming to terms with quantified reasoning},
 booktitle    = {{POPL}},
 publisher    = {{ACM}},
 pages        = {260--270},
 doi          = {10.1145/3009837.3009887},
)
@inproceedings(Vampire13,
 author       = {Laura Kov{\'{a}}cs and Andrei Voronkov},
 year         = {2013},
 title        = {First-Order Theorem Proving and Vampire},
 booktitle    = {{CAV}},
 series       = {Lecture Notes in Computer Science},
 volume       = {8044},
 publisher    = {Springer},
 pages        = {1--35},
 doi          = {10.1007/978-3-642-39799-8\_1},
)
@inproceedings(Leino12,
 author       = {K. Rustan M. Leino},
 year         = {2012},
 title        = {Automating Induction with an {SMT} Solver},
 booktitle    = {{VMCAI}},
 series       = {Lecture Notes in Computer Science},
 volume       = {7148},
 publisher    = {Springer},
 pages        = {315--331},
 doi          = {10.1007/978-3-642-27940-9\_21},
)
@article(Moore19,
 author       = {J. Strother Moore},
 year         = {2019},
 title        = {Milestones from the Pure Lisp theorem prover to {ACL2}},
 journal      = {Formal Aspects Comput.},
 volume       = {31},
 number       = {6},
 pages        = {699--732},
 doi          = {10.1007/s00165-019-00490-3},
)
@inproceedings(PickFG20,
 author       = {Lauren Pick and Grigory Fedyukovich and Aarti Gupta},
 year         = {2020},
 title        = {Automating Modular Verification of Secure Information Flow},
 booktitle    = {{FMCAD}},
 publisher    = {{IEEE}},
 pages        = {158--168},
 doi          = {10.34727/2020/isbn.978-3-85448-042-6\_23},
)
@inproceedings(TheoryInstUWA18,
 author       = {Giles Reger and Martin Suda and Andrei Voronkov},
 year         = {2018},
 title        = {Unification with Abstraction and Theory Instantiation in Saturation-Based Reasoning},
 booktitle    = {{TACAS}},
 series       = {Lecture Notes in Computer Science},
 volume       = {10805},
 publisher    = {Springer},
 pages        = {3--22},
 doi          = {10.1007/978-3-319-89960-2\_1},
)
@inproceedings(VampireInduction19,
 author       = {Giles Reger and Andrei Voronkov},
 year         = {2019},
 title        = {Induction in Saturation-Based Proof Search},
 booktitle    = {{CADE}},
 series       = {Lecture Notes in Computer Science},
 volume       = {11716},
 publisher    = {Springer},
 pages        = {477--494},
 doi          = {10.1007/978-3-030-29436-6\_28},
)
@inproceedings(ReynoldsK15,
 author       = {Andrew Reynolds and Viktor Kuncak},
 year         = {2015},
 title        = {Induction for {SMT} Solvers},
 booktitle    = {{VMCAI}},
 series       = {Lecture Notes in Computer Science},
 volume       = {8931},
 publisher    = {Springer},
 pages        = {80--98},
 doi          = {10.1007/978-3-662-46081-8\_5},
)
@misc(automatingInductionByReflection_extended,
 author       = {Johannes Schoisswohl and Laura Kovacs},
 year         = {2021},
 title        = {Automating Induction by Reflection},
 url          = {https://arxiv.org/abs/2106.05066},
)
@inproceedings(AVATAR14,
 author       = {Andrei Voronkov},
 year         = {2014},
 title        = {{AVATAR:} The Architecture for First-Order Theorem Provers},
 booktitle    = {{CAV}},
 series       = {Lecture Notes in Computer Science},
 volume       = {8559},
 publisher    = {Springer},
 pages        = {696--710},
 doi          = {10.1007/978-3-319-08867-9\_46},
)