jan@42309
|
1 |
@book{proakis2004contemporary,
|
jan@42309
|
2 |
title={Contemporary communication systems using MATLAB and Simulink},
|
jan@42309
|
3 |
author={Proakis, J.G. and Salehi, M. and Bauch, G.},
|
jan@42309
|
4 |
isbn={9780534406172},
|
jan@42309
|
5 |
lccn={31054410},
|
jan@42309
|
6 |
series={BookWare companion series},
|
jan@42309
|
7 |
url={http://books.google.at/books?id=5mXGQgAACAAJ},
|
jan@42309
|
8 |
year={2004},
|
jan@42309
|
9 |
publisher={Thomson--Brooks/Cole}
|
jan@42309
|
10 |
}
|
jan@42309
|
11 |
@book{oppenheim2010discrete,
|
jan@42309
|
12 |
title={Discrete-time signal processing},
|
jan@42309
|
13 |
author={Oppenheim, A.V. and Schafer, R.W.},
|
jan@42309
|
14 |
isbn={9780131988422},
|
jan@42309
|
15 |
series={Prentice-Hall signal processing series},
|
jan@42309
|
16 |
url={http://books.google.at/books?id=mYsoAQAAMAAJ},
|
jan@42309
|
17 |
year={2010},
|
jan@42309
|
18 |
publisher={Prentice Hall}
|
jan@42326
|
19 |
}
|
jan@42326
|
20 |
@manual{wenzel2011system,
|
jan@42326
|
21 |
title={The Isabelle System Manual},
|
jan@42326
|
22 |
author={Wenzel, M. and Berghofer, S.},
|
neuper@42328
|
23 |
organization={TU München},
|
jan@42326
|
24 |
year={2011},
|
jan@42326
|
25 |
month={January}
|
neuper@42328
|
26 |
}
|
neuper@42328
|
27 |
@Book{Nipkow-Paulson-Wenzel:2002,
|
neuper@42328
|
28 |
author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
|
neuper@42328
|
29 |
title = {{Isabelle/HOL} --- A Proof Assistant for Higher-Order Logic},
|
neuper@42328
|
30 |
publisher = {Springer},
|
neuper@42328
|
31 |
series = {LNCS},
|
neuper@42328
|
32 |
volume = 2283,
|
neuper@42328
|
33 |
year = 2002}
|
neuper@42328
|
34 |
@Book{progr-mathematica,
|
neuper@42328
|
35 |
author = {Maeder, Roman E.},
|
neuper@42328
|
36 |
title = {Programming in Mathematica},
|
neuper@42328
|
37 |
publisher = {Addison-Wesley},
|
neuper@42328
|
38 |
address = {Reading, Mass.},
|
neuper@42328
|
39 |
year = {1997}
|
neuper@42328
|
40 |
}
|
neuper@42328
|
41 |
@Book{prog-maple06,
|
neuper@42328
|
42 |
author = {Aladjav, Victor and Bogdevicius, Marijonas},
|
neuper@42328
|
43 |
title = {Maple: Programming, Physical and Engineering Problems},
|
neuper@42328
|
44 |
publisher = {Fultus Corporation},
|
neuper@42328
|
45 |
year = {2006},
|
neuper@42328
|
46 |
month = {February 27},
|
neuper@42328
|
47 |
annote = {ISBN: 1596820802}
|
neuper@42328
|
48 |
}
|
neuper@42328
|
49 |
@Article{plmms10,
|
neuper@42328
|
50 |
author = {Florian Haftmann and Cezary Kaliszyk and Walther Neuper},
|
neuper@42328
|
51 |
title = {{CTP}-based programming languages~? Considerations about an experimental design},
|
neuper@42328
|
52 |
journal = {ACM Communications in Computer Algebra},
|
neuper@42328
|
53 |
year = {2010},
|
neuper@42328
|
54 |
volume = {44},
|
neuper@42328
|
55 |
number = {1/2},
|
neuper@42328
|
56 |
pages = {27-41} %,
|
neuper@42328
|
57 |
%month = {March/June},
|
neuper@42328
|
58 |
%note = {http://www.ist.tugraz.at/projects/isac/publ/plmms-10.pdf}
|
neuper@42328
|
59 |
}
|
neuper@42328
|
60 |
@inproceedings{casproto,
|
neuper@42328
|
61 |
author = {Cezary Kaliszyk and
|
neuper@42328
|
62 |
Freek Wiedijk},
|
neuper@42328
|
63 |
title = {Certified Computer Algebra on Top of an Interactive Theorem
|
neuper@42328
|
64 |
Prover},
|
neuper@42328
|
65 |
booktitle = {Calculemus},
|
neuper@42328
|
66 |
year = {2007},
|
neuper@42328
|
67 |
pages = {94-105},
|
neuper@42328
|
68 |
ee = {http://dx.doi.org/10.1007/978-3-540-73086-6_8},
|
neuper@42328
|
69 |
crossref = {DBLP:conf/mkm/2007},
|
neuper@42328
|
70 |
bibsource = {DBLP, http://dblp.uni-trier.de}
|
neuper@42328
|
71 |
}
|
neuper@42328
|
72 |
@InProceedings{wn:lucas-interp-12,
|
neuper@42328
|
73 |
author = {Neuper, Walther},
|
neuper@42328
|
74 |
title = {Automated Generation of User Guidance by Combining Computation and Deduction},
|
neuper@42328
|
75 |
booktitle = {THedu'11: CTP-compontents for educational software},
|
neuper@42328
|
76 |
year = {2012},
|
neuper@42328
|
77 |
editor = {Quaresma, Pedro},
|
neuper@42328
|
78 |
publisher = {EPTCS},
|
neuper@42328
|
79 |
note = {To appear}
|
neuper@42328
|
80 |
}
|
neuper@42328
|
81 |
@Manual{Huet_all:94,
|
neuper@42328
|
82 |
author = {Huet, G. and Kahn, G. and Paulin-Mohring, C.},
|
neuper@42328
|
83 |
title = {The Coq Proof Assistant},
|
neuper@42328
|
84 |
institution = {INRIA-Rocquencourt},
|
neuper@42328
|
85 |
year = {1994},
|
neuper@42328
|
86 |
type = {Tutorial},
|
neuper@42328
|
87 |
number = {Version 5.10},
|
neuper@42328
|
88 |
address = {CNRS-ENS Lyon},
|
neuper@42328
|
89 |
status={},source={Theorema},location={-}
|
neuper@42328
|
90 |
}
|
neuper@42328
|
91 |
@TECHREPORT{Back-SD09,
|
neuper@42328
|
92 |
author = {Back, Ralph-Johan},
|
neuper@42328
|
93 |
title = {Structured Derivations as a Unified Proof Style for Teaching Mathematics},
|
neuper@42328
|
94 |
institution = {TUCS - Turku Centre for Computer Science},
|
neuper@42328
|
95 |
year = {2009},
|
neuper@42328
|
96 |
type = {TUCS Technical Report},
|
neuper@42328
|
97 |
number = {949},
|
neuper@42328
|
98 |
address = {Turku, Finland},
|
neuper@42328
|
99 |
month = {July}
|
neuper@42328
|
100 |
}
|
neuper@42328
|
101 |
@InProceedings{ActiveMath-MAIN11,
|
jan@42330
|
102 |
author = {Melis, Erica and Siekmann, Jörg},
|
neuper@42328
|
103 |
title = {An Intelligent Tutoring System for Mathematics},
|
jan@42330
|
104 |
booktitle = {Seventh International Conference Artificial Intelligence and Soft Computing (ICAISC)},
|
jan@42330
|
105 |
pages = {91-101},
|
neuper@42328
|
106 |
year = {2004},
|
jan@42330
|
107 |
editor = {Rutkowski, L. and Siekmann, J. and Tadeusiewicz, R. and Zadeh, L.A.},
|
neuper@42328
|
108 |
number = {3070,},
|
neuper@42328
|
109 |
series = {LNAI},
|
neuper@42328
|
110 |
publisher = {Springer-Verlag},
|
neuper@42328
|
111 |
doi = {doi:10.1007/978-3-540-24844-6\_12}}
|
neuper@42328
|
112 |
@TechReport{mat-tutor-cmu-MAIN11,
|
neuper@42328
|
113 |
author = {John R. Anderson},
|
neuper@42328
|
114 |
title = {Intelligent Tutoring and High School Mathematics},
|
neuper@42328
|
115 |
institution = {Carnegie Mellon University, Department of Psychology},
|
neuper@42328
|
116 |
year = {2008},
|
neuper@42328
|
117 |
type = {Technical Report},
|
neuper@42328
|
118 |
number = {20},
|
neuper@42328
|
119 |
note = {http://repository.cmu.edu/psychology/20}
|
neuper@42328
|
120 |
}
|
neuper@42328
|
121 |
@PhdThesis{proof-strategies-11,
|
neuper@42328
|
122 |
author = {Dietrich, Dominik},
|
neuper@42328
|
123 |
title = {Proof Planning with Compiled Strategies},
|
neuper@42328
|
124 |
school = {FR 6.2 Informatik, Saarland University},
|
neuper@42328
|
125 |
year = {2011}
|
neuper@42328
|
126 |
}
|
neuper@42328
|
127 |
@proceedings{DBLP:conf/mkm/2007,
|
neuper@42328
|
128 |
editor = {Manuel Kauers and
|
neuper@42328
|
129 |
Manfred Kerber and
|
neuper@42328
|
130 |
Robert Miner and
|
neuper@42328
|
131 |
Wolfgang Windsteiger},
|
neuper@42328
|
132 |
title = {Towards Mechanized Mathematical Assistants, 14th Symposium,
|
neuper@42328
|
133 |
Calculemus 2007, 6th International Conference, MKM 2007,
|
neuper@42328
|
134 |
Hagenberg, Austria, June 27-30, 2007, Proceedings},
|
neuper@42328
|
135 |
booktitle = {Calculemus/MKM},
|
neuper@42328
|
136 |
publisher = {Springer},
|
neuper@42328
|
137 |
series = {Lecture Notes in Computer Science},
|
neuper@42328
|
138 |
volume = {4573},
|
neuper@42328
|
139 |
year = {2007},
|
neuper@42328
|
140 |
isbn = {978-3-540-73083-5},
|
neuper@42328
|
141 |
bibsource = {DBLP, http://dblp.uni-trier.de}
|
neuper@42328
|
142 |
}
|