1 @book{proakis2004contemporary, |
|
2 title={Contemporary communication systems using MATLAB and Simulink}, |
|
3 author={Proakis, J.G. and Salehi, M. and Bauch, G.}, |
|
4 isbn={9780534406172}, |
|
5 lccn={31054410}, |
|
6 series={BookWare companion series}, |
|
7 url={http://books.google.at/books?id=5mXGQgAACAAJ}, |
|
8 year={2004}, |
|
9 publisher={Thomson--Brooks/Cole} |
|
10 } |
|
11 @book{oppenheim2010discrete, |
|
12 title={Discrete-time signal processing}, |
|
13 author={Oppenheim, A.V. and Schafer, R.W.}, |
|
14 isbn={9780131988422}, |
|
15 series={Prentice-Hall signal processing series}, |
|
16 url={http://books.google.at/books?id=mYsoAQAAMAAJ}, |
|
17 year={2010}, |
|
18 publisher={Prentice Hall} |
|
19 } |
|
20 @manual{wenzel2011system, |
|
21 title={The Isabelle System Manual}, |
|
22 author={Wenzel, M. and Berghofer, S.}, |
|
23 organization={TU Muenchen}, |
|
24 year={2011}, |
|
25 month={January} |
|
26 } |
|
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}, |
|
31 series = {LNCS}, |
|
32 volume = 2283, |
|
33 year = 2002} |
|
34 @Book{progr-mathematica, |
|
35 author = {Maeder, Roman E.}, |
|
36 title = {Programming in Mathematica}, |
|
37 publisher = {Addison-Wesley}, |
|
38 address = {Reading, Mass.}, |
|
39 year = {1997} |
|
40 } |
|
41 @Book{prog-maple06, |
|
42 author = {Aladjav, Victor and Bogdevicius, Marijonas}, |
|
43 title = {Maple: Programming, Physical and Engineering Problems}, |
|
44 publisher = {Fultus Corporation}, |
|
45 year = {2006}, |
|
46 month = {February 27}, |
|
47 annote = {ISBN: 1596820802} |
|
48 } |
|
49 @Article{plmms10, |
|
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}, |
|
53 year = {2010}, |
|
54 volume = {44}, |
|
55 number = {1/2}, |
|
56 pages = {27-41} %, |
|
57 %month = {March/June}, |
|
58 %note = {http://www.ist.tugraz.at/projects/isac/publ/plmms-10.pdf} |
|
59 } |
|
60 @inproceedings{casproto, |
|
61 author = {Cezary Kaliszyk and |
|
62 Freek Wiedijk}, |
|
63 title = {Certified Computer Algebra on Top of an Interactive Theorem |
|
64 Prover}, |
|
65 booktitle = {Calculemus}, |
|
66 year = {2007}, |
|
67 pages = {94-105}, |
|
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} |
|
71 } |
|
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}, |
|
76 year = {2012}, |
|
77 editor = {Quaresma, Pedro}, |
|
78 publisher = {EPTCS}, |
|
79 note = {To appear} |
|
80 } |
|
81 @Manual{Huet_all:94, |
|
82 author = {Huet, G. and Kahn, G. and Paulin-Mohring, C.}, |
|
83 title = {The Coq Proof Assistant}, |
|
84 institution = {INRIA-Rocquencourt}, |
|
85 year = {1994}, |
|
86 type = {Tutorial}, |
|
87 number = {Version 5.10}, |
|
88 address = {CNRS-ENS Lyon}, |
|
89 status={},source={Theorema},location={-} |
|
90 } |
|
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}, |
|
95 year = {2009}, |
|
96 type = {TUCS Technical Report}, |
|
97 number = {949}, |
|
98 address = {Turku, Finland}, |
|
99 month = {July} |
|
100 } |
|
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)}, |
|
105 pages = {91-101}, |
|
106 year = {2004}, |
|
107 editor = {Rutkowski, L. and Siekmann, J. and Tadeusiewicz, R. and Zadeh, L.A.}, |
|
108 number = {3070,}, |
|
109 series = {LNAI}, |
|
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}, |
|
116 year = {2008}, |
|
117 type = {Technical Report}, |
|
118 number = {20}, |
|
119 note = {http://repository.cmu.edu/psychology/20} |
|
120 } |
|
121 @PhdThesis{proof-strategies-11, |
|
122 author = {Dietrich, Dominik}, |
|
123 title = {Proof Planning with Compiled Strategies}, |
|
124 school = {FR 6.2 Informatik, Saarland University}, |
|
125 year = {2011} |
|
126 } |
|
127 @proceedings{DBLP:conf/mkm/2007, |
|
128 editor = {Manuel Kauers and |
|
129 Manfred Kerber and |
|
130 Robert Miner 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}, |
|
138 volume = {4573}, |
|
139 year = {2007}, |
|
140 isbn = {978-3-540-73083-5}, |
|
141 bibsource = {DBLP, http://dblp.uni-trier.de} |
|
142 } |
|