109 |
123 |
110 \subsection{Goals of the Thesis} |
124 \subsection{Goals of the Thesis} |
111 |
125 |
112 todo |
126 todo |
113 |
127 |
114 \subsection{Milestones for the Project} |
128 |
|
129 \subsection{Structure of the Thesis} |
|
130 |
|
131 todo |
|
132 |
|
133 \section{Mechanization of Mathematics for SP Problems} |
|
134 todo |
|
135 |
|
136 \subsection{Relevant Knowledge available in Isabelle} |
|
137 todo |
|
138 |
|
139 \paragraph{example FFT}, describe in detail !!!! |
|
140 |
|
141 ? different meaning: FFT in Maple |
|
142 |
|
143 gap between what is available and what is required (@)! |
|
144 |
|
145 traditional notation ? |
|
146 |
|
147 \subsection{Relevant Knowledge available in isac} |
|
148 todo |
|
149 |
|
150 specifications (``application axis'') and methods (``algorithmic axis'') |
|
151 |
|
152 partial fractions, cancellation of multivariate rational terms, ... |
|
153 |
|
154 \subsection{Survey: Available Knowledge and Selected Problems} |
|
155 todo |
|
156 |
|
157 estimate gap (@) for each problem (tables) |
|
158 |
|
159 conclusion: following order for implementing the problems ... |
|
160 |
|
161 \subsection{Formalization of missing knowledge in Isabelle} |
|
162 todo |
|
163 |
|
164 axiomatization ... where ... and |
|
165 |
|
166 \subsection{Notes on Problems with Traditional Notation} |
|
167 todo |
|
168 |
|
169 u[n] !! |
|
170 |
|
171 f x = why not f(x) ?!?! |
|
172 |
|
173 ... |
|
174 |
|
175 terms are not full simplified in traditional notations, in isac we have to simplify them complete to check weather results are compatible or not. in e.g. the solutions of an second order linear equation is an rational in isac but in tradition we keep fractions as long as possible and as long as they are 'beautiful' (1/8, 5/16,...) |
|
176 |
|
177 %----------// PART 2 \\----------% |
|
178 |
|
179 \part{Implementation} |
|
180 |
|
181 %\section{Implementation of Certain SP Problems} |
|
182 %tell why only choosen one problem given by geiger |
|
183 % |
|
184 %\subsection{Formal Specification of Problems} |
|
185 %todo |
|
186 % |
|
187 %\subsection{Methods Solving the Problems} |
|
188 %todo |
|
189 % |
|
190 %\subsection{Integration of Subproblems available in isac} |
|
191 %todo |
|
192 % |
|
193 %\subsection{Examples and Multimedia Content} |
|
194 %todo |
|
195 |
|
196 {\center todo} |
|
197 %\input{../../../test/Tools/isac/ADDTESTS/course/SignalProcess/document/Build_Inverse_Z_Transform} |
|
198 |
|
199 \clearpage |
|
200 |
|
201 %----------// PART 3 \\----------% |
|
202 |
|
203 \part{Project Management} |
|
204 |
|
205 \section{Milestones for the Project} |
115 Die Planung des Projekts teilt sich in folgende Iterationen: |
206 Die Planung des Projekts teilt sich in folgende Iterationen: |
116 \begin{enumerate} |
207 \begin{enumerate} |
117 \item \textbf{Sammeln von Informationen "uber Themengebiete und deren Realisierbarkeit } (29.06. -- 27.07.) |
208 \item \textbf{Sammeln von Informationen "uber Themengebiete und deren Realisierbarkeit } (29.06. -- 27.07.) |
118 identify problems relevant for certain SP lectures |
209 identify problems relevant for certain SP lectures |
119 |
210 |
127 \item \textbf{Dokumentation der Aufgaben} (14.11. -- 02.12.) |
218 \item \textbf{Dokumentation der Aufgaben} (14.11. -- 02.12.) |
128 \item \textbf{Ausarbeitung in Latex, Bakkarbeit} (05.12. -- todo) |
219 \item \textbf{Ausarbeitung in Latex, Bakkarbeit} (05.12. -- todo) |
129 \item \textbf{2. Prsentation - Abschluss der Arbeit} (todo) |
220 \item \textbf{2. Prsentation - Abschluss der Arbeit} (todo) |
130 \end{enumerate} |
221 \end{enumerate} |
131 |
222 |
132 \subsection{Structure of the Thesis} |
223 \section{Beschreibung der Meilensteine}\label{ms-desc} |
133 |
224 todo |
134 todo |
225 \section{Bericht zum Projektverlauf} |
135 |
226 todo |
136 \section{Mechanization of Mathematics for SP Problems} |
|
137 todo |
|
138 |
|
139 \subsection{Relevant Knowledge available in Isabelle} |
|
140 todo |
|
141 |
|
142 \paragraph{example FFT}, describe in detail !!!! |
|
143 |
|
144 ? different meaning: FFT in Maple |
|
145 |
|
146 gap between what is available and what is required (@)! |
|
147 |
|
148 traditional notation ? |
|
149 |
|
150 \subsection{Relevant Knowledge available in isac} |
|
151 todo |
|
152 |
|
153 specifications (``application axis'') and methods (``algorithmic axis'') |
|
154 |
|
155 partial fractions, cancellation of multivariate rational terms, ... |
|
156 |
|
157 \subsection{Survey: Available Knowledge and Selected Problems} |
|
158 todo |
|
159 |
|
160 estimate gap (@) for each problem (tables) |
|
161 |
|
162 conclusion: following order for implementing the problems ... |
|
163 |
|
164 \subsection{Formalization of missing knowledge in Isabelle} |
|
165 todo |
|
166 |
|
167 axiomatization ... where ... and |
|
168 |
|
169 \subsection{Notes on Problems with Traditional Notation} |
|
170 todo |
|
171 |
|
172 u[n] !! |
|
173 |
|
174 f x = why not f(x) ?!?! |
|
175 |
|
176 ... |
|
177 |
|
178 terms are not full simplified in traditional notations, in isac we have to simplify them complete to check weather results are compatible or not. in e.g. the solutions of an second order linear equation is an rational in isac but in tradition we keep fractions as long as possible and as long as they are 'beautiful' (1/8, 5/16,...) |
|
179 |
|
180 \section{Implementation of Certain SP Problems} |
|
181 todo |
|
182 |
|
183 \subsection{Formal Specification of Problems} |
|
184 todo |
|
185 |
|
186 \subsection{Methods Solving the Problems} |
|
187 todo |
|
188 |
|
189 \subsection{Integration of Subproblems available in isac} |
|
190 todo |
|
191 |
|
192 \subsection{Examples and Multimedia Content} |
|
193 todo |
|
194 |
|
195 |
227 |
196 \section{Related Work and Open Questions} |
228 \section{Related Work and Open Questions} |
197 todo |
229 todo |
198 |
230 |
199 See ``introduction'': This thesis tries to connect these two worlds ... this trial is one of the first; others see related work |
231 See ``introduction'': This thesis tries to connect these two worlds ... this trial is one of the first; others see related work |
200 |
232 |
201 |
|
202 |
|
203 \section{Beschreibung der Meilensteine}\label{ms-desc} |
|
204 todo |
|
205 \section{Bericht zum Projektverlauf} |
|
206 todo |
|
207 \section{Abschliesende Bemerkungen} |
233 \section{Abschliesende Bemerkungen} |
208 todo |
234 todo |
|
235 |
|
236 |
209 |
237 |
210 \clearpage |
238 \clearpage |
211 |
239 |
212 \renewcommand{\refname}{\section{Sources}} % Using "Sources" as the title of the section |
240 \renewcommand{\refname}{\section{Sources}} % Using "Sources" as the title of the section |
213 \bibliographystyle{alpha} |
241 \bibliographystyle{alpha} |
214 \bibliography{references} |
242 \bibliography{references} |
215 |
243 |
216 \clearpage |
244 \clearpage |
217 |
245 |
|
246 |
|
247 %----------// APPENDIX \\-----------% |
|
248 |
218 \appendix |
249 \appendix |
219 %\section*{Anhang} |
250 |
220 \section{Demobeispiel} |
|
221 |
|
222 %\input{./Inverse_Z_Transform/document/Inverse_Z_Transform.tex} |
|
223 |
|
224 \begin{verbatim} |
|
225 |
|
226 bsp |
|
227 |
|
228 \end{verbatim} |
|
229 |
251 |
230 \section{Stundenliste} |
252 \section{Stundenliste} |
231 |
253 \begin{footnotesize} |
232 \subsection*{Voraussetzungen zum Arbeitsbeginn schaffen} |
254 \begin{longtable}[h]{l p{6.5cm} c c r} |
233 \begin{tabular}[t]{lll} |
255 {\bf Date} & {\bf Description} & {\bf Begin} & {\bf End} & {\bf Dur.}\\ |
234 {\bf Datum} & {\bf Stunden} & {\bf Beschreibung} \\ |
256 \hline \hline |
235 10.02.2011 & 2:00 & Besprechung der Problemstellung \\ |
257 \endhead |
236 \end{tabular} |
258 29.06.2011 & Treffen mit Geiger und Neuper & 15:00 & 17:30 & 2,50\\ |
|
259 02.07.2011 & Beispielaufbereitung (Bsp. Geiger Mail) & 20:00 & 21:30 & 1,50\\ |
|
260 03.07.2011 & Beispielaufbereitung, Vorraussetzungsausw. & 21:00 & 22:45 & 1,75\\ |
|
261 05.07.2011 & Treffen mit Neuper, Informationsaustausch & 10:00 & 13:00 & 3,00\\ |
|
262 06.07.2011 & Isabelle Installation & 20:00 & 22:30 & 2,50\\ |
|
263 07.07.2011 & Treffen mit Neuper, Präsentationsvorbereitung & 14:45 & 16:15 & 1,50\\ |
|
264 18.07.2011 & Präsentationsvorbereitung - Struktur & 14:15 & 16:00 & 1,75\\ |
|
265 19.07.2011 & Präsentationsvorbereitung - Inhalt & 07:20 & 09:20 & 2,00\\ |
|
266 19.07.2011 & Treffen mit Neuper & 10:00 & 12:00 & 2,00\\ |
|
267 21.07.2011 & HG Fehlersuche, Latex Ausarbeitung & 11:10 & 14:00 & 2,83\\ |
|
268 22.07.2011 & Treffen mit Neuper & 10:00 & 12:00 & 2,00\\ |
|
269 23.07.2011 & Berechnungen in Latex fertigstellen & 13:45 & 16:30 & 2,75\\ |
|
270 24.07.2011 & Präsentation fertigstellen & 20:10 & 20:40 & 0,50\\ |
|
271 25.07.2011 & Treffen mit Neuper, Präsentation \& erste Tests & 15:15 & 17:55 & 2,67\\ |
|
272 26.07.2011 & Test\_Complex.thy erarbeiten & 10:45 & 12:10 & 1,42\\ |
|
273 27.07.2011 & present-1 mit Neuper, Geiger & 10:00 & 12:00 & 2,00\\ |
|
274 \hline |
|
275 02.09.2011 & Treffen mit Neuper, Vorlage Bakk-Arbeit & 08:30 & 10:20 & 1,83\\ |
|
276 05.09.2011 & Treffen mit Neuper, Beginn Partialbruchzerlegung & 09:30 & 12:45 & 3,25\\ |
|
277 05.09.2011 & Partialbruchzerlegung & 17:10 & 18:30 & 1,33\\ |
|
278 06.09.2011 & Dokumentation Partialbruchzerlegung & 10:00 & 13:15 & 3,25\\ |
|
279 07.09.2011 & Treffen mit Neuper, Einführung Programmierung & 10:00 & 12:50 & 2,83\\ |
|
280 08.09.2011 & Latex Umgebung einrichten - Theory export & 19:00 & 22:45 & 3,75\\ |
|
281 09.09.2011 & Latex Umgebung einrichten - Makefile & 11:40 & 15:00 & 3,33\\ |
|
282 10.09.2011 & Treffen mit Neuper, HG Fehler, Skript Inv.-Z-Transf. & 10:00 & 12:00 & 2,00\\ |
|
283 14.09.2011 & Skript Inv.-Z-Transf Prgrammierung & 09:10 & 12:25 & 3,25\\ |
|
284 16.09.2011 & Informationssammlung Summen & 13:15 & 16:00 & 2,75\\ |
|
285 19.09.2011 & Programmierübung & 10:00 & 13:10 & 3,17\\ |
|
286 20.09.2011 & Trefffen mit Neuper, Unterstützung bei Program. & 15:30 & 18:10 & 2,67\\ |
|
287 23.09.2011 & Neukonfiguration IsaMakefile & 13:00 & 14:30 & 1,50\\ |
|
288 23.09.2011 & Treffen Neuper, Programmierung Build\_Inverse\_Z & 14:30 & 17:30 & 3,00\\ |
|
289 26.09.2011 & Skript Partialbruchzerlegung - getArgument & 13:30 & 16:15 & 2,75\\ |
|
290 27.09.2011 & Treffen mit Neuper, HG Fehler & 09:00 & 12:20 & 3,33\\ |
|
291 28.09.2011 & Treffen mit Neuper, Dateiumstrukturierung & 10:00 & 12:30 & 2,50\\ |
|
292 01.10.2011 & Testen & 10:00 & 11:00 & 1,00\\ |
|
293 02.10.2011 & Fehlersuche & 15:00 & 16:10 & 1,17\\ |
|
294 06.10.2011 & Treffen mit Neuper & 15:00 & 17:50 & 2,83\\ |
|
295 07.10.2011 & Treffen mit Neuper, Programmbesprechung & 15:00 & 16:50 & 1,83\\ |
|
296 09.10.2011 & Bakk. Arbeit & 16:30 & 18:45 & 2,25\\ |
|
297 11.10.2011 & Treffen mit Neuper, Programmbespr., Abstract & 14:10 & 17:10 & 3,00 |
|
298 \end{longtable} |
|
299 \end{footnotesize} |
237 |
300 |
238 \section{Calculations} |
301 \section{Calculations} |
239 \input{calulations} |
302 \input{calulations} |
240 |
|
241 |
|
242 \end{document} |
303 \end{document} |