1 \documentclass[a4paper,12pt]{article} |
|
2 |
|
3 \usepackage[german]{babel} |
|
4 \usepackage[T1]{fontenc} |
|
5 \usepackage[latin1]{inputenc} |
|
6 |
|
7 \usepackage{graphicx} |
|
8 |
|
9 \bibliographystyle{alpha} |
|
10 |
|
11 \def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$} |
|
12 \def\sisac{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$} |
|
13 |
|
14 \begin{document} |
|
15 |
|
16 \title{ |
|
17 \Large{ |
|
18 \bf Interactive Course Material for Signal Processing based on Isabelle/\isac\\~\\ |
|
19 } |
|
20 \sisac-Projektteam des Instituts für Softwaretechnologie,\\Technische Universität Graz\\ |
|
21 \vspace{0.7cm} |
|
22 \large{ |
|
23 Betreuer: Dr. Walther Neuper |
|
24 } |
|
25 } |
|
26 \author{Jan Simon Rocnik\\{\tt jan.rocnik@student.tugraz.at}} |
|
27 |
|
28 \date{\today} |
|
29 \maketitle |
|
30 \clearpage |
|
31 \tableofcontents |
|
32 \clearpage |
|
33 |
|
34 |
|
35 \section{Introduction} |
|
36 |
|
37 todo |
|
38 |
|
39 motivation from \textbf{practice of mathematics learning} ... STEOP |
|
40 |
|
41 \textbf{mathematics applied} in signal processing (SP) |
|
42 |
|
43 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} |
|
44 |
|
45 This thesis tries to \textbf{connect these two worlds} ... this trial is one of the first; others see related work |
|
46 |
|
47 \subsection{Mechanization of Mathematics} |
|
48 |
|
49 todo |
|
50 |
|
51 hughe theories of mathematics |
|
52 |
|
53 still a hugh gap between these theories and ``real applications'' e.g. in SP |
|
54 |
|
55 ? 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. |
|
56 |
|
57 CTP Isabelle ... survey of knowledge, links to knowledge |
|
58 |
|
59 \paragraph{\sisac} |
|
60 TODO |
|
61 |
|
62 adds an ``application'' axis (formal specifications of problems) and an ``algorithmic'' axis to the ``deductive'' axis of knowledge ... 3-dimensional universe of mathematics. |
|
63 |
|
64 \subsection{Goals of the Thesis} |
|
65 |
|
66 todo |
|
67 |
|
68 \subsection{Milestones for the Project} |
|
69 Die Planung des Projekts teilt sich in folgende Iterationen: |
|
70 \begin{enumerate} |
|
71 \item \textbf{Sammeln von Informationen über Themengebiete und deren Realisierbarkeit } (29.06. -- 27.07.) |
|
72 identify problems relevant for certain SP lectures |
|
73 |
|
74 estimate chances to realized them within the scope of this thesis |
|
75 |
|
76 order for implementing the problems negotiated with lecturers |
|
77 |
|
78 |
|
79 \item \textbf{1. Präsentation - Auswählen der realisierbaren Themengebiete} (27.07.) |
|
80 \item \textbf{Ausarbeiten der Aufgaben in \isac} (01.09. -- 11.11.) |
|
81 \item \textbf{Dokumentation der Aufgaben} (14.11. -- 02.12.) |
|
82 \item \textbf{Ausarbeitung in Latex, Bakkarbeit} (05.12. -- todo) |
|
83 \item \textbf{2. Präsentation - Abschluss der Arbeit} (todo) |
|
84 \end{enumerate} |
|
85 |
|
86 \subsection{Structure of the Thesis} |
|
87 |
|
88 todo |
|
89 |
|
90 \section{Mechanization of Mathematics for SP Problems} |
|
91 todo |
|
92 |
|
93 \subsection{Relevant Knowledge available in Isabelle} |
|
94 todo |
|
95 |
|
96 \paragraph{example FFT}, describe in detail !!!! |
|
97 |
|
98 ? different meaning: FFT in Maple |
|
99 |
|
100 gap between what is available and what is required (@)! |
|
101 |
|
102 traditional notation ? |
|
103 |
|
104 \subsection{Relevant Knowledge available in \isac} |
|
105 todo |
|
106 |
|
107 specifications (``application axis'') and methods (``algorithmic axis'') |
|
108 |
|
109 partial fractions, cancellation of multivariate rational terms, ... |
|
110 |
|
111 \subsection{Survey: Available Knowledge and Selected Problems} |
|
112 todo |
|
113 |
|
114 estimate gap (@) for each problem (tables) |
|
115 |
|
116 conclusion: following order for implementing the problems ... |
|
117 |
|
118 \subsection{Formalization of missing knowledge in Isabelle} |
|
119 todo |
|
120 |
|
121 axiomatization ... where ... and |
|
122 |
|
123 \subsection{Notes on Problems with Traditional Notation} |
|
124 todo |
|
125 |
|
126 u[n] !! |
|
127 |
|
128 f x = why not f(x) ?!?! |
|
129 |
|
130 ... |
|
131 |
|
132 \section{Implementation of Certain SP Problems} |
|
133 todo |
|
134 |
|
135 \subsection{Formal Specification of Problems} |
|
136 todo |
|
137 |
|
138 \subsection{Methods Solving the Problems} |
|
139 todo |
|
140 |
|
141 \subsection{Integration of Subproblems available in \isac} |
|
142 todo |
|
143 |
|
144 \subsection{Examples and Multimedia Content} |
|
145 todo |
|
146 |
|
147 |
|
148 \section{Related Work and Open Questions} |
|
149 todo |
|
150 |
|
151 See ``introduction'': This thesis tries to connect these two worlds ... this trial is one of the first; others see related work |
|
152 |
|
153 |
|
154 |
|
155 \section{Beschreibung der Meilensteine}\label{ms-desc} |
|
156 todo |
|
157 \section{Bericht zum Projektverlauf} |
|
158 todo |
|
159 \section{Abschliesende Bemerkungen} |
|
160 todo |
|
161 |
|
162 \clearpage |
|
163 |
|
164 \bibliography{bib} |
|
165 |
|
166 \clearpage |
|
167 |
|
168 \appendix |
|
169 %\section*{Anhang} |
|
170 \section{Demobeispiel}\label{demo-code} |
|
171 \begin{verbatim} |
|
172 |
|
173 bsp |
|
174 |
|
175 \end{verbatim} |
|
176 |
|
177 \section{Stundenliste} |
|
178 |
|
179 \subsection*{Voraussetzungen zum Arbeitsbeginn schaffen} |
|
180 \begin{tabular}[t]{lll} |
|
181 {\bf Datum} & {\bf Stunden} & {\bf Beschreibung} \\ |
|
182 10.02.2011 & 2:00 & Besprechung der Problemstellung \\ |
|
183 \end{tabular} |
|
184 |
|
185 |
|
186 \end{document} |
|