jan@42309: @book{proakis2004contemporary, jan@42309: title={Contemporary communication systems using MATLAB and Simulink}, jan@42309: author={Proakis, J.G. and Salehi, M. and Bauch, G.}, jan@42309: isbn={9780534406172}, jan@42309: lccn={31054410}, jan@42309: series={BookWare companion series}, jan@42309: url={http://books.google.at/books?id=5mXGQgAACAAJ}, jan@42309: year={2004}, jan@42309: publisher={Thomson--Brooks/Cole} jan@42309: } jan@42309: @book{oppenheim2010discrete, jan@42309: title={Discrete-time signal processing}, jan@42309: author={Oppenheim, A.V. and Schafer, R.W.}, jan@42309: isbn={9780131988422}, jan@42309: series={Prentice-Hall signal processing series}, jan@42309: url={http://books.google.at/books?id=mYsoAQAAMAAJ}, jan@42309: year={2010}, jan@42309: publisher={Prentice Hall} jan@42326: } jan@42326: @manual{wenzel2011system, jan@42326: title={The Isabelle System Manual}, jan@42326: author={Wenzel, M. and Berghofer, S.}, jan@42381: organization={TU Muenchen}, jan@42326: year={2011}, jan@42326: month={January} neuper@42328: } neuper@42328: @Book{Nipkow-Paulson-Wenzel:2002, neuper@42328: author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel}, neuper@42328: title = {{Isabelle/HOL} --- A Proof Assistant for Higher-Order Logic}, neuper@42328: publisher = {Springer}, neuper@42328: series = {LNCS}, neuper@42328: volume = 2283, neuper@42328: year = 2002} neuper@42328: @Book{progr-mathematica, neuper@42328: author = {Maeder, Roman E.}, neuper@42328: title = {Programming in Mathematica}, neuper@42328: publisher = {Addison-Wesley}, neuper@42328: address = {Reading, Mass.}, neuper@42328: year = {1997} neuper@42328: } neuper@42328: @Book{prog-maple06, neuper@42328: author = {Aladjav, Victor and Bogdevicius, Marijonas}, neuper@42328: title = {Maple: Programming, Physical and Engineering Problems}, neuper@42328: publisher = {Fultus Corporation}, neuper@42328: year = {2006}, neuper@42328: month = {February 27}, neuper@42328: annote = {ISBN: 1596820802} neuper@42328: } neuper@42328: @Article{plmms10, neuper@42328: author = {Florian Haftmann and Cezary Kaliszyk and Walther Neuper}, neuper@42328: title = {{CTP}-based programming languages~? Considerations about an experimental design}, neuper@42328: journal = {ACM Communications in Computer Algebra}, neuper@42328: year = {2010}, neuper@42328: volume = {44}, neuper@42328: number = {1/2}, neuper@42328: pages = {27-41} %, neuper@42328: %month = {March/June}, neuper@42328: %note = {http://www.ist.tugraz.at/projects/isac/publ/plmms-10.pdf} neuper@42328: } neuper@42328: @inproceedings{casproto, neuper@42328: author = {Cezary Kaliszyk and neuper@42328: Freek Wiedijk}, neuper@42328: title = {Certified Computer Algebra on Top of an Interactive Theorem neuper@42328: Prover}, neuper@42328: booktitle = {Calculemus}, neuper@42328: year = {2007}, neuper@42328: pages = {94-105}, neuper@42328: ee = {http://dx.doi.org/10.1007/978-3-540-73086-6_8}, neuper@42328: crossref = {DBLP:conf/mkm/2007}, neuper@42328: bibsource = {DBLP, http://dblp.uni-trier.de} neuper@42328: } neuper@42328: @InProceedings{wn:lucas-interp-12, neuper@42328: author = {Neuper, Walther}, neuper@42328: title = {Automated Generation of User Guidance by Combining Computation and Deduction}, neuper@42328: booktitle = {THedu'11: CTP-compontents for educational software}, neuper@42328: year = {2012}, neuper@42328: editor = {Quaresma, Pedro}, neuper@42328: publisher = {EPTCS}, neuper@42328: note = {To appear} neuper@42328: } neuper@42328: @Manual{Huet_all:94, neuper@42328: author = {Huet, G. and Kahn, G. and Paulin-Mohring, C.}, neuper@42328: title = {The Coq Proof Assistant}, neuper@42328: institution = {INRIA-Rocquencourt}, neuper@42328: year = {1994}, neuper@42328: type = {Tutorial}, neuper@42328: number = {Version 5.10}, neuper@42328: address = {CNRS-ENS Lyon}, neuper@42328: status={},source={Theorema},location={-} neuper@42328: } neuper@42328: @TECHREPORT{Back-SD09, neuper@42328: author = {Back, Ralph-Johan}, neuper@42328: title = {Structured Derivations as a Unified Proof Style for Teaching Mathematics}, neuper@42328: institution = {TUCS - Turku Centre for Computer Science}, neuper@42328: year = {2009}, neuper@42328: type = {TUCS Technical Report}, neuper@42328: number = {949}, neuper@42328: address = {Turku, Finland}, neuper@42328: month = {July} neuper@42328: } neuper@42328: @InProceedings{ActiveMath-MAIN11, jan@42330: author = {Melis, Erica and Siekmann, Jörg}, neuper@42328: title = {An Intelligent Tutoring System for Mathematics}, jan@42330: booktitle = {Seventh International Conference Artificial Intelligence and Soft Computing (ICAISC)}, jan@42330: pages = {91-101}, neuper@42328: year = {2004}, jan@42330: editor = {Rutkowski, L. and Siekmann, J. and Tadeusiewicz, R. and Zadeh, L.A.}, neuper@42328: number = {3070,}, neuper@42328: series = {LNAI}, neuper@42328: publisher = {Springer-Verlag}, neuper@42328: doi = {doi:10.1007/978-3-540-24844-6\_12}} neuper@42328: @TechReport{mat-tutor-cmu-MAIN11, neuper@42328: author = {John R. Anderson}, neuper@42328: title = {Intelligent Tutoring and High School Mathematics}, neuper@42328: institution = {Carnegie Mellon University, Department of Psychology}, neuper@42328: year = {2008}, neuper@42328: type = {Technical Report}, neuper@42328: number = {20}, neuper@42328: note = {http://repository.cmu.edu/psychology/20} neuper@42328: } neuper@42328: @PhdThesis{proof-strategies-11, neuper@42328: author = {Dietrich, Dominik}, neuper@42328: title = {Proof Planning with Compiled Strategies}, neuper@42328: school = {FR 6.2 Informatik, Saarland University}, neuper@42328: year = {2011} neuper@42328: } neuper@42328: @proceedings{DBLP:conf/mkm/2007, neuper@42328: editor = {Manuel Kauers and neuper@42328: Manfred Kerber and neuper@42328: Robert Miner and neuper@42328: Wolfgang Windsteiger}, neuper@42328: title = {Towards Mechanized Mathematical Assistants, 14th Symposium, neuper@42328: Calculemus 2007, 6th International Conference, MKM 2007, neuper@42328: Hagenberg, Austria, June 27-30, 2007, Proceedings}, neuper@42328: booktitle = {Calculemus/MKM}, neuper@42328: publisher = {Springer}, neuper@42328: series = {Lecture Notes in Computer Science}, neuper@42328: volume = {4573}, neuper@42328: year = {2007}, neuper@42328: isbn = {978-3-540-73083-5}, neuper@42328: bibsource = {DBLP, http://dblp.uni-trier.de} neuper@42328: }