2 %handout, % prints handouts (=no animations, for printed version)
9 \usepackage{beamerthemedefault}
12 \definecolor{lgray}{RGB}{238,238,238}
14 \useoutertheme[subsection=false]{smoothbars}
15 \useinnertheme{circles}
17 \setbeamercolor{block title}{fg=black,bg=gray}
18 \setbeamercolor{block title alerted}{use=alerted text,fg=black,bg=alerted text.fg!75!bg}
19 \setbeamercolor{block title example}{use=example text,fg=black,bg=example text.fg!75!bg}
20 \setbeamercolor{block body}{parent=normal text,use=block title,bg=block title.bg!25!bg}
21 \setbeamercolor{block body alerted}{parent=normal text,use=block title alerted,bg=block title alerted.bg!25!bg}
22 \setbeamercolor{block body example}{parent=normal text,use=block title example,bg=block title example.bg!25!bg}
24 %activate hyperlinks at the end
25 %\usepackage{hyperref}
27 \usepackage[english]{babel}
28 \usepackage[utf8]{inputenc}
32 \definecolor{tug}{rgb}{0.96862,0.14509,0.27450}
34 \def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
35 \def\sisac{{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}}
37 \setbeamertemplate{headline}[text line]{
38 \begin{beamercolorbox}[wd=\paperwidth,ht=8ex,dp=4ex]{}
39 \insertnavigation{0.85\paperwidth}
40 \raisebox{-10pt}{\includegraphics[width=15mm]{tuglogo}}\vskip2pt
41 \hskip-1pt\rule{\paperwidth}{0.3pt}
45 \setbeamertemplate{navigation symbols}{}
47 \definecolor{gray}{rgb}{0.8,0.8,0.8}
48 \setbeamercolor{footline}{fg=black,bg=gray}
50 % Fusszeile mit Autor, Titel und Foliennummer / Gesamtfolienzahl
51 \setbeamertemplate{footline}[text line]{
53 \begin{beamercolorbox}[wd=\paperwidth]{footline}
54 \rule{\paperwidth}{0.3pt}
55 \colorbox{tug}{\rule{3pt}{0pt}\rule{0pt}{3pt}}
56 \textbf{\rule{0pt}{5pt}\insertshortauthor\hfill\insertshortinstitute\hfill%
57 \insertshorttitle\rule{1em}{0pt}}
58 \rule{\paperwidth}{0.3pt}
60 \begin{beamercolorbox}[wd=\paperwidth,ht=2ex,dp=2ex]{white}
64 %% Titelblatt-Einstellungen
65 \institute[IST, SPSC]{Institute for Software Technology\\Institute of Signal Processing and Speech Communication\\Graz University of Technology}
66 \title[ISAC for Signal Processing]{Interactive Course Material for\\ Signal Processing based on\\ Isabelle/\isac}
67 \subtitle{Baccalaureate Thesis}
71 % Subject and Keywords for PDF
72 \subject{Final presentation of Baccalaureate Thesis}
73 \keywords{Isac, Isabelle, ist, spsc, thesis, course material}
75 \titlegraphic{\includegraphics[width=20mm]{tuglogo}}
77 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
79 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
91 \tableofcontents[hideallsubsections %
93 ] % erzeugt Inhaltsverzeichnis
97 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
98 \section{Introduction}
99 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
101 \subsection{isabelle}
103 \frametitle{What is Isabelle?}
106 \item Generic Proof Assistant
107 \item Formula proofing in logical calculus
108 \item Developed in Cambridge, Muenchen and Paris
115 \frametitle{What is {\isac}?}
118 \item \textcolor{tug}{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal A}$}belle for~{}\textcolor{tug}{${\cal C}$}alculations
119 \item Interactive Course Material
121 \item Developed at Austrian Universities
126 \subsection{motivation}
128 \frametitle{Motivation - {\isac{}}'s~Potential}
130 \item Stepwise solving of engineering problems\\
131 {\small $\rightarrow$ \textcolor{tug}{Consistent Framework}}
132 \item Explaining underlying knowledge\\
133 {\small $\rightarrow$ \textcolor{tug}{Transparent Content, Access to Multimedia Content}}
134 \item Checking steps input by the student\\
135 {\small $\rightarrow$ \textcolor{tug}{Proof Situation}}
136 \item Assessing stepwise problem solving\\
137 {\small $\rightarrow$ \textcolor{tug}{One system for tutoring and assessment}}
142 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
143 \section{Thesis Definition}
144 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
147 \frametitle{Thesis Definition}
148 %---> Follow up thesis abstract! <---%
151 \item Creation of interactive course material\\
152 {\small Based on problems given by SPSC}
153 \item Content should be usable\ldots
155 \item in Signalprocessing Problem Classes
156 \item in \emph{STEOP}
158 \item Guideline for upcoming TP-Programmers.
159 \item Feedback of usability\\
160 {\small (TP-Programming-Language)}
167 \frametitle{Issues to Accomplish I}
170 \item What knowledge is mechanized in Isabelle?\\
171 {\small How about new?}
172 \item What problems are implemented in {\sisac{}}?\\
173 {\small How about new?}
174 \item What is the effort?
180 \frametitle{Issues to Accomplish II}
183 \item How look calculations like?\\
184 {\small Ansatzs, Subproblems?}
185 \item How are problems specified?\\
186 {\small Given, Pre-/Postcondition, Find?}
187 \item What is the contents of the interactive course material?\\
188 {\small Figures, Explanations,\ldots}
193 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
195 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
197 \subsection{Technical Survey}
199 \frametitle{Technical Survey I {\normalsize Mechanizing Knowledge}}
202 \item Not enough knowledge is mechanized\\
203 {\small Equation Solving, Integrals,\ldots}
204 \item Computer Mathematicians required!\\
205 {\small Mathematics: Equation solving, Engineer: Z-Transform}
206 \item RISC Linz, Mathematics TU Graz
212 \frametitle{Technical Survey II {\normalsize Notation Problems} }
215 \item Different brackets have different meanings\\
216 {\small $u[n] \neq u(n)$\ldots in Math; but also in the source code}
217 \item Simplification, tricks and beauty\\
218 {\small $X\cdot(a+b)+Y\cdot(c+d)=aX+bX+cY+dY$}\\
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)=$}\\
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)$} $}
225 \subsection{Demonstration}
227 \frametitle{Demonstration of {\isac}}
230 \item {\Large Development Environment} (Backend)
232 \item {\Large Math Assistant} (Frontend)
237 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
239 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
241 \subsection{Accomplished Work}
243 \frametitle{Accomplished Work}
245 \item Partial Fractions\\ {\small Theorems, Specification, Program}
246 \item Inverse Z-Transform with Partial Fractions\\ {\small Theorems, Specification, Program}
247 \item Isabelle Theory indicating issues\\ {\small Preparation for {\sisac{}}-developers}
251 \subsection{Partially Accomplished}
253 \frametitle{Partially Accomplished}
256 \item Guidelines for Upcoming TP-Programmers\\
257 {\small \textbf{Note:} Development environment and languages changes}
263 \subsection{Not Accomplished}
265 \frametitle{Not Accomplished}
268 \item Content of interactive course material\\
269 {\small Figures, Explanations,\ldots}
270 \item A sufficient count of implementations
271 \item No support of labs and lectures atm
272 \item No material for \emph{STEOP} atm
277 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
279 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
282 \frametitle{Conclusion}
285 \item TP-based language not ready
286 \item Programming guideline not yet sufficient
287 \item Hope for usability in enginieering studies
289 \item Hard to spend 200h on 1 programm
290 \item \isac{} pointed at my own error
295 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
297 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%