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}