1.1 --- a/doc-src/isac/jrocnik/vorlage-bakkarbeit.tex	Fri Sep 02 08:27:19 2011 +0200
     1.2 +++ b/doc-src/isac/jrocnik/vorlage-bakkarbeit.tex	Fri Sep 02 10:09:45 2011 +0200
     1.3 @@ -32,18 +32,50 @@
     1.4  \clearpage
     1.5  
     1.6  
     1.7 -\section{Zur Aufgabenstellung}
     1.8 +\section{Introduction}
     1.9  
    1.10  todo
    1.11  
    1.12 -\section{Planung des Projektes}
    1.13 +motivation from \textbf{practice of mathematics learning} ... STEOP
    1.14 +
    1.15 +\textbf{mathematics applied} in signal processing (SP)
    1.16 +
    1.17 +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.18 +
    1.19 +This thesis tries to \textbf{connect these two worlds} ... this trial is one of the first; others see related work
    1.20 +
    1.21 +\subsection{Mechanization of Mathematics}
    1.22  
    1.23  todo
    1.24  
    1.25 -\subsection{Zeitplanung des Projekt}
    1.26 +hughe theories of mathematics
    1.27 +
    1.28 +still a hugh gap between these theories and ``real applications'' e.g. in SP
    1.29 +
    1.30 +? 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.31 +
    1.32 +CTP Isabelle ... survey of knowledge, links to knowledge
    1.33 +
    1.34 +\paragraph{\sisac}
    1.35 +TODO
    1.36 +
    1.37 +adds an ``application'' axis (formal specifications of problems) and an ``algorithmic'' axis to the ``deductive'' axis of knowledge ... 3-dimensional universe of mathematics.
    1.38 +
    1.39 +\subsection{Goals of the Thesis}
    1.40 +
    1.41 +todo
    1.42 +
    1.43 +\subsection{Milestones for the Project}
    1.44  Die Planung des Projekts teilt sich in folgende Iterationen:
    1.45  \begin{enumerate}
    1.46 -\item \textbf{Sammeln von Informationen über Themengebite und deren Realisierbarkeit } (29.06. -- 27.07.)
    1.47 +\item \textbf{Sammeln von Informationen über Themengebiete und deren Realisierbarkeit } (29.06. -- 27.07.)
    1.48 +identify problems relevant for certain SP lectures
    1.49 +
    1.50 +estimate chances to realized them within the scope of this thesis
    1.51 +
    1.52 +order for implementing the problems negotiated with lecturers
    1.53 +
    1.54 +
    1.55  \item \textbf{1. Präsentation - Auswählen der realisierbaren Themengebiete} (27.07.)
    1.56  \item \textbf{Ausarbeiten der Aufgaben in \isac} (01.09. -- 11.11.)
    1.57  \item \textbf{Dokumentation der Aufgaben} (14.11. -- 02.12.)
    1.58 @@ -51,8 +83,75 @@
    1.59  \item \textbf{2. Präsentation - Abschluss der Arbeit} (todo)
    1.60  \end{enumerate}
    1.61  
    1.62 -\section{Konzepte und Lösungen}
    1.63 +\subsection{Structure of the Thesis}
    1.64 +
    1.65  todo
    1.66 +
    1.67 +\section{Mechanization of Mathematics for SP Problems}
    1.68 +todo
    1.69 +
    1.70 +\subsection{Relevant Knowledge available in Isabelle}
    1.71 +todo
    1.72 +
    1.73 +\paragraph{example FFT}, describe in detail !!!! 
    1.74 +
    1.75 +? different meaning: FFT in Maple
    1.76 +
    1.77 +gap between what is available and what is required (@)!
    1.78 +
    1.79 +traditional notation ?
    1.80 +
    1.81 +\subsection{Relevant Knowledge available in \isac}
    1.82 +todo
    1.83 +
    1.84 +specifications (``application axis'') and methods (``algorithmic axis'')
    1.85 +
    1.86 +partial fractions, cancellation of multivariate rational terms, ...
    1.87 +
    1.88 +\subsection{Survey: Available Knowledge and Selected Problems}
    1.89 +todo
    1.90 +
    1.91 +estimate gap (@) for each problem (tables)
    1.92 +
    1.93 +conclusion: following order for implementing the problems ...
    1.94 +
    1.95 +\subsection{Formalization of missing knowledge in Isabelle}
    1.96 +todo
    1.97 +
    1.98 +axiomatization ... where ... and
    1.99 +
   1.100 +\subsection{Notes on Problems with Traditional Notation}
   1.101 +todo
   1.102 +
   1.103 +u[n] !!
   1.104 +
   1.105 +f x =  why not f(x) ?!?!
   1.106 +
   1.107 +...
   1.108 +
   1.109 +\section{Implementation of Certain SP Problems}
   1.110 +todo
   1.111 +
   1.112 +\subsection{Formal Specification of Problems}
   1.113 +todo
   1.114 +
   1.115 +\subsection{Methods Solving the Problems}
   1.116 +todo
   1.117 +
   1.118 +\subsection{Integration of Subproblems available in \isac}
   1.119 +todo
   1.120 +
   1.121 +\subsection{Examples and Multimedia Content}
   1.122 +todo
   1.123 +
   1.124 +
   1.125 +\section{Related Work and Open Questions}
   1.126 +todo
   1.127 +
   1.128 +See ``introduction'': This thesis tries to connect these two worlds ... this trial is one of the first; others see related work
   1.129 +
   1.130 +
   1.131 +
   1.132  \section{Beschreibung der Meilensteine}\label{ms-desc}
   1.133  todo
   1.134  \section{Bericht zum Projektverlauf}