jan@42322: %   Title:  bakkarbeit_jrocnik.tex
jan@42322: %   Author: Jan Rocnik
jan@42322: %   (c) copyright due to lincense terms.
jan@42322: %2345678901234567890123456789012345678901234567890123456789012345678901234567890
jan@42322: %       10        20        30        40        50        60        70        80
jan@42322: 
jan@42322: %TODO:
jan@42322: %%\cite{proakis2004contemporary}
jan@42322: %%--01-- pointer or label to related works
jan@42322: 
jan@42322: %define document class
jan@42307: \documentclass[a4paper, 12pt]{article}
jan@42235: 
jan@42322: %packages for language and input
jan@42307: \usepackage[english]{babel} 
jan@42235: \usepackage[T1]{fontenc}
jan@42235: \usepackage[latin1]{inputenc}
jan@42235: 
jan@42322: %generel packages
jan@42307: \usepackage{url}
neuper@42073: \usepackage{graphicx}
jan@42246: \usepackage{endnotes}
jan@42246: \usepackage{trfsigns}
jan@42246: \usepackage{setspace}
jan@42307: \usepackage[pdfpagelabels]{hyperref}
jan@42316: \usepackage{longtable}
jan@42322: 
jan@42322: %isabelle relevant packages
jan@42316: \usepackage{isabelle,isabellesym}
jan@42235: 
jan@42322: %define isac logos
neuper@42073: \def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
neuper@42073: \def\sisac{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
neuper@42073: 
jan@42322: %----------// BEGIN DOCUMENT \\----------%
jan@42322: 
neuper@42073: \begin{document}
neuper@42073: 
jan@42316: %----------// INFO SETUP \\----------%
jan@42316: 
jan@42235: \title{
jan@42235: 	\Large{
jan@42235:   	\bf Interactive Course Material for Signal Processing based on Isabelle/\isac\\~\\
jan@42235:   }
jan@42307: 	\sisac-Team in Cooperation with \\~\\
jan@42307: 	Institute for Software Technology\\
jan@42307: 	Institute of Signal Processing and Speech Communication\\~\\
jan@42276: 	Graz University of Technology\\
jan@42235: 	\vspace{0.7cm}
jan@42307: 	\normalsize{
jan@42316: 		Supervisor: Univ.-Prof. Dipl.-Ing. Dr.techn. Franz Wotawa
jan@42235: 	}
jan@42235: }
jan@42307: 
jan@42307: \author{Jan Simon Rocnik\\\href{mailto:student.tugraz.at}{\tt jan.rocnik@student.tugraz.at}}
jan@42235: 
jan@42235: \date{\today}
jan@42307: 
jan@42316: %----------// TITLE PAGE \\----------%
jan@42316: 
jan@42307: \begin{titlepage}
neuper@42073: \maketitle
jan@42307: \thispagestyle{empty}\end{titlepage}
neuper@42073: \clearpage
jan@42307: 
jan@42316: %----------// THANKS \\----------%
jan@42316: 
jan@42307: \setcounter{page}{2}
jan@42307: \begin{center}
jan@42307: Special Thanks to\\
jan@42307: \hfill \\
jan@42307: \emph{Dr.techn. Walther Neuper}\\
jan@42307: \emph{Dipl.-Ing. Bernhard Geiger}
jan@42307: \end{center}
jan@42307: \thispagestyle{empty}
jan@42307: \clearpage
jan@42307: 
jan@42316: %----------// ABSTRACT \\----------%
jan@42307: 
jan@42307: \begin{abstract}
jan@42307: The Baccalaureate Thesis creates interactive course material for Signal Processing based on the experimental math assistant Isabelle/\sisac.
jan@42307: 
jan@42307: 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.
jan@42307: 
jan@42307: 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.
jan@42307: 
jan@42307: 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.
jan@42307: 
jan@42307: So the practical outcome of this thesis is twofold:
jan@42307: 
jan@42307: (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
jan@42307: 
jan@42307: (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. 
jan@42307: \end{abstract}\clearpage
jan@42307: 
jan@42307: 
jan@42307: \pagenumbering{Roman}
neuper@42073: \tableofcontents
neuper@42073: \clearpage
jan@42307: \pagenumbering{arabic}
neuper@42073: 
jan@42307: \setcounter{page}{5}
jan@42316: 
jan@42316: 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.
jan@42316: 
jan@42316: %----------// PART-1 \\----------%
jan@42316: 
jan@42316: \part{Project Fundamentals}
neuper@42304: 
jan@42322: \section{Introduction}
neuper@42073: 
jan@42322: The motivation to this thesis mainly takes it source from the feeling of understanding difficult signal processing tasks and the will to help others to get this feeling to.
jan@42322: \par Signal Processing requieres a huge range of mathematic knowledge as well as a feeling for simplification and number tricks but even though this fact, the operations themself are no higher ones. The main task is to understand. Aside this description we think of the classic math ideas and techniques, consisting of predefined formulas, notations and forumularsations we learn.
jan@42322: \par Mathematics mechanized in Computer Theorem Provers \emph{(CTP)} has (almost) a problem with traditional mathematical notations (predicate calculus) for axioms, definitions, lemmas, theorems as a computer programm or script is not able to interpret every greek or latin letter and every greek, latin or whatever calculations symbol. Also if we would be able to handle thehse symbols we would have a problem to interpret them correctly. In different problems, symbols and letters have different meanings and ask for different ways to get through. Exclusive from the input, also the output can be a problem. We are familar with a specified notations and style taught in university but a computer programm has no knowledge of the form probved by a professor and the maschines themselve also have not yet the possibilities to print every symbol (correct) Recent developments provide proofs in a humand readable format but according to the fact that there is no mony for good working formel editors yet, the style is one thing we have to live with.
jan@42322: \par This thesis tries to \empg{connect} these two worlds and is one of the first guidelines to implement problem classes in {\sisac}. For others see related works. %--01--
jan@42322: The major challenge of the practical part, of this thesis, is, that "`connecting the two worlds"' involves programming in a CTP-based programming language which is in a very early state of prototyping. There is no concrete experience data ready to hand.
neuper@42304: 
neuper@42240: \subsection{Mechanization of Mathematics}
neuper@42073: 
jan@42235: todo
neuper@42073: 
neuper@42240: hughe theories of mathematics
neuper@42240: 
neuper@42240: still a hugh gap between these theories and ``real applications'' e.g. in SP
neuper@42240: 
neuper@42240: ? 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.
neuper@42240: 
neuper@42240: CTP Isabelle ... survey of knowledge, links to knowledge
neuper@42240: 
neuper@42240: \paragraph{\sisac}
neuper@42240: TODO
neuper@42240: 
neuper@42240: adds an ``application'' axis (formal specifications of problems) and an ``algorithmic'' axis to the ``deductive'' axis of knowledge ... 3-dimensional universe of mathematics.
neuper@42240: 
neuper@42240: \subsection{Goals of the Thesis}
neuper@42240: 
neuper@42240: todo
neuper@42240: 
neuper@42073: 
neuper@42240: \subsection{Structure of the Thesis}
neuper@42240: 
jan@42235: todo
neuper@42240: 
neuper@42240: \section{Mechanization of Mathematics for SP Problems}
neuper@42240: todo
neuper@42240: 
neuper@42240: \subsection{Relevant Knowledge available in Isabelle}
neuper@42240: todo
neuper@42240: 
neuper@42240: \paragraph{example FFT}, describe in detail !!!! 
neuper@42240: 
neuper@42240: ? different meaning: FFT in Maple
neuper@42240: 
neuper@42240: gap between what is available and what is required (@)!
neuper@42240: 
neuper@42240: traditional notation ?
neuper@42240: 
jan@42307: \subsection{Relevant Knowledge available in isac}
neuper@42240: todo
neuper@42240: 
neuper@42240: specifications (``application axis'') and methods (``algorithmic axis'')
neuper@42240: 
neuper@42240: partial fractions, cancellation of multivariate rational terms, ...
neuper@42240: 
neuper@42240: \subsection{Survey: Available Knowledge and Selected Problems}
neuper@42240: todo
neuper@42240: 
neuper@42240: estimate gap (@) for each problem (tables)
neuper@42240: 
neuper@42240: conclusion: following order for implementing the problems ...
neuper@42240: 
neuper@42240: \subsection{Formalization of missing knowledge in Isabelle}
neuper@42240: todo
neuper@42240: 
neuper@42240: axiomatization ... where ... and
neuper@42240: 
neuper@42240: \subsection{Notes on Problems with Traditional Notation}
jan@42322: Due the thesis work we discorvers severell problems of traditional notations.
neuper@42240: 
neuper@42240: u[n] !!
neuper@42240: 
neuper@42240: f x =  why not f(x) ?!?!
neuper@42240: 
neuper@42240: ...
neuper@42240: 
jan@42276: 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,...)
jan@42276: 
jan@42316: %----------// PART 2 \\----------%
jan@42316: 
jan@42316: \part{Implementation}
jan@42316: 
jan@42316: %\section{Implementation of Certain SP Problems}
jan@42316: %tell why only choosen one problem given by geiger
jan@42316: %
jan@42316: %\subsection{Formal Specification of Problems}
jan@42316: %todo
jan@42316: %
jan@42316: %\subsection{Methods Solving the Problems}
jan@42316: %todo
jan@42316: %
jan@42316: %\subsection{Integration of Subproblems available in isac}
jan@42316: %todo
jan@42316: %
jan@42316: %\subsection{Examples and Multimedia Content}
jan@42316: %todo
jan@42316: 
jan@42316: {\center todo}
jan@42322: \input{../../../test/Tools/isac/ADDTESTS/course/SignalProcess/document/Build_Inverse_Z_Transform}
jan@42316: 
jan@42316: \clearpage
jan@42316: 
jan@42316: %----------// PART 3 \\----------%
jan@42316: 
jan@42316: \part{Project Management}
jan@42316: 
jan@42316: \section{Milestones for the Project}
jan@42316: Die Planung des Projekts teilt sich in folgende Iterationen:
jan@42316: \begin{enumerate}
jan@42316: \item \textbf{Sammeln von Informationen "uber Themengebiete und deren Realisierbarkeit } (29.06. -- 27.07.)
jan@42316: identify problems relevant for certain SP lectures
jan@42316: 
jan@42316: estimate chances to realized them within the scope of this thesis
jan@42316: 
jan@42316: order for implementing the problems negotiated with lecturers
jan@42316: 
jan@42316: 
jan@42316: \item \textbf{1. Prsentation - Auswhlen der realisierbaren Themengebiete} (27.07.)
jan@42316: \item \textbf{Ausarbeiten der Aufgaben in \isac} (01.09. -- 11.11.)
jan@42316: \item \textbf{Dokumentation der Aufgaben} (14.11. -- 02.12.)
jan@42316: \item \textbf{Ausarbeitung in Latex, Bakkarbeit} (05.12. -- todo)
jan@42316: \item \textbf{2. Prsentation - Abschluss der Arbeit} (todo)
jan@42316: \end{enumerate}
jan@42316: 
jan@42316: \section{Beschreibung der Meilensteine}\label{ms-desc}
neuper@42240: todo
jan@42316: \section{Bericht zum Projektverlauf}
neuper@42240: todo
neuper@42240: 
neuper@42240: \section{Related Work and Open Questions}
neuper@42240: todo
neuper@42240: 
neuper@42240: See ``introduction'': This thesis tries to connect these two worlds ... this trial is one of the first; others see related work
neuper@42240: 
jan@42235: \section{Abschliesende Bemerkungen}
jan@42235: todo
neuper@42073: 
jan@42316: 
jan@42316: 
neuper@42073: \clearpage
neuper@42073: 
jan@42309: \renewcommand{\refname}{\section{Sources}} % Using "Sources" as the title of the section
jan@42309: \bibliographystyle{alpha}
jan@42309: \bibliography{references}
neuper@42073: 
neuper@42073: \clearpage
neuper@42073: 
jan@42316: 
jan@42316: %----------// APPENDIX \\-----------%
jan@42316: 
neuper@42073: \appendix
jan@42251: 
neuper@42073: 
neuper@42073: \section{Stundenliste}
jan@42316: \begin{footnotesize}
jan@42316: \begin{longtable}[h]{l p{6.5cm} c c r}
jan@42316: {\bf Date} & {\bf Description} & {\bf Begin} & {\bf End} & {\bf Dur.}\\
jan@42316: \hline \hline
jan@42316: \endhead
jan@42316: 29.06.2011 & Treffen mit Geiger und Neuper & 15:00 & 17:30 & 2,50\\ 
jan@42316: 02.07.2011 & Beispielaufbereitung (Bsp. Geiger Mail) & 20:00 & 21:30 & 1,50\\ 
jan@42316: 03.07.2011 & Beispielaufbereitung, Vorraussetzungsausw. & 21:00 & 22:45 & 1,75\\ 
jan@42316: 05.07.2011 & Treffen mit Neuper, Informationsaustausch & 10:00 & 13:00 & 3,00\\ 
jan@42316: 06.07.2011 & Isabelle Installation & 20:00 & 22:30 & 2,50\\ 
jan@42316: 07.07.2011 & Treffen mit Neuper, Präsentationsvorbereitung & 14:45 & 16:15 & 1,50\\ 
jan@42316: 18.07.2011 & Präsentationsvorbereitung - Struktur & 14:15 & 16:00 & 1,75\\ 
jan@42316: 19.07.2011 & Präsentationsvorbereitung - Inhalt & 07:20 & 09:20 & 2,00\\ 
jan@42316: 19.07.2011 & Treffen mit Neuper & 10:00 & 12:00 & 2,00\\ 
jan@42316: 21.07.2011 & HG Fehlersuche, Latex Ausarbeitung & 11:10 & 14:00 & 2,83\\ 
jan@42316: 22.07.2011 & Treffen mit Neuper & 10:00 & 12:00 & 2,00\\ 
jan@42316: 23.07.2011 & Berechnungen in Latex fertigstellen & 13:45 & 16:30 & 2,75\\ 
jan@42316: 24.07.2011 & Präsentation fertigstellen & 20:10 & 20:40 & 0,50\\ 
jan@42316: 25.07.2011 & Treffen mit Neuper, Präsentation \& erste Tests & 15:15 & 17:55 & 2,67\\ 
jan@42316: 26.07.2011 & Test\_Complex.thy erarbeiten & 10:45 & 12:10 & 1,42\\ 
jan@42316: 27.07.2011 & present-1 mit Neuper, Geiger & 10:00 & 12:00 & 2,00\\
jan@42316: \hline 
jan@42316: 02.09.2011 & Treffen mit Neuper, Vorlage Bakk-Arbeit & 08:30 & 10:20 & 1,83\\ 
jan@42316: 05.09.2011 & Treffen mit Neuper, Beginn Partialbruchzerlegung & 09:30 & 12:45 & 3,25\\ 
jan@42316: 05.09.2011 & Partialbruchzerlegung & 17:10 & 18:30 & 1,33\\ 
jan@42316: 06.09.2011 & Dokumentation Partialbruchzerlegung & 10:00 & 13:15 & 3,25\\ 
jan@42316: 07.09.2011 & Treffen mit Neuper, Einführung Programmierung & 10:00 & 12:50 & 2,83\\ 
jan@42316: 08.09.2011 & Latex Umgebung einrichten - Theory export & 19:00 & 22:45 & 3,75\\ 
jan@42316: 09.09.2011 & Latex Umgebung einrichten - Makefile & 11:40 & 15:00 & 3,33\\ 
jan@42316: 10.09.2011 & Treffen mit Neuper, HG Fehler, Skript Inv.-Z-Transf. & 10:00 & 12:00 & 2,00\\ 
jan@42316: 14.09.2011 & Skript Inv.-Z-Transf Prgrammierung & 09:10 & 12:25 & 3,25\\ 
jan@42316: 16.09.2011 & Informationssammlung Summen & 13:15 & 16:00 & 2,75\\ 
jan@42316: 19.09.2011 & Programmierübung & 10:00 & 13:10 & 3,17\\ 
jan@42316: 20.09.2011 & Trefffen mit Neuper, Unterstützung bei Program. & 15:30 & 18:10 & 2,67\\ 
jan@42316: 23.09.2011 & Neukonfiguration IsaMakefile & 13:00 & 14:30 & 1,50\\ 
jan@42316: 23.09.2011 & Treffen Neuper, Programmierung Build\_Inverse\_Z & 14:30 & 17:30 & 3,00\\ 
jan@42316: 26.09.2011 & Skript Partialbruchzerlegung - getArgument & 13:30 & 16:15 & 2,75\\ 
jan@42316: 27.09.2011 & Treffen mit Neuper, HG Fehler & 09:00 & 12:20 & 3,33\\ 
jan@42316: 28.09.2011 & Treffen mit Neuper, Dateiumstrukturierung & 10:00 & 12:30 & 2,50\\ 
jan@42316: 01.10.2011 & Testen & 10:00 & 11:00 & 1,00\\ 
jan@42316: 02.10.2011 & Fehlersuche & 15:00 & 16:10 & 1,17\\ 
jan@42316: 06.10.2011 & Treffen mit Neuper & 15:00 & 17:50 & 2,83\\ 
jan@42316: 07.10.2011 & Treffen mit Neuper, Programmbesprechung & 15:00 & 16:50 & 1,83\\ 
jan@42316: 09.10.2011 & Bakk. Arbeit & 16:30 & 18:45 & 2,25\\ 
jan@42316: 11.10.2011 & Treffen mit Neuper, Programmbespr., Abstract & 14:10 & 17:10 & 3,00
jan@42316: \end{longtable}
jan@42316: \end{footnotesize}
neuper@42073: 
jan@42246: \section{Calculations}
jan@42251: \input{calulations}
neuper@42073: \end{document}