1 \documentclass[a4paper, 12pt]{scrartcl}
3 \usepackage[english,german]{babel}
4 \usepackage[T1]{fontenc}
5 \usepackage[latin1]{inputenc}
12 \bibliographystyle{alpha}
14 \def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
15 \def\sisac{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
21 \bf Interactive Course Material for Signal Processing based on Isabelle/\isac\\~\\
23 \sisac-Projektteam des Instituts für Softwaretechnologie,\\Technische Universität Graz\\
26 Betreuer: Dr. Walther Neuper
29 \author{Jan Simon Rocnik\\{\tt jan.rocnik@student.tugraz.at}}
38 \section{Introduction}
42 motivation from \textbf{practice of mathematics learning} ... STEOP
44 \textbf{mathematics applied} in signal processing (SP)
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}
48 This thesis tries to \textbf{connect these two worlds} ... this trial is one of the first; others see related work
50 \subsection{Mechanization of Mathematics}
54 hughe theories of mathematics
56 still a hugh gap between these theories and ``real applications'' e.g. in SP
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.
60 CTP Isabelle ... survey of knowledge, links to knowledge
65 adds an ``application'' axis (formal specifications of problems) and an ``algorithmic'' axis to the ``deductive'' axis of knowledge ... 3-dimensional universe of mathematics.
67 \subsection{Goals of the Thesis}
71 \subsection{Milestones for the Project}
72 Die Planung des Projekts teilt sich in folgende Iterationen:
74 \item \textbf{Sammeln von Informationen über Themengebiete und deren Realisierbarkeit } (29.06. -- 27.07.)
75 identify problems relevant for certain SP lectures
77 estimate chances to realized them within the scope of this thesis
79 order for implementing the problems negotiated with lecturers
82 \item \textbf{1. Präsentation - Auswählen der realisierbaren Themengebiete} (27.07.)
83 \item \textbf{Ausarbeiten der Aufgaben in \isac} (01.09. -- 11.11.)
84 \item \textbf{Dokumentation der Aufgaben} (14.11. -- 02.12.)
85 \item \textbf{Ausarbeitung in Latex, Bakkarbeit} (05.12. -- todo)
86 \item \textbf{2. Präsentation - Abschluss der Arbeit} (todo)
89 \subsection{Structure of the Thesis}
93 \section{Mechanization of Mathematics for SP Problems}
96 \subsection{Relevant Knowledge available in Isabelle}
99 \paragraph{example FFT}, describe in detail !!!!
101 ? different meaning: FFT in Maple
103 gap between what is available and what is required (@)!
105 traditional notation ?
107 \subsection{Relevant Knowledge available in \isac}
110 specifications (``application axis'') and methods (``algorithmic axis'')
112 partial fractions, cancellation of multivariate rational terms, ...
114 \subsection{Survey: Available Knowledge and Selected Problems}
117 estimate gap (@) for each problem (tables)
119 conclusion: following order for implementing the problems ...
121 \subsection{Formalization of missing knowledge in Isabelle}
124 axiomatization ... where ... and
126 \subsection{Notes on Problems with Traditional Notation}
131 f x = why not f(x) ?!?!
135 \section{Implementation of Certain SP Problems}
138 \subsection{Formal Specification of Problems}
141 \subsection{Methods Solving the Problems}
144 \subsection{Integration of Subproblems available in \isac}
147 \subsection{Examples and Multimedia Content}
151 \section{Related Work and Open Questions}
154 See ``introduction'': This thesis tries to connect these two worlds ... this trial is one of the first; others see related work
158 \section{Beschreibung der Meilensteine}\label{ms-desc}
160 \section{Bericht zum Projektverlauf}
162 \section{Abschliesende Bemerkungen}
173 \section{Demobeispiel}\label{demo-code}
180 \section{Stundenliste}
182 \subsection*{Voraussetzungen zum Arbeitsbeginn schaffen}
183 \begin{tabular}[t]{lll}
184 {\bf Datum} & {\bf Stunden} & {\bf Beschreibung} \\
185 10.02.2011 & 2:00 & Besprechung der Problemstellung \\
188 \section{Calculations}
189 \include{calulations}