1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/doc-src/isac/jrocnik/bakkarbeit_jrocnik.tex Tue Sep 06 15:57:25 2011 +0200
1.3 @@ -0,0 +1,186 @@
1.4 +\documentclass[a4paper,12pt]{article}
1.5 +
1.6 +\usepackage[german]{babel}
1.7 +\usepackage[T1]{fontenc}
1.8 +\usepackage[latin1]{inputenc}
1.9 +
1.10 +\usepackage{graphicx}
1.11 +
1.12 +\bibliographystyle{alpha}
1.13 +
1.14 +\def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
1.15 +\def\sisac{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
1.16 +
1.17 +\begin{document}
1.18 +
1.19 +\title{
1.20 + \Large{
1.21 + \bf Interactive Course Material for Signal Processing based on Isabelle/\isac\\~\\
1.22 + }
1.23 + \sisac-Projektteam des Instituts für Softwaretechnologie,\\Technische Universität Graz\\
1.24 + \vspace{0.7cm}
1.25 + \large{
1.26 + Betreuer: Dr. Walther Neuper
1.27 + }
1.28 +}
1.29 +\author{Jan Simon Rocnik\\{\tt jan.rocnik@student.tugraz.at}}
1.30 +
1.31 +\date{\today}
1.32 +\maketitle
1.33 +\clearpage
1.34 +\tableofcontents
1.35 +\clearpage
1.36 +
1.37 +
1.38 +\section{Introduction}
1.39 +
1.40 +todo
1.41 +
1.42 +motivation from \textbf{practice of mathematics learning} ... STEOP
1.43 +
1.44 +\textbf{mathematics applied} in signal processing (SP)
1.45 +
1.46 +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}
1.47 +
1.48 +This thesis tries to \textbf{connect these two worlds} ... this trial is one of the first; others see related work
1.49 +
1.50 +\subsection{Mechanization of Mathematics}
1.51 +
1.52 +todo
1.53 +
1.54 +hughe theories of mathematics
1.55 +
1.56 +still a hugh gap between these theories and ``real applications'' e.g. in SP
1.57 +
1.58 +? 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.
1.59 +
1.60 +CTP Isabelle ... survey of knowledge, links to knowledge
1.61 +
1.62 +\paragraph{\sisac}
1.63 +TODO
1.64 +
1.65 +adds an ``application'' axis (formal specifications of problems) and an ``algorithmic'' axis to the ``deductive'' axis of knowledge ... 3-dimensional universe of mathematics.
1.66 +
1.67 +\subsection{Goals of the Thesis}
1.68 +
1.69 +todo
1.70 +
1.71 +\subsection{Milestones for the Project}
1.72 +Die Planung des Projekts teilt sich in folgende Iterationen:
1.73 +\begin{enumerate}
1.74 +\item \textbf{Sammeln von Informationen über Themengebiete und deren Realisierbarkeit } (29.06. -- 27.07.)
1.75 +identify problems relevant for certain SP lectures
1.76 +
1.77 +estimate chances to realized them within the scope of this thesis
1.78 +
1.79 +order for implementing the problems negotiated with lecturers
1.80 +
1.81 +
1.82 +\item \textbf{1. Präsentation - Auswählen der realisierbaren Themengebiete} (27.07.)
1.83 +\item \textbf{Ausarbeiten der Aufgaben in \isac} (01.09. -- 11.11.)
1.84 +\item \textbf{Dokumentation der Aufgaben} (14.11. -- 02.12.)
1.85 +\item \textbf{Ausarbeitung in Latex, Bakkarbeit} (05.12. -- todo)
1.86 +\item \textbf{2. Präsentation - Abschluss der Arbeit} (todo)
1.87 +\end{enumerate}
1.88 +
1.89 +\subsection{Structure of the Thesis}
1.90 +
1.91 +todo
1.92 +
1.93 +\section{Mechanization of Mathematics for SP Problems}
1.94 +todo
1.95 +
1.96 +\subsection{Relevant Knowledge available in Isabelle}
1.97 +todo
1.98 +
1.99 +\paragraph{example FFT}, describe in detail !!!!
1.100 +
1.101 +? different meaning: FFT in Maple
1.102 +
1.103 +gap between what is available and what is required (@)!
1.104 +
1.105 +traditional notation ?
1.106 +
1.107 +\subsection{Relevant Knowledge available in \isac}
1.108 +todo
1.109 +
1.110 +specifications (``application axis'') and methods (``algorithmic axis'')
1.111 +
1.112 +partial fractions, cancellation of multivariate rational terms, ...
1.113 +
1.114 +\subsection{Survey: Available Knowledge and Selected Problems}
1.115 +todo
1.116 +
1.117 +estimate gap (@) for each problem (tables)
1.118 +
1.119 +conclusion: following order for implementing the problems ...
1.120 +
1.121 +\subsection{Formalization of missing knowledge in Isabelle}
1.122 +todo
1.123 +
1.124 +axiomatization ... where ... and
1.125 +
1.126 +\subsection{Notes on Problems with Traditional Notation}
1.127 +todo
1.128 +
1.129 +u[n] !!
1.130 +
1.131 +f x = why not f(x) ?!?!
1.132 +
1.133 +...
1.134 +
1.135 +\section{Implementation of Certain SP Problems}
1.136 +todo
1.137 +
1.138 +\subsection{Formal Specification of Problems}
1.139 +todo
1.140 +
1.141 +\subsection{Methods Solving the Problems}
1.142 +todo
1.143 +
1.144 +\subsection{Integration of Subproblems available in \isac}
1.145 +todo
1.146 +
1.147 +\subsection{Examples and Multimedia Content}
1.148 +todo
1.149 +
1.150 +
1.151 +\section{Related Work and Open Questions}
1.152 +todo
1.153 +
1.154 +See ``introduction'': This thesis tries to connect these two worlds ... this trial is one of the first; others see related work
1.155 +
1.156 +
1.157 +
1.158 +\section{Beschreibung der Meilensteine}\label{ms-desc}
1.159 +todo
1.160 +\section{Bericht zum Projektverlauf}
1.161 +todo
1.162 +\section{Abschliesende Bemerkungen}
1.163 +todo
1.164 +
1.165 +\clearpage
1.166 +
1.167 +\bibliography{bib}
1.168 +
1.169 +\clearpage
1.170 +
1.171 +\appendix
1.172 +%\section*{Anhang}
1.173 +\section{Demobeispiel}\label{demo-code}
1.174 +\begin{verbatim}
1.175 +
1.176 +bsp
1.177 +
1.178 +\end{verbatim}
1.179 +
1.180 +\section{Stundenliste}
1.181 +
1.182 +\subsection*{Voraussetzungen zum Arbeitsbeginn schaffen}
1.183 +\begin{tabular}[t]{lll}
1.184 + {\bf Datum} & {\bf Stunden} & {\bf Beschreibung} \\
1.185 + 10.02.2011 & 2:00 & Besprechung der Problemstellung \\
1.186 +\end{tabular}
1.187 +
1.188 +
1.189 +\end{document}