|
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 \usepackage{url} |
|
32 |
|
33 \definecolor{tug}{rgb}{0.96862,0.14509,0.27450} |
|
34 |
|
35 \def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$} |
|
36 \def\sisac{{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}} |
|
37 |
|
38 \setbeamertemplate{headline}[text line]{ |
|
39 \begin{beamercolorbox}[wd=\paperwidth,ht=8ex,dp=4ex]{} |
|
40 \insertnavigation{0.85\paperwidth} |
|
41 \raisebox{-10pt}{\includegraphics[width=15mm]{tuglogo}}\vskip2pt |
|
42 \hskip-1pt\rule{\paperwidth}{0.3pt} |
|
43 \end{beamercolorbox} |
|
44 } |
|
45 |
|
46 \setbeamertemplate{navigation symbols}{} |
|
47 |
|
48 \definecolor{gray}{rgb}{0.8,0.8,0.8} |
|
49 \setbeamercolor{footline}{fg=black,bg=gray} |
|
50 |
|
51 % Fusszeile mit Autor, Titel und Foliennummer / Gesamtfolienzahl |
|
52 \setbeamertemplate{footline}[text line]{ |
|
53 \hskip-1pt |
|
54 \begin{beamercolorbox}[wd=\paperwidth]{footline} |
|
55 \rule{\paperwidth}{0.3pt} |
|
56 \colorbox{tug}{\rule{3pt}{0pt}\rule{0pt}{3pt}} |
|
57 \textbf{\rule{0pt}{5pt}\insertshortauthor\hfill\insertshortinstitute\hfill% |
|
58 \insertshorttitle\rule{1em}{0pt}} |
|
59 \rule{\paperwidth}{0.3pt} |
|
60 \end{beamercolorbox} |
|
61 \begin{beamercolorbox}[wd=\paperwidth,ht=2ex,dp=2ex]{white} |
|
62 \end{beamercolorbox} |
|
63 }% |
|
64 |
|
65 %% Titelblatt-Einstellungen |
|
66 \institute[IST]{Institute for Software Technology\\Graz University of Technology} |
|
67 \title[ISAC for Signal Processing]{Interactive Course Material by TP-based Programming} |
|
68 \subtitle{A Case Study} |
|
69 \author{Jan Ro\v{c}nik} |
|
70 \date{24. June 2012} |
|
71 |
|
72 % Subject and Keywords for PDF |
|
73 \subject{CADGME Presentation} |
|
74 \keywords{interactive course material, signal processing, z transform, TP-based programming |
|
75 language, Lucas-Interpreter, Theorem Proving} |
|
76 |
|
77 \titlegraphic{\includegraphics[width=20mm]{tuglogo}} |
|
78 |
|
79 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
80 \begin{document} |
|
81 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
82 |
|
83 \begin{frame}[plain] |
|
84 \frametitle{} |
|
85 \titlepage |
|
86 \end{frame} |
|
87 |
|
88 |
|
89 |
|
90 %\begin{frame} |
|
91 % \frametitle{Contents} |
|
92 % \begin{spacing}{0.3} |
|
93 % \tableofcontents[hideallsubsections % |
|
94 % % ,pausesections |
|
95 % ] % erzeugt Inhaltsverzeichnis |
|
96 % \end{spacing} |
|
97 %\end{frame} |
|
98 |
|
99 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
100 \section{Introduction} |
|
101 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
102 |
|
103 \subsection{isabelle} |
|
104 \begin{frame} |
|
105 \frametitle{What is Isabelle?} |
|
106 \begin{spacing}{1.5} |
|
107 \begin{itemize} |
|
108 \item Generic Proof Assistant |
|
109 \item Formula proofing in logical calculus |
|
110 \item Developed in Cambridge, Muenchen and Paris |
|
111 \end{itemize} |
|
112 \end{spacing} |
|
113 \end{frame} |
|
114 |
|
115 \subsection{isac} |
|
116 \begin{frame} |
|
117 \frametitle{What is {\isac}?} |
|
118 \begin{spacing}{1.5} |
|
119 \begin{itemize} |
|
120 \item \textcolor{tug}{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal A}$}belle for~{}\textcolor{tug}{${\cal C}$}alculations |
|
121 \item Interactive Course Material |
|
122 \item Learning Coach |
|
123 \item Developed at Austrian Universities |
|
124 \end{itemize} |
|
125 \end{spacing} |
|
126 \end{frame} |
|
127 |
|
128 \subsection{motivation} |
|
129 \begin{frame} |
|
130 \frametitle{Motivation - {\isac{}}'s~Potential} |
|
131 \begin{itemize} |
|
132 \item Stepwise solving of engineering problems\\ |
|
133 {\small $\rightarrow$ \textcolor{tug}{Consistent Framework}} |
|
134 \item Explaining underlying knowledge\\ |
|
135 {\small $\rightarrow$ \textcolor{tug}{Transparent Content, Access to Multimedia Content}} |
|
136 \item Checking steps input by the student\\ |
|
137 {\small $\rightarrow$ \textcolor{tug}{Proof Situation}} |
|
138 \item Assessing stepwise problem solving\\ |
|
139 {\small $\rightarrow$ \textcolor{tug}{One system for tutoring and assessment}} |
|
140 \end{itemize} |
|
141 \end{frame} |
|
142 |
|
143 |
|
144 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
145 \section{Material Creation} |
|
146 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
147 |
|
148 \begin{frame} |
|
149 \frametitle{Work flow} |
|
150 \begin{spacing}{1.8} |
|
151 \begin{itemize} |
|
152 \item Problem Analysis |
|
153 \item Information Collection |
|
154 \item \textbf{TP-Programming} |
|
155 \item Documentation |
|
156 \end{itemize} |
|
157 \end{spacing} |
|
158 \end{frame} |
|
159 |
|
160 \subsection{issues} |
|
161 \begin{frame} |
|
162 \frametitle{Issues to Accomplish I} |
|
163 \begin{spacing}{1.4} |
|
164 \begin{itemize} |
|
165 \item What knowledge is mechanized in Isabelle?\\ |
|
166 {\small How about new?} |
|
167 \item What problems are implemented in {\sisac{}}?\\ |
|
168 {\small How about new?} |
|
169 \item What is the effort? |
|
170 \end{itemize} |
|
171 \end{spacing} |
|
172 \end{frame} |
|
173 |
|
174 \begin{frame} |
|
175 \frametitle{Issues to Accomplish II} |
|
176 \begin{spacing}{1.4} |
|
177 \begin{itemize} |
|
178 \item How look calculations like?\\ |
|
179 {\small Ansatzs, Subproblems?} |
|
180 \item How are problems specified?\\ |
|
181 {\small Given, Pre-/Postcondition, Find?} |
|
182 \item What is the contents of the interactive course material?\\ |
|
183 {\small Figures, Explanations,\ldots} |
|
184 \end{itemize} |
|
185 \end{spacing} |
|
186 \end{frame} |
|
187 |
|
188 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
189 \section{Details} |
|
190 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
191 |
|
192 \subsection{Technical Survey} |
|
193 \begin{frame} |
|
194 \frametitle{Technical Survey I {\normalsize Mechanizing Knowledge}} |
|
195 \begin{spacing}{1.5} |
|
196 \begin{itemize} |
|
197 \item Not enough knowledge is mechanized\\ |
|
198 {\small Equation Solving, Integrals,\ldots} |
|
199 \item Computer Mathematicians required!\\ |
|
200 {\small Mathematics: Equation solving, Engineer: Z-Transform} |
|
201 \item RISC Linz, Mathematics TU Graz |
|
202 \end{itemize} |
|
203 \end{spacing} |
|
204 \end{frame} |
|
205 |
|
206 \begin{frame} |
|
207 \frametitle{Technical Survey II {\normalsize Notation Problems} } |
|
208 \begin{spacing}{1.5} |
|
209 \begin{itemize} |
|
210 \item Different brackets have different meanings\\ |
|
211 {\small $u[n] \neq u(n)$\ldots in Math; but also in the source code} |
|
212 \item Simplification, tricks and beauty\\ |
|
213 {\small $X\cdot(a+b)+Y\cdot(c+d)=aX+bX+cY+dY$}\\ |
|
214 {\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)=$}\\ |
|
215 {\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)$} $} |
|
216 \end{itemize} |
|
217 \end{spacing} |
|
218 \end{frame} |
|
219 |
|
220 \subsection{Demonstration} |
|
221 \begin{frame} |
|
222 \frametitle{Demonstration of {\isac}} |
|
223 \begin{spacing}{1.5} |
|
224 \begin{itemize} |
|
225 \item TODO |
|
226 \end{itemize} |
|
227 \end{spacing} |
|
228 \end{frame} |
|
229 |
|
230 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
231 \section{Summary} |
|
232 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
233 |
|
234 \begin{frame} |
|
235 \frametitle{Conclusion} |
|
236 \begin{spacing}{1.2} |
|
237 \begin{itemize} |
|
238 \item TP-based language not ready |
|
239 \item Programming guideline not yet sufficient |
|
240 \item Hope for usability in enginieering studies |
|
241 \vspace{5mm} |
|
242 \item Hard to spend 200h on 1 programm |
|
243 \item \isac{} pointed at my own error |
|
244 \end{itemize} |
|
245 \end{spacing} |
|
246 \end{frame} |
|
247 |
|
248 |
|
249 \begin{frame} |
|
250 \frametitle{Contact} |
|
251 \begin{spacing}{1.2} |
|
252 \begin{itemize} |
|
253 \item Isabelle \href{isabelle.in.tum.de}{isabelle.in.tum.de} |
|
254 \item The {\sisac}-Project: \href{www.ist.tugraz.at/isac}{www.ist.tugraz.at/isac} |
|
255 \item Projectleader: \href{mailto:neuper@ist.tugraz.at}{neuper@ist.tugraz.at} |
|
256 \item Jan Rocnik: \href{mailto:jan.rocnik@student.tugraz.at}{jan.rocnik@student.tugraz.at} |
|
257 \end{itemize} |
|
258 \end{spacing} |
|
259 \end{frame} |
|
260 |
|
261 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
262 \end{document} |
|
263 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
264 |
|
265 %% EOF |