@book{proakis2004contemporary,

   title={Contemporary communication systems using MATLAB and Simulink},

   author={Proakis, J.G. and Salehi, M. and Bauch, G.},

   isbn={9780534406172},

   lccn={31054410},

   series={BookWare companion series},

   url={http://books.google.at/books?id=5mXGQgAACAAJ},

   year={2004},

   publisher={Thomson--Brooks/Cole}

 }

 @book{oppenheim2010discrete,

   title={Discrete-time signal processing},

   author={Oppenheim, A.V. and Schafer, R.W.},

   isbn={9780131988422},

   series={Prentice-Hall signal processing series},

   url={http://books.google.at/books?id=mYsoAQAAMAAJ},

   year={2010},

   publisher={Prentice Hall}

 }

 @manual{wenzel2011system,

 	title={The Isabelle System Manual},

 	author={Wenzel, M. and Berghofer, S.},

 	organization={TU Muenchen},

 	year={2011},

 	month={January}

 }

 @Book{Nipkow-Paulson-Wenzel:2002,

   author	= {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},

   title		= {{Isabelle/HOL} --- A Proof Assistant for Higher-Order Logic},

   publisher	= {Springer},

   series	= {LNCS},

   volume	= 2283,

   year		= 2002}

 @Book{progr-mathematica,

   author = 	 {Maeder, Roman E.},

   title = 	 {Programming in Mathematica},

   publisher = 	 {Addison-Wesley},

   address = 	 {Reading, Mass.},

   year = 	 {1997}

 }

 @Book{prog-maple06,

   author = 	 {Aladjav, Victor and Bogdevicius, Marijonas},

   title = 	 {Maple: Programming, Physical and Engineering Problems},

   publisher = 	 {Fultus Corporation},

   year = 	 {2006},

   month = 	 {February 27},

   annote = 	 {ISBN: 1596820802}

 }

 @Article{plmms10,

   author = 	 {Florian Haftmann and Cezary Kaliszyk and Walther Neuper},

   title = 	 {{CTP}-based programming languages~? Considerations about an experimental design},

   journal = 	 {ACM Communications in Computer Algebra},

   year = 	 {2010},

   volume = 	 {44},

   number = 	 {1/2},

   pages = 	 {27-41} %,

   %month = 	 {March/June},

   %note = 	 {http://www.ist.tugraz.at/projects/isac/publ/plmms-10.pdf}

 }

 @inproceedings{casproto,

   author    = {Cezary Kaliszyk and

                Freek Wiedijk},

   title     = {Certified Computer Algebra on Top of an Interactive Theorem

                Prover},

   booktitle = {Calculemus},

   year      = {2007},

   pages     = {94-105},

   ee        = {http://dx.doi.org/10.1007/978-3-540-73086-6_8},

   crossref  = {DBLP:conf/mkm/2007},

   bibsource = {DBLP, http://dblp.uni-trier.de}

 }

 @InProceedings{wn:lucas-interp-12,

   author = 	 {Neuper, Walther},

   title = 	 {Automated Generation of User Guidance by Combining Computation and Deduction},

   booktitle = {THedu'11: CTP-compontents for educational software},

   year = 	 {2012},

   editor = 	 {Quaresma, Pedro},

   publisher = {EPTCS},

   note = {To appear}

 }

 @Manual{Huet_all:94,

   author = 	 {Huet, G. and Kahn, G. and  Paulin-Mohring, C.},

   title = 	 {The Coq Proof Assistant},

   institution =  {INRIA-Rocquencourt},

   year = 	 {1994},

   type = 	 {Tutorial},

   number = 	 {Version 5.10},

   address = 	 {CNRS-ENS Lyon},

   status={},source={Theorema},location={-}

 }

 @TECHREPORT{Back-SD09,

   author = {Back, Ralph-Johan},

   title = {Structured Derivations as a Unified Proof Style for Teaching Mathematics},

   institution = {TUCS - Turku Centre for Computer Science},

   year = {2009},

   type = {TUCS Technical Report},

   number = {949},

   address = {Turku, Finland},

   month = {July}

 }

 @InProceedings{ActiveMath-MAIN11,

   author = 	 {Melis, Erica and Siekmann, Jörg},

   title = 	 {An Intelligent Tutoring System for Mathematics},

   booktitle = {Seventh International Conference Artificial Intelligence and Soft Computing (ICAISC)},

   pages = 	 {91-101},

   year = 	 {2004},

   editor = 	 {Rutkowski, L. and Siekmann, J. and Tadeusiewicz, R. and Zadeh, L.A.},

   number = 	 {3070,},

   series = 	 {LNAI},

   publisher = {Springer-Verlag},

   doi =          {doi:10.1007/978-3-540-24844-6\_12}}

 @TechReport{mat-tutor-cmu-MAIN11,

   author = 	 {John R. Anderson},

   title = 	 {Intelligent Tutoring and High School Mathematics},

   institution =  {Carnegie Mellon University, Department of Psychology},

   year = 	 {2008},

   type = 	 {Technical Report},

   number = 	 {20},

   note = 	 {http://repository.cmu.edu/psychology/20}

 }

 @PhdThesis{proof-strategies-11,

   author = 	 {Dietrich, Dominik},

   title = 	 {Proof Planning with Compiled Strategies},

   school = 	 {FR 6.2 Informatik, Saarland University},

   year = 	 {2011}

 }

 @proceedings{DBLP:conf/mkm/2007,

   editor    = {Manuel Kauers and

                Manfred Kerber and

                Robert Miner and

                Wolfgang Windsteiger},

   title     = {Towards Mechanized Mathematical Assistants, 14th Symposium,

                Calculemus 2007, 6th International Conference, MKM 2007,

                Hagenberg, Austria, June 27-30, 2007, Proceedings},

   booktitle = {Calculemus/MKM},

   publisher = {Springer},

   series    = {Lecture Notes in Computer Science},

   volume    = {4573},

   year      = {2007},

   isbn      = {978-3-540-73083-5},

   bibsource = {DBLP, http://dblp.uni-trier.de}

 }