|
1 \documentclass[% |
|
2 %handout, % prints handouts (=no animations, for printed version) |
|
3 %mathserif |
|
4 %xcolor=pst, |
|
5 14pt |
|
6 % fleqn |
|
7 ]{beamer} |
|
8 |
|
9 \usepackage{beamerthemedefault} |
|
10 |
|
11 \usepackage{color} |
|
12 \definecolor{lgray}{RGB}{238,238,238} |
|
13 |
|
14 \useoutertheme[subsection=false]{smoothbars} |
|
15 \useinnertheme{circles} |
|
16 |
|
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} |
|
23 |
|
24 %activate hyperlinks at the end |
|
25 %\usepackage{hyperref} |
|
26 |
|
27 \usepackage[english]{babel} |
|
28 \usepackage[utf8]{inputenc} |
|
29 \usepackage{array} |
|
30 \usepackage{setspace} |
|
31 |
|
32 \definecolor{tug}{rgb}{0.96862,0.14509,0.27450} |
|
33 |
|
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}$}} |
|
36 |
|
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} |
|
42 \end{beamercolorbox} |
|
43 } |
|
44 |
|
45 \setbeamertemplate{navigation symbols}{} |
|
46 |
|
47 \definecolor{gray}{rgb}{0.8,0.8,0.8} |
|
48 \setbeamercolor{footline}{fg=black,bg=gray} |
|
49 |
|
50 % Fusszeile mit Autor, Titel und Foliennummer / Gesamtfolienzahl |
|
51 \setbeamertemplate{footline}[text line]{ |
|
52 \hskip-1pt |
|
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} |
|
59 \end{beamercolorbox} |
|
60 \begin{beamercolorbox}[wd=\paperwidth,ht=2ex,dp=2ex]{white} |
|
61 \end{beamercolorbox} |
|
62 }% |
|
63 |
|
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} |
|
68 \author{Jan Rocnik} |
|
69 \date{\today} |
|
70 |
|
71 % Subject and Keywords for PDF |
|
72 \subject{Final presentation of Baccalaureate Thesis} |
|
73 \keywords{Isac, Isabelle, ist, spsc, thesis, course material} |
|
74 |
|
75 \titlegraphic{\includegraphics[width=20mm]{tuglogo}} |
|
76 |
|
77 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
78 \begin{document} |
|
79 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
80 |
|
81 \begin{frame}[plain] |
|
82 \frametitle{} |
|
83 \titlepage |
|
84 \end{frame} |
|
85 |
|
86 |
|
87 |
|
88 \begin{frame} |
|
89 \frametitle{Contents} |
|
90 \begin{spacing}{0.3} |
|
91 \tableofcontents[hideallsubsections % |
|
92 % ,pausesections |
|
93 ] % erzeugt Inhaltsverzeichnis |
|
94 \end{spacing} |
|
95 \end{frame} |
|
96 |
|
97 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
98 \section{Introduction} |
|
99 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
100 |
|
101 \subsection{isabelle} |
|
102 \begin{frame} |
|
103 \frametitle{What is Isabelle?} |
|
104 \begin{spacing}{1.5} |
|
105 \begin{itemize} |
|
106 \item Generic Proof Assistant |
|
107 \item Formula proofing in logical calculus |
|
108 \item Developed in Cambridge, Muenchen and Paris |
|
109 \end{itemize} |
|
110 \end{spacing} |
|
111 \end{frame} |
|
112 |
|
113 \subsection{isac} |
|
114 \begin{frame} |
|
115 \frametitle{What is {\isac}?} |
|
116 \begin{spacing}{1.5} |
|
117 \begin{itemize} |
|
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 |
|
120 \item Learning Coach |
|
121 \item Developed at Austrian Universities |
|
122 \end{itemize} |
|
123 \end{spacing} |
|
124 \end{frame} |
|
125 |
|
126 \subsection{motivation} |
|
127 \begin{frame} |
|
128 \frametitle{Motivation - {\isac{}}'s~Potential} |
|
129 \begin{itemize} |
|
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}} |
|
138 \end{itemize} |
|
139 \end{frame} |
|
140 |
|
141 |
|
142 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
143 \section{Thesis Definition} |
|
144 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
145 |
|
146 \begin{frame} |
|
147 \frametitle{Thesis Definition} |
|
148 %---> Follow up thesis abstract! <---% |
|
149 \begin{spacing}{1.2} |
|
150 \begin{itemize} |
|
151 \item Creation of interactive course material\\ |
|
152 {\small Based on problems given by SPSC} |
|
153 \item Content should be usable\ldots |
|
154 \begin{itemize} |
|
155 \item in Signalprocessing Problem Classes |
|
156 \item in \emph{STEOP} |
|
157 \end{itemize} |
|
158 \item Guideline for upcoming TP-Programmers. |
|
159 \item Feedback of usability\\ |
|
160 {\small (TP-Programming-Language)} |
|
161 \end{itemize} |
|
162 \end{spacing} |
|
163 \end{frame} |
|
164 |
|
165 \subsection{issues} |
|
166 \begin{frame} |
|
167 \frametitle{Issues to Accomplish I} |
|
168 \begin{spacing}{1.4} |
|
169 \begin{itemize} |
|
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? |
|
175 \end{itemize} |
|
176 \end{spacing} |
|
177 \end{frame} |
|
178 |
|
179 \begin{frame} |
|
180 \frametitle{Issues to Accomplish II} |
|
181 \begin{spacing}{1.4} |
|
182 \begin{itemize} |
|
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} |
|
189 \end{itemize} |
|
190 \end{spacing} |
|
191 \end{frame} |
|
192 |
|
193 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
194 \section{Details} |
|
195 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
196 |
|
197 \subsection{Technical Survey} |
|
198 \begin{frame} |
|
199 \frametitle{Technical Survey I {\normalsize Mechanizing Knowledge}} |
|
200 \begin{spacing}{1.5} |
|
201 \begin{itemize} |
|
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 |
|
207 \end{itemize} |
|
208 \end{spacing} |
|
209 \end{frame} |
|
210 |
|
211 \begin{frame} |
|
212 \frametitle{Technical Survey II {\normalsize Notation Problems} } |
|
213 \begin{spacing}{1.5} |
|
214 \begin{itemize} |
|
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)$} $} |
|
221 \end{itemize} |
|
222 \end{spacing} |
|
223 \end{frame} |
|
224 |
|
225 \subsection{Demonstration} |
|
226 \begin{frame} |
|
227 \frametitle{Demonstration of {\isac}} |
|
228 \begin{spacing}{1.5} |
|
229 \begin{itemize} |
|
230 \item {\Large Development Environment} (Backend) |
|
231 \vspace{15mm} |
|
232 \item {\Large Math Assistant} (Frontend) |
|
233 \end{itemize} |
|
234 \end{spacing} |
|
235 \end{frame} |
|
236 |
|
237 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
238 \section{Summary} |
|
239 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
240 |
|
241 \subsection{Accomplished Work} |
|
242 \begin{frame} |
|
243 \frametitle{Accomplished Work} |
|
244 \begin{itemize} |
|
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} |
|
248 \end{itemize} |
|
249 \end{frame} |
|
250 |
|
251 \subsection{Partially Accomplished} |
|
252 \begin{frame} |
|
253 \frametitle{Partially Accomplished} |
|
254 \begin{spacing}{1.4} |
|
255 \begin{itemize} |
|
256 \item Guidelines for Upcoming TP-Programmers\\ |
|
257 {\small \textbf{Note:} Development environment and languages changes} |
|
258 \item Examples |
|
259 \end{itemize} |
|
260 \end{spacing} |
|
261 \end{frame} |
|
262 |
|
263 \subsection{Not Accomplished} |
|
264 \begin{frame} |
|
265 \frametitle{Not Accomplished} |
|
266 \begin{spacing}{1.2} |
|
267 \begin{itemize} |
|
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 |
|
273 \end{itemize} |
|
274 \end{spacing} |
|
275 \end{frame} |
|
276 |
|
277 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
278 \section{Conclusion} |
|
279 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
280 |
|
281 \begin{frame} |
|
282 \frametitle{Conclusion} |
|
283 \begin{spacing}{1.2} |
|
284 \begin{itemize} |
|
285 \item TP-based language not ready |
|
286 \item Programming guideline not yet sufficient |
|
287 \item Hope for usability in enginieering studies |
|
288 \vspace{5mm} |
|
289 \item Hard to spend 200h on 1 programm |
|
290 \item \isac{} pointed at my own error |
|
291 \end{itemize} |
|
292 \end{spacing} |
|
293 \end{frame} |
|
294 |
|
295 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
296 \end{document} |
|
297 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
298 |
|
299 %% EOF |