\documentclass[a4paper, 12pt]{scrartcl}

 \usepackage[english,german]{babel} 

 \usepackage[T1]{fontenc}

 \usepackage[latin1]{inputenc}

 \usepackage{graphicx}

 \usepackage{endnotes}

 \usepackage{trfsigns}

 \usepackage{setspace}

 \usepackage{isabelle}

 \usepackage{isabellesym}

 \bibliographystyle{alpha}

 \def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}

 \def\sisac{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}

 \begin{document}

 \title{

 	\Large{

   	\bf Interactive Course Material for Signal Processing based on Isabelle/\isac\\~\\

   }

 	\sisac-Projektteam des Instituts für Softwaretechnologie,\\Technische Universität Graz\\

 	\vspace{0.7cm}

 	\large{

 		Betreuer: Dr. Walther Neuper

 	}

 }

 \author{Jan Simon Rocnik\\{\tt jan.rocnik@student.tugraz.at}}

 \date{\today}

 \maketitle

 \clearpage

 \tableofcontents

 \clearpage

 \section{Introduction}

 todo

 motivation from \textbf{practice of mathematics learning} ... STEOP

 \textbf{mathematics applied} in signal processing (SP)

 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}

 This thesis tries to \textbf{connect these two worlds} ... this trial is one of the first; others see related work

 \subsection{Mechanization of Mathematics}

 todo

 hughe theories of mathematics

 still a hugh gap between these theories and ``real applications'' e.g. in SP

 ? 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.

 CTP Isabelle ... survey of knowledge, links to knowledge

 \paragraph{\sisac}

 TODO

 adds an ``application'' axis (formal specifications of problems) and an ``algorithmic'' axis to the ``deductive'' axis of knowledge ... 3-dimensional universe of mathematics.

 \subsection{Goals of the Thesis}

 todo

 \subsection{Milestones for the Project}

 Die Planung des Projekts teilt sich in folgende Iterationen:

 \begin{enumerate}

 \item \textbf{Sammeln von Informationen über Themengebiete und deren Realisierbarkeit } (29.06. -- 27.07.)

 identify problems relevant for certain SP lectures

 estimate chances to realized them within the scope of this thesis

 order for implementing the problems negotiated with lecturers

 \item \textbf{1. Präsentation - Auswählen der realisierbaren Themengebiete} (27.07.)

 \item \textbf{Ausarbeiten der Aufgaben in \isac} (01.09. -- 11.11.)

 \item \textbf{Dokumentation der Aufgaben} (14.11. -- 02.12.)

 \item \textbf{Ausarbeitung in Latex, Bakkarbeit} (05.12. -- todo)

 \item \textbf{2. Präsentation - Abschluss der Arbeit} (todo)

 \end{enumerate}

 \subsection{Structure of the Thesis}

 todo

 \section{Mechanization of Mathematics for SP Problems}

 todo

 \subsection{Relevant Knowledge available in Isabelle}

 todo

 \paragraph{example FFT}, describe in detail !!!! 

 ? different meaning: FFT in Maple

 gap between what is available and what is required (@)!

 traditional notation ?

 \subsection{Relevant Knowledge available in \isac}

 todo

 specifications (``application axis'') and methods (``algorithmic axis'')

 partial fractions, cancellation of multivariate rational terms, ...

 \subsection{Survey: Available Knowledge and Selected Problems}

 todo

 estimate gap (@) for each problem (tables)

 conclusion: following order for implementing the problems ...

 \subsection{Formalization of missing knowledge in Isabelle}

 todo

 axiomatization ... where ... and

 \subsection{Notes on Problems with Traditional Notation}

 todo

 u[n] !!

 f x =  why not f(x) ?!?!

 ...

 \section{Implementation of Certain SP Problems}

 todo

 \subsection{Formal Specification of Problems}

 todo

 \subsection{Methods Solving the Problems}

 todo

 \subsection{Integration of Subproblems available in \isac}

 todo

 \subsection{Examples and Multimedia Content}

 todo

 \section{Related Work and Open Questions}

 todo

 See ``introduction'': This thesis tries to connect these two worlds ... this trial is one of the first; others see related work

 \section{Beschreibung der Meilensteine}\label{ms-desc}

 todo

 \section{Bericht zum Projektverlauf}

 todo

 \section{Abschliesende Bemerkungen}

 todo

 \clearpage

 \bibliography{bib}

 \clearpage

 \appendix

 %\section*{Anhang}

 \section{Demobeispiel}

 \input{./Inverse_Z-Transform/document/Inverse_Z_Transform.tex}

 \begin{verbatim}

 bsp

 \end{verbatim}

 \section{Stundenliste}

 \subsection*{Voraussetzungen zum Arbeitsbeginn schaffen}

 \begin{tabular}[t]{lll}

     {\bf Datum} & {\bf Stunden} & {\bf Beschreibung} \\

     10.02.2011 & 2:00 & Besprechung der Problemstellung \\

 \end{tabular}

 \section{Calculations}

 \input{calulations}

 \end{document}