@article(RISC2487,
 author       = "B. Buchberger and A. Craciun and T. Jebelean and L. Kovacs and T. Kutsia and K. Nakagawa and F. Piroi and N. Popov and J. Robu and M. Rosenkranz and W. Windsteiger",
 year         = "2006",
 title        = "{Theorema: Towards Computer-Aided Mathematical Theory Exploration}",
 journal      = "Journal of Applied Logic",
 volume       = "4",
 number       = "4",
 pages        = "470--504",
 doi          = "10.1016/j.jal.2005.10.006",
)
@inproceedings(RISC2330,
 author       = "B. Buchberger and C. Dupre and T. Jebelean and F. Kriftner and K. Nakagawa and D. Vasaru and W. Windsteiger",
 year         = "2000",
 title        = "{The Theorema Project: A Progress Report}",
 editor       = "M. Kerber and M. Kohlhase",
 booktitle    = "{Symbolic Computation and Automated Reasoning (Proceedings of CALCULEMUS 2000, Symposium on the Integration of Symbolic Computation and Mechanized Reasoning)}",
 organization = "St. Andrews, Scotland",
 publisher    = "Copyright: A.K. Peters, Natick, Massachusetts",
 pages        = "98--113",
)
@inproceedings(RISC2674,
 author       = "B. Buchberger and T. Jebelean and F. Kriftner and M. Marin and E. Tomuta and D. Vasaru",
 year         = "1997",
 title        = "{A Survey of the Theorema project}",
 editor       = "W. Kuechlin",
 booktitle    = "{Proceedings of ISSAC'97 (International Symposium on Symbolic and Algebraic Computation, Maui, Hawaii, July 21-23, 1997)}",
 publisher    = "ACM Press",
 pages        = "384--391",
 doi          = "10.1145/258726.258853",
)
@inproceedings(Kammueller99locales:a,
 author       = "Florian Kamm{\"u}ller and Markus Wenzel and Lawrence C. Paulson",
 year         = "1999",
 title        = "{Locales: A Sectioning Concept for Isabelle}",
 booktitle    = "{Theorem Proving in Higher Order Logics (TPHOLs'99), LNCS 1690}",
 publisher    = "Springer",
 pages        = "149--165",
 doi          = "10.1007/3-540-48256-3\_11",
)
@inproceedings(RISC4610,
 author       = "Manfred Kerber and Christoph Lange and Colin Rowat and Wolfgang Windsteiger",
 year         = "2013",
 title        = "{Developing an Auction Theory Toolbox}",
 editor       = "Manfred Kerber and Christoph Lange and Colin Rowat",
 booktitle    = "{AISB 2013}",
 url          = "http://www.cs.bham.ac.uk/research/projects/formare/events/aisb2013/proceedings.php",
)
@inproceedings(RISC3067,
 author       = "G. Mayrhofer and S. Saminger and W. Windsteiger",
 year         = "2007",
 title        = "{CreaComp: Experimental Formal Mathematics for the Classroom}",
 editor       = "Shangzhi Li and Dongming Wang and  and Jing-Zhong Zhang",
 booktitle    = "{Symbolic Computation and Education}",
 publisher    = "World Scientific Publishing Co.",
 address      = "Singapore, New Jersey",
 pages        = "94--114",
 doi          = "10.1142/9789812776006\_0006",
)
@incollection(RISC2737,
 author       = "W. Windsteiger and B. Buchberger and M. Rosenkranz",
 year         = "2006",
 title        = "{Theorema}",
 editor       = "Freek Wiedijk",
 booktitle    = "{The Seventeen Provers of the World}",
 series       = "LNAI",
 volume       = "3600",
 publisher    = "Springer Berlin Heidelberg New York",
 pages        = "96--107",
 doi          = "10.1007/11542384\_14",
)
@book(Mma3,
 author       = "S. Wolfram",
 year         = "1996",
 title        = "The Mathematica Book",
 edition      = "third",
 publisher    = "Wolfram Media/Cambridge University Press",
)