jrocnik: comments to 3.2.
1 @book{nipk:rew-all-that,
2 title={Term rewriting and all that},
3 author={Baader, Franz and Nipkow, Tobias },
4 publisher={Cambridge University Press},year={1998},
5 volume={},series={},address={},edition={},month={},
6 note={},status={},source={},location={IST}
10 author = {Jan Rocnik},
11 title = {Interactive Course Material for Signal Processing based on Isabelle/{\isac}},
12 howpublished = {Bakkalaureate Thesis},
14 note = {IST, Graz University of Technology, http://www.ist.tugraz.at/projects/isac/publ/jrocnik\_bakk.pdf}
17 @book{proakis2004contemporary,
18 title={Contemporary communication systems using MATLAB and Simulink},
19 author={Proakis, J.G. and Salehi, M. and Bauch, G.},
22 series={BookWare companion series},
23 url={http://books.google.at/books?id=5mXGQgAACAAJ},
25 publisher={Thomson--Brooks/Cole}
27 @book{oppenheim2010discrete,
28 title={Discrete-time signal processing},
29 author={Oppenheim, A.V. and Schafer, R.W.},
31 series={Prentice-Hall signal processing series},
32 url={http://books.google.at/books?id=mYsoAQAAMAAJ},
34 publisher={Prentice Hall}
36 @manual{wenzel2011system,
37 title={The Isabelle System Manual},
38 author={Wenzel, M. and Berghofer, S.},
39 organization={TU Muenchen},
43 @Book{Nipkow-Paulson-Wenzel:2002,
44 author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
45 title = {{Isabelle/HOL} --- A Proof Assistant for Higher-Order Logic},
46 publisher = {Springer},
50 @Book{progr-mathematica,
51 author = {Maeder, Roman E.},
52 title = {Programming in Mathematica},
53 publisher = {Addison-Wesley},
54 address = {Reading, Mass.},
58 author = {Aladjav, Victor and Bogdevicius, Marijonas},
59 title = {Maple: Programming, Physical and Engineering Problems},
60 publisher = {Fultus Corporation},
62 month = {February 27},
63 annote = {ISBN: 1596820802}
66 author = {Florian Haftmann and Cezary Kaliszyk and Walther Neuper},
67 title = {{CTP}-based programming languages~? Considerations about an experimental design},
68 journal = {ACM Communications in Computer Algebra},
75 @inproceedings{casproto,
76 author = {Cezary Kaliszyk and
78 title = {Certified Computer Algebra on Top of an Interactive Theorem
80 booktitle = {Calculemus},
83 ee = {http://dx.doi.org/10.1007/978-3-540-73086-6_8},
84 crossref = {DBLP:conf/mkm/2007},
85 bibsource = {DBLP, http://dblp.uni-trier.de}
87 @InProceedings{wn:lucas-interp-12,
88 author = {Neuper, Walther},
89 title = {Automated Generation of User Guidance by Combining Computation and Deduction},
90 booktitle = {THedu'11: CTP-compontents for educational software},
92 editor = {Quaresma, Pedro},
97 author = {Huet, G. and Kahn, G. and Paulin-Mohring, C.},
98 title = {The Coq Proof Assistant},
99 institution = {INRIA-Rocquencourt},
102 number = {Version 5.10},
103 address = {CNRS-ENS Lyon},
104 status={},source={Theorema},location={-}
106 @TECHREPORT{Back-SD09,
107 author = {Back, Ralph-Johan},
108 title = {Structured Derivations as a Unified Proof Style for Teaching Mathematics},
109 institution = {TUCS - Turku Centre for Computer Science},
111 type = {TUCS Technical Report},
113 address = {Turku, Finland},
116 @InProceedings{ActiveMath-MAIN11,
117 author = {Melis, Erica and Siekmann, Jörg},
118 title = {An Intelligent Tutoring System for Mathematics},
119 booktitle = {Seventh International Conference Artificial Intelligence and Soft Computing (ICAISC)},
122 editor = {Rutkowski, L. and Siekmann, J. and Tadeusiewicz, R. and Zadeh, L.A.},
125 publisher = {Springer-Verlag},
126 doi = {doi:10.1007/978-3-540-24844-6\_12}}
127 @TechReport{mat-tutor-cmu-MAIN11,
128 author = {John R. Anderson},
129 title = {Intelligent Tutoring and High School Mathematics},
130 institution = {Carnegie Mellon University, Department of Psychology},
132 type = {Technical Report},
134 note = {http://repository.cmu.edu/psychology/20}
136 @PhdThesis{proof-strategies-11,
137 author = {Dietrich, Dominik},
138 title = {Proof Planning with Compiled Strategies},
139 school = {FR 6.2 Informatik, Saarland University},
142 @proceedings{DBLP:conf/mkm/2007,
143 editor = {Manuel Kauers and
146 Wolfgang Windsteiger},
147 title = {Towards Mechanized Mathematical Assistants, 14th Symposium,
148 Calculemus 2007, 6th International Conference, MKM 2007,
149 Hagenberg, Austria, June 27-30, 2007, Proceedings},
150 booktitle = {Calculemus/MKM},
151 publisher = {Springer},
152 series = {Lecture Notes in Computer Science},
155 isbn = {978-3-540-73083-5},
156 bibsource = {DBLP, http://dblp.uni-trier.de}
159 @InProceedings{gdaroczy-EP-13,
160 author = {Gabriella Dar\'{o}czy and Walther Neuper},
161 booktitle = {unknown},
162 title = {Exploitation of ``Next-Step-Guidance'' in a {TP}-based Math Assistant},
163 OPTpages = {TODO-TODO},
164 crossref = {eduTPS-12}
168 @Proceedings{eduTPS-12,
169 title = {Theorem-Prover based Systems for Education (eduTPS)},
179 OPTorganization = {},
180 publisher = {The Electronic Journal of Mathematics and Technology},
185 @Misc{nipkow-prog-prove,
186 author = {Nipkow, Tobias},
187 title = {Programming and Proving in {Isabelle/HOL}},
188 howpublished = {contained in the Isabelle distribution},
194 author = {J. Roger Hindley},
195 title = {Basic Simple Type Theory},
196 publisher = {Cambridge University Press},
198 editor = {S. Abramsky and P. H. Aczel and others},
200 series = {Cambridge Tracts in Theoretical Computer Science},
201 address = {Cambridge},
206 author = {Milner, R.},
207 title = {A Theory of Type Polymorphism in Programming},
208 journal = {Journal of Computer and System Science (JCSS)},
215 @inproceedings{Wenzel-11:doc-orient,
216 author = {Wenzel, Makarius},
217 title = {Isabelle as document-oriented proof assistant},
218 booktitle = {Proceedings of the 18th Calculemus and 10th international conference on Intelligent computer mathematics},
221 isbn = {978-3-642-22672-4},
222 location = {Bertinoro, Italy},
225 url = {http://dl.acm.org/citation.cfm?id=2032713.2032732},
227 publisher = {Springer-Verlag},
228 address = {Berlin, Heidelberg},
230 @InProceedings{makar-jedit-12,
231 author = {Makarius Wenzel},
232 title = {Isabelle/{jEdit} — a Prover IDE within the {PIDE} framework},
233 booktitle = {Conference on Intelligent Computer Mathematics (CICM 2012)},
235 editor = { J. Jeuring and others},
238 publisher = {Springer}
241 @InProceedings{Makarius-09:parall-proof,
242 author = {Wenzel, Makarius},
243 title = {Parallel Proof Checking in {Isabelle/Isar}},
244 booktitle = {ACM SIGSAM 2009 International Workshop on Programming Languages for Mechanized Mathematics Systems (PLMMS)},
246 editor = {Dos Reis and L. Th\'ery},
249 publisher = {ACM Digital library}
253 author = {Jean Francois Monin and Michael G. Hinchey},
254 title = {Understanding formal methods},
255 publisher = {Springer},
260 author = {Bj{\o}rner, Dines},
261 title = {Domain Engineering. Technology Management, Research and Engineering},
262 publisher = {JAIST Press},
265 series = {COE Research Monograph Series},
267 address = {Nomi, Japan}