1 @book{proakis2004contemporary,
2 title={Contemporary communication systems using MATLAB and Simulink},
3 author={Proakis, J.G. and Salehi, M. and Bauch, G.},
6 series={BookWare companion series},
7 url={http://books.google.at/books?id=5mXGQgAACAAJ},
9 publisher={Thomson--Brooks/Cole}
11 @book{oppenheim2010discrete,
12 title={Discrete-time signal processing},
13 author={Oppenheim, A.V. and Schafer, R.W.},
15 series={Prentice-Hall signal processing series},
16 url={http://books.google.at/books?id=mYsoAQAAMAAJ},
18 publisher={Prentice Hall}
20 @manual{wenzel2011system,
21 title={The Isabelle System Manual},
22 author={Wenzel, M. and Berghofer, S.},
23 organization={TU Muenchen},
27 @Book{Nipkow-Paulson-Wenzel:2002,
28 author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
29 title = {{Isabelle/HOL} --- A Proof Assistant for Higher-Order Logic},
30 publisher = {Springer},
34 @Book{progr-mathematica,
35 author = {Maeder, Roman E.},
36 title = {Programming in Mathematica},
37 publisher = {Addison-Wesley},
38 address = {Reading, Mass.},
42 author = {Aladjav, Victor and Bogdevicius, Marijonas},
43 title = {Maple: Programming, Physical and Engineering Problems},
44 publisher = {Fultus Corporation},
46 month = {February 27},
47 annote = {ISBN: 1596820802}
50 author = {Florian Haftmann and Cezary Kaliszyk and Walther Neuper},
51 title = {{CTP}-based programming languages~? Considerations about an experimental design},
52 journal = {ACM Communications in Computer Algebra},
58 note = {http://www.ist.tugraz.at/projects/isac/publ/plmms-10.pdf}
60 @inproceedings{casproto,
61 author = {Cezary Kaliszyk and
63 title = {Certified Computer Algebra on Top of an Interactive Theorem
65 booktitle = {Calculemus},
68 ee = {http://dx.doi.org/10.1007/978-3-540-73086-6_8},
69 crossref = {DBLP:conf/mkm/2007},
70 bibsource = {DBLP, http://dblp.uni-trier.de}
72 @InProceedings{wn:lucas-interp-12,
73 author = {Neuper, Walther},
74 title = {Automated Generation of User Guidance by Combining Computation and Deduction},
75 booktitle = {THedu'11: CTP-compontents for educational software},
77 editor = {Quaresma, Pedro},
82 author = {Huet, G. and Kahn, G. and Paulin-Mohring, C.},
83 title = {The Coq Proof Assistant},
84 institution = {INRIA-Rocquencourt},
87 number = {Version 5.10},
88 address = {CNRS-ENS Lyon},
89 status={},source={Theorema},location={-}
91 @TECHREPORT{Back-SD09,
92 author = {Back, Ralph-Johan},
93 title = {Structured Derivations as a Unified Proof Style for Teaching Mathematics},
94 institution = {TUCS - Turku Centre for Computer Science},
96 type = {TUCS Technical Report},
98 address = {Turku, Finland},
101 @InProceedings{ActiveMath-MAIN11,
102 author = {Melis, Erica and Siekmann, Jörg},
103 title = {An Intelligent Tutoring System for Mathematics},
104 booktitle = {Seventh International Conference Artificial Intelligence and Soft Computing (ICAISC)},
107 editor = {Rutkowski, L. and Siekmann, J. and Tadeusiewicz, R. and Zadeh, L.A.},
110 publisher = {Springer-Verlag},
111 doi = {doi:10.1007/978-3-540-24844-6\_12}}
112 @TechReport{mat-tutor-cmu-MAIN11,
113 author = {John R. Anderson},
114 title = {Intelligent Tutoring and High School Mathematics},
115 institution = {Carnegie Mellon University, Department of Psychology},
117 type = {Technical Report},
119 note = {http://repository.cmu.edu/psychology/20}
121 @PhdThesis{proof-strategies-11,
122 author = {Dietrich, Dominik},
123 title = {Proof Planning with Compiled Strategies},
124 school = {FR 6.2 Informatik, Saarland University},
127 @proceedings{DBLP:conf/mkm/2007,
128 editor = {Manuel Kauers and
131 Wolfgang Windsteiger},
132 title = {Towards Mechanized Mathematical Assistants, 14th Symposium,
133 Calculemus 2007, 6th International Conference, MKM 2007,
134 Hagenberg, Austria, June 27-30, 2007, Proceedings},
135 booktitle = {Calculemus/MKM},
136 publisher = {Springer},
137 series = {Lecture Notes in Computer Science},
140 isbn = {978-3-540-73083-5},
141 bibsource = {DBLP, http://dblp.uni-trier.de}
144 @InProceedings{gdaroczy-EP-13,
145 author = {Gabriella Dar\'{o}czy and Walther Neuper},
146 title = {Exploitation of ``Next-Step-Guidance'' in a {TP}-based Math Assistant},
147 OPTpages = {TODO-TODO},
148 crossref = {eduTPS-12}
152 @Proceedings{eduTPS-12,
153 title = {Theorem-Prover based Systems for Education (eduTPS)},
163 OPTorganization = {},
164 publisher = {The Electronic Journal of Mathematics and Technology},
169 @Misc{nipkow-prog-prove,
170 author = {Nipkow, Tobias},
171 title = {Programming and Proving in {Isabelle/HOL}},
172 howpublished = {contained in the Isabelle distribution},
178 author = {J. Roger Hindley},
179 title = {Basic Simple Type Theory},
180 publisher = {Cambridge University Press},
182 editor = {S. Abramsky and P. H. Aczel and others},
184 series = {Cambridge Tracts in Theoretical Computer Science},
185 address = {Cambridge},
190 author = {Milner, R.},
191 title = {A Theory of Type Polymorphism in Programming},
192 journal = {Journal of Computer and System Science (JCSS)},