|
jan@42381
|
1 |
\documentclass[%
|
|
jan@42381
|
2 |
%handout, % prints handouts (=no animations, for printed version)
|
|
jan@42381
|
3 |
%mathserif
|
|
jan@42381
|
4 |
%xcolor=pst,
|
|
jan@42381
|
5 |
14pt
|
|
jan@42381
|
6 |
% fleqn
|
|
jan@42381
|
7 |
]{beamer}
|
|
jan@42381
|
8 |
|
|
jan@42381
|
9 |
\usepackage{beamerthemedefault}
|
|
jan@42381
|
10 |
|
|
jan@42420
|
11 |
\usepackage{color}
|
|
jan@42420
|
12 |
\definecolor{lgray}{RGB}{238,238,238}
|
|
jan@42420
|
13 |
|
|
jan@42381
|
14 |
\useoutertheme[subsection=false]{smoothbars}
|
|
jan@42381
|
15 |
\useinnertheme{circles}
|
|
jan@42381
|
16 |
|
|
jan@42381
|
17 |
\setbeamercolor{block title}{fg=black,bg=gray}
|
|
jan@42381
|
18 |
\setbeamercolor{block title alerted}{use=alerted text,fg=black,bg=alerted text.fg!75!bg}
|
|
jan@42381
|
19 |
\setbeamercolor{block title example}{use=example text,fg=black,bg=example text.fg!75!bg}
|
|
jan@42381
|
20 |
\setbeamercolor{block body}{parent=normal text,use=block title,bg=block title.bg!25!bg}
|
|
jan@42381
|
21 |
\setbeamercolor{block body alerted}{parent=normal text,use=block title alerted,bg=block title alerted.bg!25!bg}
|
|
jan@42381
|
22 |
\setbeamercolor{block body example}{parent=normal text,use=block title example,bg=block title example.bg!25!bg}
|
|
jan@42381
|
23 |
|
|
jan@42401
|
24 |
%activate hyperlinks at the end
|
|
jan@42381
|
25 |
%\usepackage{hyperref}
|
|
jan@42381
|
26 |
|
|
jan@42381
|
27 |
\usepackage[english]{babel}
|
|
jan@42381
|
28 |
\usepackage[utf8]{inputenc}
|
|
jan@42381
|
29 |
\usepackage{array}
|
|
jan@42381
|
30 |
\usepackage{setspace}
|
|
jan@42381
|
31 |
|
|
jan@42381
|
32 |
\definecolor{tug}{rgb}{0.96862,0.14509,0.27450}
|
|
jan@42381
|
33 |
|
|
jan@42381
|
34 |
\def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
|
|
jan@42381
|
35 |
\def\sisac{{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}}
|
|
jan@42381
|
36 |
|
|
jan@42381
|
37 |
\setbeamertemplate{headline}[text line]{
|
|
jan@42381
|
38 |
\begin{beamercolorbox}[wd=\paperwidth,ht=8ex,dp=4ex]{}
|
|
jan@42381
|
39 |
\insertnavigation{0.85\paperwidth}
|
|
jan@42381
|
40 |
\raisebox{-10pt}{\includegraphics[width=15mm]{tuglogo}}\vskip2pt
|
|
jan@42381
|
41 |
\hskip-1pt\rule{\paperwidth}{0.3pt}
|
|
jan@42381
|
42 |
\end{beamercolorbox}
|
|
jan@42381
|
43 |
}
|
|
jan@42381
|
44 |
|
|
jan@42381
|
45 |
\setbeamertemplate{navigation symbols}{}
|
|
jan@42381
|
46 |
|
|
jan@42381
|
47 |
\definecolor{gray}{rgb}{0.8,0.8,0.8}
|
|
jan@42381
|
48 |
\setbeamercolor{footline}{fg=black,bg=gray}
|
|
jan@42381
|
49 |
|
|
jan@42381
|
50 |
% Fusszeile mit Autor, Titel und Foliennummer / Gesamtfolienzahl
|
|
jan@42381
|
51 |
\setbeamertemplate{footline}[text line]{
|
|
jan@42381
|
52 |
\hskip-1pt
|
|
jan@42381
|
53 |
\begin{beamercolorbox}[wd=\paperwidth]{footline}
|
|
jan@42381
|
54 |
\rule{\paperwidth}{0.3pt}
|
|
jan@42381
|
55 |
\colorbox{tug}{\rule{3pt}{0pt}\rule{0pt}{3pt}}
|
|
jan@42381
|
56 |
\textbf{\rule{0pt}{5pt}\insertshortauthor\hfill\insertshortinstitute\hfill%
|
|
jan@42381
|
57 |
\insertshorttitle\rule{1em}{0pt}}
|
|
jan@42381
|
58 |
\rule{\paperwidth}{0.3pt}
|
|
jan@42381
|
59 |
\end{beamercolorbox}
|
|
jan@42381
|
60 |
\begin{beamercolorbox}[wd=\paperwidth,ht=2ex,dp=2ex]{white}
|
|
jan@42381
|
61 |
\end{beamercolorbox}
|
|
jan@42381
|
62 |
}%
|
|
jan@42381
|
63 |
|
|
jan@42381
|
64 |
%% Titelblatt-Einstellungen
|
|
jan@42381
|
65 |
\institute[IST, SPSC]{Institute for Software Technology\\Institute of Signal Processing and Speech Communication\\Graz University of Technology}
|
|
jan@42381
|
66 |
\title[ISAC for Signal Processing]{Interactive Course Material for\\ Signal Processing based on\\ Isabelle/\isac}
|
|
jan@42381
|
67 |
\subtitle{Baccalaureate Thesis}
|
|
jan@42381
|
68 |
\author{Jan Rocnik}
|
|
jan@42401
|
69 |
\date{\today}
|
|
jan@42381
|
70 |
|
|
jan@42381
|
71 |
% Subject and Keywords for PDF
|
|
jan@42418
|
72 |
\subject{Final presentation of Baccalaureate Thesis}
|
|
jan@42418
|
73 |
\keywords{Isac, Isabelle, ist, spsc, thesis, course material}
|
|
jan@42381
|
74 |
|
|
jan@42381
|
75 |
\titlegraphic{\includegraphics[width=20mm]{tuglogo}}
|
|
jan@42381
|
76 |
|
|
jan@42381
|
77 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
jan@42381
|
78 |
\begin{document}
|
|
jan@42381
|
79 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
jan@42381
|
80 |
|
|
jan@42381
|
81 |
\begin{frame}[plain]
|
|
jan@42381
|
82 |
\frametitle{}
|
|
jan@42381
|
83 |
\titlepage
|
|
jan@42381
|
84 |
\end{frame}
|
|
jan@42381
|
85 |
|
|
jan@42381
|
86 |
|
|
jan@42381
|
87 |
|
|
jan@42381
|
88 |
\begin{frame}
|
|
jan@42381
|
89 |
\frametitle{Contents}
|
|
jan@42401
|
90 |
\begin{spacing}{0.3}
|
|
jan@42381
|
91 |
\tableofcontents[hideallsubsections %
|
|
jan@42381
|
92 |
% ,pausesections
|
|
jan@42381
|
93 |
] % erzeugt Inhaltsverzeichnis
|
|
jan@42401
|
94 |
\end{spacing}
|
|
jan@42381
|
95 |
\end{frame}
|
|
jan@42381
|
96 |
|
|
jan@42381
|
97 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
jan@42381
|
98 |
\section{Introduction}
|
|
jan@42381
|
99 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
jan@42381
|
100 |
|
|
jan@42381
|
101 |
\subsection{isabelle}
|
|
jan@42381
|
102 |
\begin{frame}
|
|
jan@42418
|
103 |
\frametitle{What is Isabelle?}
|
|
jan@42381
|
104 |
\begin{spacing}{1.5}
|
|
jan@42402
|
105 |
\begin{itemize}
|
|
jan@42402
|
106 |
\item Generic Proof Assistant
|
|
jan@42418
|
107 |
\item Formula proofing in logical calculus
|
|
jan@42402
|
108 |
\item Developed in Cambridge, Muenchen and Paris
|
|
jan@42402
|
109 |
\end{itemize}
|
|
jan@42381
|
110 |
\end{spacing}
|
|
jan@42381
|
111 |
\end{frame}
|
|
jan@42381
|
112 |
|
|
jan@42381
|
113 |
\subsection{isac}
|
|
jan@42381
|
114 |
\begin{frame}
|
|
jan@42401
|
115 |
\frametitle{What is {\isac}?}
|
|
jan@42381
|
116 |
\begin{spacing}{1.5}
|
|
jan@42402
|
117 |
\begin{itemize}
|
|
jan@42402
|
118 |
\item \textcolor{tug}{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal A}$}belle for~{}\textcolor{tug}{${\cal C}$}alculations
|
|
jan@42418
|
119 |
\item Interactive Course Material
|
|
jan@42402
|
120 |
\item Learning Coach
|
|
jan@42420
|
121 |
\item Developed at Austrian Universities
|
|
jan@42402
|
122 |
\end{itemize}
|
|
jan@42381
|
123 |
\end{spacing}
|
|
jan@42381
|
124 |
\end{frame}
|
|
jan@42381
|
125 |
|
|
jan@42401
|
126 |
\subsection{motivation}
|
|
jan@42401
|
127 |
\begin{frame}
|
|
jan@42420
|
128 |
\frametitle{Motivation - {\isac{}}'s~Potential}
|
|
jan@42401
|
129 |
\begin{itemize}
|
|
jan@42420
|
130 |
\item Stepwise solving of engineering problems\\
|
|
jan@42402
|
131 |
{\small $\rightarrow$ \textcolor{tug}{Consistent Framework}}
|
|
jan@42401
|
132 |
\item Explaining underlying knowledge\\
|
|
jan@42402
|
133 |
{\small $\rightarrow$ \textcolor{tug}{Transparent Content, Access to Multimedia Content}}
|
|
jan@42402
|
134 |
\item Checking steps input by the student\\
|
|
jan@42402
|
135 |
{\small $\rightarrow$ \textcolor{tug}{Proof Situation}}
|
|
jan@42402
|
136 |
\item Assessing stepwise problem solving\\
|
|
jan@42402
|
137 |
{\small $\rightarrow$ \textcolor{tug}{One system for tutoring and assessment}}
|
|
jan@42401
|
138 |
\end{itemize}
|
|
jan@42401
|
139 |
\end{frame}
|
|
jan@42401
|
140 |
|
|
jan@42381
|
141 |
|
|
jan@42381
|
142 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
jan@42381
|
143 |
\section{Thesis Definition}
|
|
jan@42381
|
144 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
jan@42381
|
145 |
|
|
jan@42381
|
146 |
\begin{frame}
|
|
jan@42401
|
147 |
\frametitle{Thesis Definition}
|
|
jan@42401
|
148 |
%---> Follow up thesis abstract! <---%
|
|
jan@42402
|
149 |
\begin{spacing}{1.2}
|
|
jan@42402
|
150 |
\begin{itemize}
|
|
jan@42402
|
151 |
\item Creation of interactive course material\\
|
|
jan@42420
|
152 |
{\small Based on problems given by SPSC}
|
|
jan@42402
|
153 |
\item Content should be usable\ldots
|
|
jan@42402
|
154 |
\begin{itemize}
|
|
jan@42420
|
155 |
\item in Signalprocessing Problem Classes
|
|
jan@42420
|
156 |
\item in \emph{STEOP}
|
|
jan@42402
|
157 |
\end{itemize}
|
|
jan@42402
|
158 |
\item Guideline for upcoming TP-Programmers.
|
|
jan@42402
|
159 |
\item Feedback of usability\\
|
|
jan@42402
|
160 |
{\small (TP-Programming-Language)}
|
|
jan@42402
|
161 |
\end{itemize}
|
|
jan@42402
|
162 |
\end{spacing}
|
|
jan@42381
|
163 |
\end{frame}
|
|
jan@42381
|
164 |
|
|
jan@42381
|
165 |
\subsection{issues}
|
|
jan@42381
|
166 |
\begin{frame}
|
|
jan@42401
|
167 |
\frametitle{Issues to Accomplish I}
|
|
jan@42402
|
168 |
\begin{spacing}{1.4}
|
|
jan@42402
|
169 |
\begin{itemize}
|
|
jan@42418
|
170 |
\item What knowledge is mechanized in Isabelle?\\
|
|
jan@42402
|
171 |
{\small How about new?}
|
|
jan@42402
|
172 |
\item What problems are implemented in {\sisac{}}?\\
|
|
jan@42402
|
173 |
{\small How about new?}
|
|
jan@42402
|
174 |
\item What is the effort?
|
|
jan@42402
|
175 |
\end{itemize}
|
|
jan@42402
|
176 |
\end{spacing}
|
|
jan@42401
|
177 |
\end{frame}
|
|
jan@42401
|
178 |
|
|
jan@42401
|
179 |
\begin{frame}
|
|
jan@42401
|
180 |
\frametitle{Issues to Accomplish II}
|
|
jan@42401
|
181 |
\begin{spacing}{1.4}
|
|
jan@42381
|
182 |
\begin{itemize}
|
|
jan@42402
|
183 |
\item How look calculations like?\\
|
|
jan@42401
|
184 |
{\small Ansatzs, Subproblems?}
|
|
jan@42402
|
185 |
\item How are problems specified?\\
|
|
jan@42401
|
186 |
{\small Given, Pre-/Postcondition, Find?}
|
|
jan@42418
|
187 |
\item What is the contents of the interactive course material?\\
|
|
jan@42418
|
188 |
{\small Figures, Explanations,\ldots}
|
|
jan@42381
|
189 |
\end{itemize}
|
|
jan@42401
|
190 |
\end{spacing}
|
|
jan@42381
|
191 |
\end{frame}
|
|
jan@42381
|
192 |
|
|
jan@42381
|
193 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
jan@42402
|
194 |
\section{Details}
|
|
jan@42381
|
195 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
jan@42381
|
196 |
|
|
jan@42418
|
197 |
\subsection{Technical Survey}
|
|
jan@42402
|
198 |
\begin{frame}
|
|
jan@42418
|
199 |
\frametitle{Technical Survey I {\normalsize Mechanizing Knowledge}}
|
|
jan@42402
|
200 |
\begin{spacing}{1.5}
|
|
jan@42402
|
201 |
\begin{itemize}
|
|
jan@42402
|
202 |
\item Not enough knowledge is mechanized\\
|
|
jan@42402
|
203 |
{\small Equation Solving, Integrals,\ldots}
|
|
jan@42420
|
204 |
\item Computer Mathematicians required!\\
|
|
jan@42420
|
205 |
{\small Mathematics: Equation solving, Engineer: Z-Transform}
|
|
jan@42420
|
206 |
\item RISC Linz, Mathematics TU Graz
|
|
jan@42402
|
207 |
\end{itemize}
|
|
jan@42402
|
208 |
\end{spacing}
|
|
jan@42402
|
209 |
\end{frame}
|
|
jan@42402
|
210 |
|
|
jan@42402
|
211 |
\begin{frame}
|
|
jan@42418
|
212 |
\frametitle{Technical Survey II {\normalsize Notation Problems} }
|
|
jan@42402
|
213 |
\begin{spacing}{1.5}
|
|
jan@42402
|
214 |
\begin{itemize}
|
|
jan@42402
|
215 |
\item Different brackets have different meanings\\
|
|
jan@42418
|
216 |
{\small $u[n] \neq u(n)$\ldots in Math; but also in the source code}
|
|
jan@42420
|
217 |
\item Simplification, tricks and beauty\\
|
|
jan@42420
|
218 |
{\small $X\cdot(a+b)+Y\cdot(c+d)=aX+bX+cY+dY$}\\
|
|
jan@42420
|
219 |
{\small $\frac{1}{j\omega}\cdot\left(e^{-j\omega}-e^{j3\omega}\right)=\frac{1}{j\omega}\cdot e^{-j2\omega}\cdot\left(e^{j\omega}-e^{-j\omega}\right)=$}\\
|
|
jan@42420
|
220 |
{\small $=\frac{1}{\omega}\, e^{-j2\omega}\cdot\colorbox{lgray}{$\frac{1}{j}\,\left(e^{j\omega}-e^{-j\omega}\right)$}=\frac{1}{\omega}\,e^{-j2\omega}\cdot\colorbox{lgray}{$2\, sin(\omega)$} $}
|
|
jan@42402
|
221 |
\end{itemize}
|
|
jan@42402
|
222 |
\end{spacing}
|
|
jan@42402
|
223 |
\end{frame}
|
|
jan@42402
|
224 |
|
|
jan@42402
|
225 |
\subsection{Demonstration}
|
|
jan@42381
|
226 |
\begin{frame}
|
|
jan@42401
|
227 |
\frametitle{Demonstration of {\isac}}
|
|
jan@42381
|
228 |
\begin{spacing}{1.5}
|
|
jan@42402
|
229 |
\begin{itemize}
|
|
jan@42418
|
230 |
\item {\Large Development Environment} (Backend)
|
|
jan@42402
|
231 |
\vspace{15mm}
|
|
jan@42402
|
232 |
\item {\Large Math Assistant} (Frontend)
|
|
jan@42402
|
233 |
\end{itemize}
|
|
jan@42381
|
234 |
\end{spacing}
|
|
jan@42381
|
235 |
\end{frame}
|
|
jan@42381
|
236 |
|
|
jan@42381
|
237 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
jan@42381
|
238 |
\section{Summary}
|
|
jan@42381
|
239 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
jan@42381
|
240 |
|
|
jan@42401
|
241 |
\subsection{Accomplished Work}
|
|
jan@42381
|
242 |
\begin{frame}
|
|
jan@42401
|
243 |
\frametitle{Accomplished Work}
|
|
jan@42381
|
244 |
\begin{itemize}
|
|
jan@42401
|
245 |
\item Partial Fractions\\ {\small Theorems, Specification, Program}
|
|
jan@42401
|
246 |
\item Inverse Z-Transform with Partial Fractions\\ {\small Theorems, Specification, Program}
|
|
jan@42418
|
247 |
\item Isabelle Theory indicating issues\\ {\small Preparation for {\sisac{}}-developers}
|
|
jan@42381
|
248 |
\end{itemize}
|
|
jan@42381
|
249 |
\end{frame}
|
|
jan@42381
|
250 |
|
|
jan@42381
|
251 |
\subsection{Partially Accomplished}
|
|
jan@42381
|
252 |
\begin{frame}
|
|
jan@42381
|
253 |
\frametitle{Partially Accomplished}
|
|
jan@42401
|
254 |
\begin{spacing}{1.4}
|
|
jan@42402
|
255 |
\begin{itemize}
|
|
jan@42402
|
256 |
\item Guidelines for Upcoming TP-Programmers\\
|
|
jan@42418
|
257 |
{\small \textbf{Note:} Development environment and languages changes}
|
|
jan@42402
|
258 |
\item Examples
|
|
jan@42402
|
259 |
\end{itemize}
|
|
jan@42401
|
260 |
\end{spacing}
|
|
jan@42381
|
261 |
\end{frame}
|
|
jan@42381
|
262 |
|
|
jan@42381
|
263 |
\subsection{Not Accomplished}
|
|
jan@42381
|
264 |
\begin{frame}
|
|
jan@42381
|
265 |
\frametitle{Not Accomplished}
|
|
jan@42401
|
266 |
\begin{spacing}{1.2}
|
|
jan@42402
|
267 |
\begin{itemize}
|
|
jan@42418
|
268 |
\item Content of interactive course material\\
|
|
jan@42418
|
269 |
{\small Figures, Explanations,\ldots}
|
|
jan@42402
|
270 |
\item A sufficient count of implementations
|
|
jan@42402
|
271 |
\item No support of labs and lectures atm
|
|
jan@42402
|
272 |
\item No material for \emph{STEOP} atm
|
|
jan@42402
|
273 |
\end{itemize}
|
|
jan@42401
|
274 |
\end{spacing}
|
|
jan@42381
|
275 |
\end{frame}
|
|
jan@42381
|
276 |
|
|
jan@42381
|
277 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
jan@42381
|
278 |
\section{Conclusion}
|
|
jan@42381
|
279 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
jan@42381
|
280 |
|
|
jan@42381
|
281 |
\begin{frame}
|
|
jan@42418
|
282 |
\frametitle{Conclusion}
|
|
jan@42401
|
283 |
\begin{spacing}{1.2}
|
|
jan@42402
|
284 |
\begin{itemize}
|
|
jan@42420
|
285 |
\item TP-based language not ready
|
|
jan@42420
|
286 |
\item Programming guideline not yet sufficient
|
|
jan@42420
|
287 |
\item Hope for usability in enginieering studies
|
|
jan@42402
|
288 |
\vspace{5mm}
|
|
jan@42420
|
289 |
\item Hard to spend 200h on 1 programm
|
|
jan@42420
|
290 |
\item \isac{} pointed at my own error
|
|
jan@42402
|
291 |
\end{itemize}
|
|
jan@42401
|
292 |
\end{spacing}
|
|
jan@42381
|
293 |
\end{frame}
|
|
jan@42381
|
294 |
|
|
jan@42381
|
295 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
jan@42381
|
296 |
\end{document}
|
|
jan@42381
|
297 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
jan@42381
|
298 |
|
|
jan@42381
|
299 |
%% EOF |