@techreport(smtlib,
 author       = {Clark Barrett and Pascal Fontaine and Cesare Tinelli},
 year         = {2017},
 title        = {{The SMT-LIB Standard: Version 2.6}},
 type         = {Technical Report},
 institution  = {Department of Computer Science, The University of Iowa},
 note         = {Available at {\tt www.SMT-LIB.org}},
)
@book(boyerMoore,
 author       = {R. S. Boyer and J S. Moore},
 year         = {1979},
 title        = {A Computational Logic},
 publisher    = {Academic Press},
)
@inproceedings(speculate,
 author       = {Rudy Braquehais and Colin Runciman},
 year         = {2017},
 title        = {Speculate: discovering conditional equations and inequalities about black-box functions by reasoning from test results},
 booktitle    = {Proceedings of the 10th ACM SIGPLAN International Symposium on Haskell},
 pages        = {40--51},
 doi          = {10.1145/3156695.3122961},
)
@inproceedings(quickcheck,
 author       = {Koen Claessen and John Hughes},
 year         = {2000},
 title        = {{QuickCheck}: a lightweight tool for random testing of {Haskell} programs},
 booktitle    = {Proceedings of ICFP},
 pages        = {268--279},
 doi          = {10.1145/351240.351266},
)
@article(monadic-quickcheck,
 author       = {Koen Claessen and John Hughes},
 year         = {2002},
 title        = {Testing Monadic Code with QuickCheck},
 journal      = {SIGPLAN Notices},
 volume       = {37},
 number       = {12},
 pages        = {47\IeC{\textendash}59},
 doi          = {10.1145/636517.636527},
)
@inproceedings(hipspec,
 author       = {Koen Claessen and Moa Johansson and Dan Ros\'en and Nicholas Smallbone},
 year         = {2013},
 title        = {Automating Inductive Proofs using Theory Exploration},
 booktitle    = {Proceedings of the Conference on Automated Deduction (CADE)},
 series       = {LNCS},
 volume       = {7898},
 publisher    = {Springer},
 pages        = {392--406},
 doi          = {10.1007/978-3-642-38574-2_27},
)
@inproceedings(tip,
 author       = {Koen Claessen and Moa Johansson and Dan Ros\'en and Nicholas Smallbone},
 year         = {2015},
 title        = {{TIP}: Tons of Inductive Problems},
 booktitle    = {Conference on Intelligent Computer Mathematics},
 series       = {LNCS},
 volume       = {9150},
 publisher    = {Springer},
 pages        = {333--337},
 doi          = {10.1007/978-3-319-20615-8_23},
)
@inproceedings(HR,
 author       = {Simon Colton},
 year         = {2002},
 title        = {The {HR} Program for Theorem Generation},
 editor       = {Andrei Voronkov},
 booktitle    = {Automated Deduction---CADE-18},
 publisher    = {Springer Berlin Heidelberg},
 address      = {Berlin, Heidelberg},
 pages        = {285--289},
 doi          = {10.1007/3-540-45620-1_24},
)
@misc(isaplanner2,
 author       = {Lucas Dixon and Moa Johansson},
 year         = {2007},
 title        = {{IsaPlanner} 2: A Proof Planner for {Isabelle}},
 howpublished = {DReaM Technical Report (System description)},
)
@inproceedings(cohipster,
 author       = {S{\'o}lr{\'u}n Halla Einarsd{\'o}ttir and Moa Johansson and Johannes {\r A}man Pohjola},
 year         = {2018},
 title        = {Into the Infinite - Theory Exploration for Coinduction},
 booktitle    = {Proceedings of AISC 2018},
 pages        = {70--86},
 doi          = {10.1007/978-3-319-99957-9_5},
)
@misc(RoughSpec,
 author       = {S{\'o}lr{\'u}n Halla Einarsd{\'o}ttir and Nicholas Smallbone and Moa Johansson},
 year         = {2021},
 title        = {Template-based Theory Exploration: Discovering Properties of Functional Programs by Testing},
 note         = {Post-proceedings of IFL'20},
)
@article(graffiti,
 author       = {Siemion Fajtlowicz},
 year         = {1988},
 title        = {On conjectures of {Graffiti}},
 journal      = {Annals of Discrete Mathematics},
 volume       = {38},
 pages        = {113--118},
 doi          = {10.1016/S0167-5060(08)70776-3},
)
@inproceedings(vampind,
 author       = {M. Hajdu and P. Hozzova and L. Kovacs and J. Schoisswohl and A. Voronkov},
 year         = {2020},
 title        = {Induction with Generalization in Superposition Reasoning},
 booktitle    = {Intelligent Computer Mathematics. CICM 2020},
 series       = {LNCS},
 volume       = {12236},
 publisher    = {Springer},
 doi          = {10.1007/978-3-030-53518-6_8},
)
@inproceedings(proofpatternrec,
 author       = {Jonathan Heras and Ekaterina Komendantskaya and Moa Johansson and Ewen Maclean},
 year         = {2013},
 title        = {Proof-Pattern Recognition and Lemma Discovery in {ACL2}},
 booktitle    = {Proceedings of LPAR},
 doi          = {10.1007/978-3-642-45221-5_27},
)
@book(hudak,
 author       = {Paul Hudak},
 year         = {200},
 title        = {The {Haskell} School of Expression: Learning Functional Programming through Multimedia},
 publisher    = {Cambridge University Press},
 doi          = {10.1017/CBO9780511818073},
)
@article(productiveuse,
 author       = {Andrew Ireland and Alan Bundy},
 year         = {1996},
 title        = {Productive Use of Failure in Inductive Proof},
 journal      = {Journal of Automated Reasoning},
 volume       = {16},
 pages        = {79--111},
 doi          = {10.1007/BF00244460},
)
@inproceedings(hipster2,
 author       = {Moa Johansson},
 year         = {2017},
 title        = {Automated theory exploration for interactive theorem proving: {An} introduction to the {Hipster} system},
 booktitle    = {Proceedings of ITP},
 series       = {LNCS},
 volume       = {10499},
 publisher    = {Springer},
 pages        = {1--11},
 doi          = {10.1007/978-3-319-66107-0_1},
)
@article(isacosy,
 author       = {Moa Johansson and Lucas Dixon and Alan Bundy},
 year         = {2011},
 title        = {Conjecture Synthesis for Inductive Theories},
 journal      = {Journal of Automated Reasoning},
 volume       = {47},
 number       = {3},
 pages        = {251--289},
 doi          = {10.1007/s10817-010-9193-y},
)
@inproceedings(hipster,
 author       = {Moa Johansson and Dan Ros\'en and Nicholas Smallbone and Koen Claessen},
 year         = {2014},
 title        = {{Hipster}: Integrating Theory Exploration in a Proof Assistant},
 booktitle    = {Proceedings of CICM},
 publisher    = {Springer},
 pages        = {108--122},
 doi          = {10.1007/978-3-319-08434-3_9},
)
@phdthesis(AM,
 author       = {Douglas B. Lenat},
 year         = {1976},
 title        = {{AM}, an artificial intelligence approach to discovery in mathematics as heuristic search},
 school       = {Stanford University},
)
@article(mathsaid,
 author       = {R. L. McCasland and A. Bundy and P. F. Smith},
 year         = {2017},
 title        = {{MATHsAiD}: Automated mathematical theory exploration},
 journal      = {Applied Intelligence},
 doi          = {10.1007/s10489-017-0954-8},
)
@article(isascheme,
 author       = {Montano-Rivas, Omar and Roy McCasland and Lucas Dixon and Alan Bundy},
 year         = {2012},
 title        = {Scheme-based theorem discovery and concept invention},
 journal      = {Expert systems with applications},
 volume       = {39},
 number       = {2},
 pages        = {1637--1646},
 doi          = {10.1016/j.eswa.2011.06.055},
 url          = {https://hdl.handle.net/1842/6269},
)
@misc(rabe2021,
 author       = {Markus N. Rabe and Dennis Lee and Kshitij Bansal and Christian Szegedy},
 year         = {2021},
 title        = {Mathematical Reasoning via Self-supervised Skip-tree Training},
 note         = {Accepted for ICLR 2021, to appear.},
)
@mastersthesis(hopster,
 author       = {Juan Ricart},
 year         = {2019},
 title        = {{Hopster: Automated discovery of mathematical properties in HOL}},
 school       = {Chalmers University of Technology},
 url          = {https://hdl.handle.net/20.500.12380/300420},
)
@inproceedings(tip-tools,
 author       = {Dan Ros\'en and Nicholas Smallbone},
 year         = {2015},
 title        = {{TIP}: Tools for Inductive Provers},
 booktitle    = {Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR)},
 series       = {LNCS},
 volume       = {9450},
 publisher    = {Springer},
 pages        = {219--232},
 doi          = {10.1007/978-3-662-48899-7_16},
)
@article(quickspec,
 author       = {Nicholas Smallbone and Moa Johansson and Koen Claessen and Maximilian Algehed},
 year         = {2017},
 title        = {Quick specifications for the busy programmer},
 journal      = {Journal of Functional Programming},
 volume       = {27},
 doi          = {10.1017/S0956796817000090},
)
@inproceedings(zeno,
 author       = {Willam Sonnex and Sophia Drossopoulou and Susan Eisenbach},
 year         = {2012},
 title        = {{Zeno: An automated prover for properties of recursive datatypes}},
 booktitle    = {Proceedings of TACAS},
 publisher    = {Springer},
 pages        = {407--421},
 doi          = {10.1007/978-3-642-28756-5_28},
)
@inproceedings(urban2020,
 author       = {Josef Urban and Jakub\IeC{\r u}v, Jan},
 year         = {2020},
 title        = {First Neural Conjecturing Datasets and Experiments},
 booktitle    = {Proceedings of CICM},
 doi          = {10.1007/978-3-030-53518-6_24},
)