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@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@42235: 	\sisac-Projektteam des Instituts für Softwaretechnologie,\\Technische Universität Graz\\
jan@42235: 	\vspace{0.7cm}
jan@42235: 	\large{
jan@42235: 		Betreuer: Dr. Walther Neuper
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: 
neuper@42240: 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 \cite{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: 
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: 
neuper@42073: \bibliography{bib}
neuper@42073: 
neuper@42073: \clearpage
neuper@42073: 
neuper@42073: \appendix
neuper@42073: %\section*{Anhang}
neuper@42073: \section{Demobeispiel}\label{demo-code}
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@42246: \include{calulations}
jan@42246: 
neuper@42073: 
neuper@42073: \end{document}