\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}