
jan@42246: \documentclass[a4paper, 12pt]{scrartcl}
jan@42235: 
jan@42246: \usepackage[english,german]{babel} 
jan@42235: \usepackage[T1]{fontenc}
jan@42235: \usepackage[latin1]{inputenc}
jan@42235: 
neuper@42073: \usepackage{graphicx}
jan@42246: \usepackage{endnotes}
jan@42246: \usepackage{trfsigns}
jan@42246: \usepackage{setspace}
jan@42251: \usepackage{isabelle}
jan@42251: \usepackage{isabellesym}
jan@42235: 
neuper@42073: \bibliographystyle{alpha}
neuper@42073: 
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: 
neuper@42073: \begin{document}
neuper@42073: 
jan@42235: \title{
jan@42235: 	\Large{
jan@42235:   	\bf Interactive Course Material for Signal Processing based on Isabelle/\isac\\~\\
jan@42235:   }
jan@42276: 	\sisac-Team of the Institute for Software Technology,\\~\\
jan@42276: 	in Cooperation with the Institute of Signal Processing and Speech Communication\\~\\
jan@42276: 	Graz University of Technology\\
jan@42235: 	\vspace{0.7cm}
jan@42235: 	\large{
jan@42276: 		Advisor: tba
jan@42235: 	}
jan@42235: }
jan@42235: \author{Jan Simon Rocnik\\{\tt jan.rocnik@student.tugraz.at}}
jan@42235: 
jan@42235: \date{\today}
neuper@42073: \maketitle
neuper@42073: \clearpage
neuper@42073: \tableofcontents
neuper@42073: \clearpage
neuper@42073: 
neuper@42073: 
neuper@42240: \section{Introduction}
neuper@42073: 
jan@42235: todo
neuper@42073: 
neuper@42240: motivation from \textbf{practice of mathematics learning} ... STEOP
neuper@42240: 
neuper@42240: \textbf{mathematics applied} in signal processing (SP)
neuper@42240: 
jan@42253: 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
neuper@42240: 
neuper@42240: This thesis tries to \textbf{connect these two worlds} ... this trial is one of the first; others see related work
neuper@42240: 
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@42240: \subsection{Milestones for the Project}
jan@42235: Die Planung des Projekts teilt sich in folgende Iterationen:
neuper@42073: \begin{enumerate}
neuper@42240: \item \textbf{Sammeln von Informationen über Themengebiete und deren Realisierbarkeit } (29.06. -- 27.07.)
neuper@42240: identify problems relevant for certain SP lectures
neuper@42240: 
neuper@42240: estimate chances to realized them within the scope of this thesis
neuper@42240: 
neuper@42240: order for implementing the problems negotiated with lecturers
neuper@42240: 
neuper@42240: 
jan@42235: \item \textbf{1. Präsentation - Auswählen der realisierbaren Themengebiete} (27.07.)
jan@42235: \item \textbf{Ausarbeiten der Aufgaben in \isac} (01.09. -- 11.11.)
jan@42235: \item \textbf{Dokumentation der Aufgaben} (14.11. -- 02.12.)
jan@42235: \item \textbf{Ausarbeitung in Latex, Bakkarbeit} (05.12. -- todo)
jan@42235: \item \textbf{2. Präsentation - Abschluss der Arbeit} (todo)
neuper@42073: \end{enumerate}
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: 
neuper@42240: \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}
neuper@42240: todo
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: 
neuper@42240: \section{Implementation of Certain SP Problems}
neuper@42240: todo
neuper@42240: 
neuper@42240: \subsection{Formal Specification of Problems}
neuper@42240: todo
neuper@42240: 
neuper@42240: \subsection{Methods Solving the Problems}
neuper@42240: todo
neuper@42240: 
neuper@42240: \subsection{Integration of Subproblems available in \isac}
neuper@42240: todo
neuper@42240: 
neuper@42240: \subsection{Examples and Multimedia Content}
neuper@42240: todo
neuper@42240: 
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: 
neuper@42240: 
neuper@42240: 
neuper@42073: \section{Beschreibung der Meilensteine}\label{ms-desc}
jan@42235: todo
neuper@42073: \section{Bericht zum Projektverlauf}
jan@42235: todo
jan@42235: \section{Abschliesende Bemerkungen}
jan@42235: todo
neuper@42073: 
neuper@42073: \clearpage
neuper@42073: 
jan@42253: %\bibliography{bib}
neuper@42073: 
neuper@42073: \clearpage
neuper@42073: 
neuper@42073: \appendix
neuper@42073: %\section*{Anhang}
jan@42251: \section{Demobeispiel}
jan@42251: 
jan@42276: %\input{./Inverse_Z_Transform/document/Inverse_Z_Transform.tex}
jan@42251: 
neuper@42073: \begin{verbatim}
neuper@42073: 
jan@42235: bsp
neuper@42073: 
neuper@42073: \end{verbatim}
neuper@42073: 
neuper@42073: \section{Stundenliste}
neuper@42073: 
neuper@42073: \subsection*{Voraussetzungen zum Arbeitsbeginn schaffen}
neuper@42073: \begin{tabular}[t]{lll}
neuper@42073:     {\bf Datum} & {\bf Stunden} & {\bf Beschreibung} \\
neuper@42073:     10.02.2011 & 2:00 & Besprechung der Problemstellung \\
neuper@42073: \end{tabular}
neuper@42073: 
jan@42246: \section{Calculations}
jan@42251: \input{calulations}
jan@42246: 
neuper@42073: 
neuper@42073: \end{document}




