1.1 --- a/doc-src/isac/jrocnik/vorlage-bakkarbeit.tex Mon Sep 05 14:43:38 2011 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,186 +0,0 @@
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}