1 \documentclass[a4paper, 12pt]{article}
3 \usepackage[english]{babel}
4 \usepackage[T1]{fontenc}
5 \usepackage[latin1]{inputenc}
12 \usepackage[pdfpagelabels]{hyperref}
13 \usepackage{longtable}
15 \usepackage{isabelle,isabellesym}
18 \def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
19 \def\sisac{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
23 %----------// INFO SETUP \\----------%
27 \bf Interactive Course Material for Signal Processing based on Isabelle/\isac\\~\\
29 \sisac-Team in Cooperation with \\~\\
30 Institute for Software Technology\\
31 Institute of Signal Processing and Speech Communication\\~\\
32 Graz University of Technology\\
35 Supervisor: Univ.-Prof. Dipl.-Ing. Dr.techn. Franz Wotawa
39 \author{Jan Simon Rocnik\\\href{mailto:student.tugraz.at}{\tt jan.rocnik@student.tugraz.at}}
43 %----------// TITLE PAGE \\----------%
47 \thispagestyle{empty}\end{titlepage}
50 %----------// THANKS \\----------%
56 \emph{Dr.techn. Walther Neuper}\\
57 \emph{Dipl.-Ing. Bernhard Geiger}
62 %----------// ABSTRACT \\----------%
65 The Baccalaureate Thesis creates interactive course material for Signal Processing based on the experimental math assistant Isabelle/\sisac.
67 The content of the course material is defined together with the Signal Processing and Speech Communication Laboratory (SPSC Lab) of Graz University of Technology (TUG). The content is planned to be used in specific lectures and labs of the SPSC and thus is thoroughly concerned with underlying mathematical and physical theory.
69 One challenge of this thesis is, that theory is not yet mechanized in Computer Theorem Provers (CTP); so this thesis will provide preliminary definitions in so-called \emph{theories} of the CTP Isabelle and theorems without proofs.
71 Another callenge is the implementation of interactive courses: this is done within the educational math assistant Isabelle/\sisac, which is under development at TU Graz. The present state of \sisac{} happens to provide the {\em first} occasion for authoring by a non-member of the \sisac{} developer team. So this challenge involves alpha-testing of the underlying ``CTP-based programming language'', because error messages are still not user-friendly and need frequent contact with \sisac-developers.
73 So the practical outcome of this thesis is twofold:
75 (1) interactive course material hopefully useful in education within the SPSC Lab and within STEOP, the introductory orientation phase at TUG, as a preview for students in Telematics on later application of math knowledge introduced in the first semester and
77 (2) a detailed description of technicalities in programming implemented as an interactive Isabelle/Isar theory, providing future programmers with guidelines and \sisac-developers with feedback in usability of the CTP-based program language.
78 \end{abstract}\clearpage
84 \pagenumbering{arabic}
88 This thesis is structured into a generell part describing the math fundamentals, a practical part including the work on \cal{ISAC} and finally the management part overviewing the work process.
90 %----------// PART-1 \\----------%
92 \part{Project Fundamentals}
94 \section{Introduction --TODO--}
96 The motivation to this thesis mainly takes it source from thr practice of mathematics learning and further ... STEOP
97 \cite{proakis2004contemporary}
99 \textbf{mathematics applied} in signal processing (SP)
101 mathematics mechanized in Computer Theorem Provers \textbf{(CTP)} ... (almost) traditional mathematical notation (predicate calculus) for axioms, definitions, lemmas, theorems. Recent developments provide also proofs in a humand readable format TODO
103 This thesis tries to \textbf{connect these two worlds} ... this trial is one of the first; others see related work
105 the major challenge of the practical part is, that ``connecting the two worlds'' involves programming in a CTP-based programming language which is in a very early state of prototyping.
107 \subsection{Mechanization of Mathematics}
111 hughe theories of mathematics
113 still a hugh gap between these theories and ``real applications'' e.g. in SP
115 ? academic engineering starts from physics (experimentation, measurement) and then proceeds to mathematical modelling --- mechanized math starts from mathematical models and (hopefully !) proceeds to match physics.
117 CTP Isabelle ... survey of knowledge, links to knowledge
122 adds an ``application'' axis (formal specifications of problems) and an ``algorithmic'' axis to the ``deductive'' axis of knowledge ... 3-dimensional universe of mathematics.
124 \subsection{Goals of the Thesis}
129 \subsection{Structure of the Thesis}
133 \section{Mechanization of Mathematics for SP Problems}
136 \subsection{Relevant Knowledge available in Isabelle}
139 \paragraph{example FFT}, describe in detail !!!!
141 ? different meaning: FFT in Maple
143 gap between what is available and what is required (@)!
145 traditional notation ?
147 \subsection{Relevant Knowledge available in isac}
150 specifications (``application axis'') and methods (``algorithmic axis'')
152 partial fractions, cancellation of multivariate rational terms, ...
154 \subsection{Survey: Available Knowledge and Selected Problems}
157 estimate gap (@) for each problem (tables)
159 conclusion: following order for implementing the problems ...
161 \subsection{Formalization of missing knowledge in Isabelle}
164 axiomatization ... where ... and
166 \subsection{Notes on Problems with Traditional Notation}
171 f x = why not f(x) ?!?!
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,...)
177 %----------// PART 2 \\----------%
179 \part{Implementation}
181 %\section{Implementation of Certain SP Problems}
182 %tell why only choosen one problem given by geiger
184 %\subsection{Formal Specification of Problems}
187 %\subsection{Methods Solving the Problems}
190 %\subsection{Integration of Subproblems available in isac}
193 %\subsection{Examples and Multimedia Content}
197 %\input{../../../test/Tools/isac/ADDTESTS/course/SignalProcess/document/Build_Inverse_Z_Transform}
201 %----------// PART 3 \\----------%
203 \part{Project Management}
205 \section{Milestones for the Project}
206 Die Planung des Projekts teilt sich in folgende Iterationen:
208 \item \textbf{Sammeln von Informationen "uber Themengebiete und deren Realisierbarkeit } (29.06. -- 27.07.)
209 identify problems relevant for certain SP lectures
211 estimate chances to realized them within the scope of this thesis
213 order for implementing the problems negotiated with lecturers
216 \item \textbf{1. Prsentation - Auswhlen der realisierbaren Themengebiete} (27.07.)
217 \item \textbf{Ausarbeiten der Aufgaben in \isac} (01.09. -- 11.11.)
218 \item \textbf{Dokumentation der Aufgaben} (14.11. -- 02.12.)
219 \item \textbf{Ausarbeitung in Latex, Bakkarbeit} (05.12. -- todo)
220 \item \textbf{2. Prsentation - Abschluss der Arbeit} (todo)
223 \section{Beschreibung der Meilensteine}\label{ms-desc}
225 \section{Bericht zum Projektverlauf}
228 \section{Related Work and Open Questions}
231 See ``introduction'': This thesis tries to connect these two worlds ... this trial is one of the first; others see related work
233 \section{Abschliesende Bemerkungen}
240 \renewcommand{\refname}{\section{Sources}} % Using "Sources" as the title of the section
241 \bibliographystyle{alpha}
242 \bibliography{references}
247 %----------// APPENDIX \\-----------%
252 \section{Stundenliste}
254 \begin{longtable}[h]{l p{6.5cm} c c r}
255 {\bf Date} & {\bf Description} & {\bf Begin} & {\bf End} & {\bf Dur.}\\
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\\
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
301 \section{Calculations}