@book(EventbBook,
 author       = "J-R. Abrial",
 year         = "2010",
 title        = "Modeling in Event-B - System and Software Engineering",
 publisher    = "Cambridge University Press",
)
@article(Rodin,
 author       = "J-R. Abrial and M. Butler and S. Hallerstede and T. Hoang and F. Mehta and L. Voisin",
 year         = "2010",
 title        = "Rodin: an open toolset for modelling and reasoning in {Event-B}",
 journal      = "STTT",
 volume       = "12",
 number       = "6",
 pages        = "447--466",
 doi          = "10.1007/s10009-010-0145-y",
)
@article(Mondex,
 author       = "M. Butler and D. Yadav",
 year         = "2008",
 title        = "An incremental development of the Mondex system in Event-B",
 journal      = "Formal Aspects of Computing",
 volume       = "20",
 number       = "1",
 pages        = "61--77",
 doi          = "10.1007/s00165-007-0061-4",
)
@book(colton:book,
 author       = "S. Colton",
 year         = "2002",
 title        = "Automated Theory Formation in Pure Mathematics",
 publisher    = "Springer-Verlag",
)
@inproceedings(ColtonICML00,
 author       = "S. Colton and A. Bundy and T. Walsh",
 year         = "2000",
 title        = "Automatic Identification of Mathematical Concepts",
 booktitle    = "17th International Conference on Machine Learning",
 publisher    = "Morgan Kaufmann",
 address      = "San Francisco, USA",
 pages        = "183--190",
)
@inproceedings(colton:00,
 author       = "S. Colton and A. Bundy and T. Walsh",
 year         = "2000",
 title        = "Automatic invention of integer sequences",
 booktitle    = "16th {IJCAI}",
 pages        = "786--791",
)
@article(colton:interestingness,
 author       = "S. Colton and A. Bundy and T. Walsh",
 year         = "2000",
 title        = "On the Notion of Interestingness in Automated Mathematical Discovery",
 journal      = "International Journal of Human Computer Studies",
 volume       = "53",
 number       = "3",
 pages        = "351--375",
 doi          = "10.1006/ijhc.2000.0394",
)
@inproceedings(colton:cp01,
 author       = "S. Colton and I. Miguel",
 year         = "2001",
 title        = "Constraint Generation via Automated Theory Formation",
 booktitle    = "7th International Conference on the Principles and Practice of Constraint Programming",
 doi          = "10.1007/3-540-45578-7\_42",
)
@article(ErnstPGMPTX2007,
 author       = "M. Ernst and J. Perkins and P. Guo and S. McCamant and C. Pacheco and M. Tschantz and C. Xiao",
 year         = "2007",
 title        = "The {Daikon} system for dynamic detection of likely invariants",
 journal      = "Science of Computer Programming",
 volume       = "69",
 number       = "1--3",
 pages        = "35--45",
 doi          = "10.1016/j.scico.2007.01.015",
)
@article(IrelandGrovLlanoButler10,
 author       = "A. Ireland and G. Grov and M. Llano and M. Butler",
 year         = "2011",
 title        = "{R}easoned {M}odelling {C}ritics: {T}urning {F}ailed {P}roofs into {M}odelling {G}uidance",
 journal      = "Science of Computer Programming",
 doi          = "10.1016/j.scico.2011.03.006",
)
@inproceedings(JoDiBu10b,
 author       = "M. Johansson and L. Dixon and A. Bundy",
 year         = "2010",
 title        = "Case-Analysis for Rippling and Inductive Proof",
 booktitle    = "1st International Conference on Interactive Theorem Proving",
 series       = "LNCS",
 volume       = "6127",
 publisher    = "Springer",
 pages        = "291--306",
 doi          = "10.1007/978-3-642-14052-5\_21",
)
@phdthesis(lenat76,
 author       = "D. Lenat",
 year         = "1976",
 title        = "AM: An Artificial Intelligence approach to discovery in mathematics",
 school       = "Stanford University",
)
@article(lenat83,
 author       = "D. Lenat",
 year         = "1983",
 title        = "Eurisko: A program which learns new heuristics and domain concepts.",
 journal      = "Artificial Intelligence",
 volume       = "21",
 doi          = "10.1016/S0004-3702(83)80005-8",
)
@inproceedings(ProB03,
 author       = "M. Leuschel and M. Butler",
 year         = "2003",
 title        = "ProB: A Model Checker for B",
 booktitle    = "International Symposium of Formal Methods Europe",
 series       = "LNCS",
 volume       = "2805",
 publisher    = "Springer",
 pages        = "855--874",
 doi          = "10.1007/978-3-540-45236-2\_46",
)
@article(afm10,
 author       = "M. Llano and G. Grov and A. Ireland",
 year         = "2010",
 title        = "Automatic Guidance for Refinement Based Formal Methods",
 journal      = "5th workshop on Automated Formal Methods (AFM`10), a satellite workshop of the 22nd International Conference on Computer Aided Verification (CAV`10).",
 note         = "Also available via: School of Mathematical and Computer Sciences, Heriot-Watt University, Technical Report HW-MACS-TR-0076; School of Informatics, University of Edinburgh, Report EDI-INF-RR-1371",
)
@inproceedings(Maclean2009:WING,
 author       = "E. Maclean and A. Ireland and L. Dixon and R. Atkey",
 year         = "2009",
 title        = "Refinement and Term Synthesis in Loop Invariant Generation",
 booktitle    = "2nd International Workshop on Invariant Generation (WING'09), a satellite workshop of ETAPS'09",
)
@incollection(mcca-bund-aute-at65,
 author       = "R. McCasland and A. Bundy and S. Autexier",
 year         = "2007",
 title        = "Automated Discovery of Inductive Theorems",
 booktitle    = "From Insight to Proof: Festschrift in Honour of Andrzej Trybulec",
 series       = "Studies in Logic, Grammar and Rhetoric",
 volume       = "10(23)",
 publisher    = "University of Bia{\l }ystok",
 pages        = "135--149",
)
@article(Otter,
 author       = "W. McCune",
 year         = "2003",
 title        = "OTTER 3.3 Reference Manual",
 journal      = "CoRR",
 volume       = "cs.SC/0310056",
)
@inproceedings(meier:calculemus02,
 author       = "A. Meier and V. Sorge and S. Colton",
 year         = "2002",
 title        = "Employing Theory Formation to Guide Proof Planning",
 booktitle    = "AISC/Calculemus'02, LNAI 2385",
 publisher    = "Springer",
 doi          = "10.1007/3-540-45470-5\_25",
)
@inproceedings(Montano:MICAI:2010,
 author       = "O. Montano-Rivas and R. McCasland and L. Dixon and A. Bundy",
 year         = "2010",
 title        = "Scheme-Based Synthesis of Inductive Theories",
 booktitle    = "MICAI",
 series       = "LNCS",
 volume       = "6437",
 pages        = "348--361",
 doi          = "10.1007/978-3-642-16761-4\_31",
)
@incollection(lsr09,
 author       = "A. Pease and A. Smaill and S. Colton and A. Ireland and M. Llano and R. Ramezani and G. Grov and M. Guhe",
 year         = "2010",
 title        = "Applying {L}akatos-style reasoning to {A}{I} problems",
 booktitle    = "Thinking Machines and the philosophy of computer science: Concepts and principles",
 publisher    = "{I}{G}{I} {G}lobal",
 address      = "PA, USA",
 pages        = "149--174",
 doi          = "10.4018/978-1-61692-014-2",
)
@incollection(partridge,
 author       = "G. Ritchie and F. Hanna",
 year         = "1990",
 title        = "{AM}: a case study in methodology",
 editor       = "D. Partridge and Y. Wilks",
 booktitle    = "The foundations of AI: a sourcebook",
 publisher    = "CUP",
 address      = "Cambridge",
 pages        = "247--265",
 doi          = "10.1017/CBO9780511663116.024",
)
@article(UML-B06,
 author       = "C. Snook and M. Butler",
 year         = "2006",
 title        = "UML-B: Formal modeling and design aided by UML",
 journal      = "ACM Transactions on Software Engineering and Methodology.",
 volume       = "15",
 number       = "1",
 pages        = "92--122",
 doi          = "10.1145/1125808.1125811",
)