@book(BB05,
 author       = "D. Basin",
 year         = "2005",
 title        = "Rippling: Meta-level Guidance for Mathematical Reasoning",
 publisher    = "Cambridge University Press",
)
@book(Bishop,
 author       = "C. Bishop",
 year         = "2006",
 title        = "Pattern Recognition and Machine Learning",
 publisher    = "Springer",
)
@inproceedings(Brock96,
 author       = "B. Brock and M. Kaufmann and {J} S. Moore",
 year         = "1996",
 title        = "ACL2 Theorems about Commercial Microprocessors",
 booktitle    = "1st International Conference on Formal Methods in Computer-Aided Design (FMCAD'96)",
 series       = "LNCS",
 volume       = "1166",
 pages        = "275--293",
 doi          = "10.1007/BFb0031816",
)
@inproceedings(testingACL2,
 author       = "H. Chamarthi and P. Dillinger and M. Kaufmann and P. Manolios",
 year         = "2011",
 title        = "Integrating Testing and Interactive Theorem Proving",
 booktitle    = "10th International Workshop on the ACL2 Theorem Prover and its Applications (ACL2'11)",
 series       = "EPTCS",
 volume       = "70",
 pages        = "4--19",
 doi          = "10.4204/EPTCS.70.1",
)
@inproceedings(hipspec,
 author       = "K. Claessen",
 year         = "2013",
 title        = "Automating Inductive Proofs using Theory Exploration",
 booktitle    = "24th International Conference on Automated Deduction (CADE-24)",
 series       = "LNCS",
 volume       = "7898",
 pages        = "392--406",
 doi          = "10.1007/978-3-642-38574-2\_27",
)
@inproceedings(HR,
 author       = "S. Colton",
 year         = "2002",
 title        = "{The HR Program for Theorem Generation}",
 booktitle    = "18th International Conference on Automated Deduction (CADE-18)",
 series       = "LNCS",
 volume       = "2392",
 pages        = "285--289",
 doi          = "10.1007/3-540-45620-1\_24",
)
@misc(acl2books,
 author       = "J. Davis",
 title        = "{ACL2 Community Books}",
 note         = "\url {https://code.google.com/p/acl2-books/}",
)
@misc(xdocacl2,
 author       = "J. Davis",
 year         = "2009--2014",
 title        = "{XDOC Documentation System for ACL2}",
 note         = "\url {http://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/}",
)
@techreport(DFGS99,
 author       = "J. Denzinger and M. Fuchs and C. Goller and S. Schulz",
 year         = "1999",
 title        = "Learning from Previous Proof Experience: A Survey",
 type         = "Technical Report",
 institution  = "Technische Universitat Munchen",
)
@article(DenzingerS00,
 author       = "J. Denzinger and S. Schulz",
 year         = "2000",
 title        = "Automatic Acquisition of Search Control Knowledge from Multiple Proof Attempts",
 journal      = "Information and Computation",
 volume       = "162",
 number       = "1-2",
 pages        = "59--79",
 doi          = "10.1006/inco.1999.2857",
)
@inproceedings(EVF07,
 author       = "C. Eastlund and D. Vaillancourt and M. Felleisen",
 year         = "2007",
 title        = "{ACL2 for Freshmen: First Experiences}",
 booktitle    = "7th International Workshop on the ACL2 Theorem Prover and its Applications (ACL2'07)",
 series       = "ACM Press",
 pages        = "200--211",
)
@article(efficientACL2,
 author       = "D. Greve",
 year         = "2008",
 title        = "Efficient Execution in an Automated Reasoning Environment",
 journal      = "Journal of Functional Programming",
 volume       = "18",
 number       = "1",
 pages        = "15--46",
 doi          = "10.1017/S0956796807006338",
)
@article(Weka,
 author       = "M. Hall",
 year         = "2009",
 title        = "{The WEKA Data Mining Software: An Update}",
 journal      = "SIGKDD Explorations",
 volume       = "11",
 number       = "1",
 pages        = "10--18",
 doi          = "10.1145/1656274.1656278",
)
@misc(acl2ml,
 author       = "J. Heras and E. Komendantskaya",
 year         = "2013--2014",
 title        = "{ACL2(ml): downloadable programs, manual, examples}",
 note         = "\url {http://staff.computing.dundee.ac.uk/katya/ACL2ml}",
)
@inproceedings(lpar13,
 author       = "J. Heras and E. Komendantskaya and M. Johansson and E. Maclean",
 year         = "2013",
 title        = "{Proof-Pattern Recognition and Lemma Discovery in ACL2}",
 booktitle    = "19th Logic for Programming Artificial Intelligence and Reasoning (LPAR-19)",
 series       = "LNCS",
 volume       = "8312",
 pages        = "389--406",
 doi          = "10.1007/978-3-642-45221-5\_27",
)
@inproceedings(HLW12,
 author       = "S. Hetzl and A. Leitsch and D. Weller",
 year         = "2012",
 title        = "Towards Algorithm Cut-Introduction",
 booktitle    = "18th Logic for Programming Artificial Intelligence and Reasoning (LPAR-18)",
 series       = "LNCS",
 volume       = "7180",
 pages        = "228--242",
 doi          = "10.1007/978-3-642-28717-6\_19",
)
@article(JDB11,
 author       = "M. Johansson and L. Dixon and A. 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",
)
@book(KMM00,
 editor       = "M. Kaufmann and P. Manolios and {J S. Moore}",
 year         = "2000",
 title        = "Computer-Aided Reasoning: ACL2 Case Studies",
 publisher    = "Kluwer Academic Publishers",
 doi          = "10.1007/978-1-4757-3188-0",
)
@book(KMM00-1,
 editor       = "M. Kaufmann and P. Manolios and {J} S. Moore",
 year         = "2000",
 title        = "Computer-Aided Reasoning: An approach",
 publisher    = "Kluwer Academic Publishers",
 doi          = "10.1007/978-1-4615-4449-4",
)
@inproceedings(KuhlweinLTUH12,
 author       = "D. K{\"u}hlwein and T. van Laarhoven and E. Tsivtsivadze and J. Urban and T. Heskes",
 year         = "2012",
 title        = "Overview and Evaluation of Premise Selection Techniques for Large Theory Mathematics",
 booktitle    = "6th International Joint Conference on Automated Reasoning (IJCAR'12)",
 series       = "LNCS",
 volume       = "7364",
 pages        = "378--392",
 doi          = "10.1007/978-3-642-31365-3\_30",
)
@inproceedings(mathsaid,
 author       = "R. L. McCasland and A. Bundy and P. F. Smith",
 year         = "2006",
 title        = "Ascertaining Mathematical Theorems",
 booktitle    = "12th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning (Calculemus 2005)",
 series       = "ENTCS",
 volume       = "151",
 pages        = "21--38",
 doi          = "10.1016/j.entcs.2005.11.021",
)
@article(montano2012,
 author       = "O. Montano-Rivas and R. Mccasland and L. Dixon and A. 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",
)
@article(JFP:1381480,
 author       = "R. Page",
 year         = "2007",
 title        = "Engineering Software Correctness",
 journal      = "Journal of Functional Programming",
 volume       = "17",
 number       = "6",
 pages        = "675--686",
 doi          = "10.1017/S095679680700634X",
)
@inproceedings(TsivtsivadzeUGH11,
 author       = "E. Tsivtsivadze and J. Urban and H. Geuvers and T. Heskes",
 year         = "2011",
 title        = "Semantic Graph Kernels for Automated Reasoning",
 booktitle    = "SIAM Conference on Data Mining (SDM'11)",
 publisher    = "SIAM / Omnipress",
 pages        = "795--803",
 doi          = "10.1137/1.9781611972818.68",
)
@inproceedings(UrbanSPV08,
 author       = "J. Urban and G. Sutcliffe and P. Pudl{\'a}k and J. Vyskocil",
 year         = "2008",
 title        = "{MaLARea SG1- Machine Learner for Automated Reasoning with Semantic Guidance}",
 booktitle    = "4th International Joint Conference on Automated Reasoning (IJCAR'08)",
 series       = "LNCS",
 volume       = "5195",
 pages        = "441--456",
 doi          = "10.1007/978-3-540-71070-7\_37",
)
@misc(WK14,
 author       = "N. Wetzler and M. Kaufmann",
 year         = "2014",
 title        = "{Remove-hyps and Writing Utilities with Make-event}",
 note         = "ACL2 Theorem Proving Seminar. University of Texas",
)