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