|
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 \definecolor{gray}{rgb}{0.8,0.8,0.8} |
|
14 |
|
15 \useoutertheme[subsection=false]{smoothbars} |
|
16 %\useinnertheme{circles} |
|
17 |
|
18 \setbeamercolor{block title}{fg=black,bg=gray} |
|
19 \setbeamercolor{block title alerted}{use=alerted text,fg=black,bg=alerted text.fg!75!bg} |
|
20 \setbeamercolor{block title example}{use=example text,fg=black,bg=example text.fg!75!bg} |
|
21 \setbeamercolor{block body}{parent=normal text,use=block title,bg=block title.bg!25!bg} |
|
22 \setbeamercolor{block body alerted}{parent=normal text,use=block title alerted,bg=block title alerted.bg!25!bg} |
|
23 \setbeamercolor{block body example}{parent=normal text,use=block title example,bg=block title example.bg!25!bg} |
|
24 |
|
25 %activate hyperlinks at the end |
|
26 %\usepackage{hyperref} |
|
27 |
|
28 \usepackage[english]{babel} |
|
29 \usepackage[utf8]{inputenc} |
|
30 \usepackage{array} |
|
31 \usepackage{setspace} |
|
32 \usepackage{url} |
|
33 |
|
34 \definecolor{tug}{rgb}{0.96862,0.14509,0.27450} |
|
35 |
|
36 \def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$} |
|
37 \def\sisac{{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}} |
|
38 |
|
39 \setbeamertemplate{headline}[text line]{ |
|
40 \begin{beamercolorbox}[wd=\paperwidth,ht=8ex,dp=4ex]{} |
|
41 \insertnavigation{0.85\paperwidth} |
|
42 \raisebox{-10pt}{\includegraphics[width=15mm]{tuglogo}}\vskip2pt |
|
43 \hskip-1pt\rule{\paperwidth}{0.3pt} |
|
44 \end{beamercolorbox} |
|
45 } |
|
46 |
|
47 \setbeamertemplate{navigation symbols}{} |
|
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]{Institute for Software Technology\\Graz University of Technology} |
|
66 \title[ISAC for Signal Processing]{Interactive Course Material by TP-based Programming} |
|
67 \subtitle{A Case Study} |
|
68 \author{Jan Ro\v{c}nik} |
|
69 \date{24. June 2012} |
|
70 |
|
71 % Subject and Keywords for PDF |
|
72 \subject{CADGME Presentation} |
|
73 \keywords{interactive course material, signal processing, z transform, TP-based programming |
|
74 language, Lucas-Interpreter, Theorem Proving} |
|
75 |
|
76 \titlegraphic{\includegraphics[width=20mm]{tuglogo}} |
|
77 |
|
78 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
79 \begin{document} |
|
80 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
81 |
|
82 \begin{frame}[plain] |
|
83 \frametitle{} |
|
84 \titlepage |
|
85 \end{frame} |
|
86 |
|
87 |
|
88 |
|
89 %\begin{frame} |
|
90 % \frametitle{Contents} |
|
91 % \begin{spacing}{0.3} |
|
92 % \tableofcontents[hideallsubsections % |
|
93 % % ,pausesections |
|
94 % ] % erzeugt Inhaltsverzeichnis |
|
95 % \end{spacing} |
|
96 %\end{frame} |
|
97 |
|
98 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
99 \section{Introduction} |
|
100 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
101 |
|
102 \subsection{isabelle} |
|
103 \begin{frame} |
|
104 \frametitle{What is Isabelle?} |
|
105 \begin{spacing}{2} |
|
106 \begin{itemize} |
|
107 \item Interactive Theorem Prover (Interactice TP) |
|
108 \item Large body of mechanized math knowledge |
|
109 \item Developed in Cambridge, Munich and Paris |
|
110 \end{itemize} |
|
111 \end{spacing} |
|
112 \end{frame} |
|
113 |
|
114 \subsection{isac} |
|
115 \begin{frame} |
|
116 \frametitle{What is {\isac}?} |
|
117 \begin{spacing}{1.7} |
|
118 \begin{itemize} |
|
119 \item \textcolor{tug}{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal A}$}belle for~{}\textcolor{tug}{${\cal C}$}alculations |
|
120 \item Interactive Course Material |
|
121 \item Learning Coach |
|
122 \item Developed at Austrian Universities |
|
123 \end{itemize} |
|
124 \end{spacing} |
|
125 \end{frame} |
|
126 |
|
127 \subsection{motivation} |
|
128 \begin{frame} |
|
129 \frametitle{{\isac{}} for Interactive Course Material} |
|
130 \begin{itemize} |
|
131 \item Stepwise solving of engineering problems\\ |
|
132 {\small $\rightarrow$ \textcolor{tug}{One Framework for all phases of problem solving}} |
|
133 \item Explaining underlying knowledge\\ |
|
134 {\small $\rightarrow$ \textcolor{tug}{Transparent Content, Access to Multimedia Content}} |
|
135 \item Checking steps input by the student\\ |
|
136 {\small $\rightarrow$ \textcolor{tug}{Proof Situation}} |
|
137 \item Assessing stepwise problem solving\\ |
|
138 {\small $\rightarrow$ \textcolor{tug}{One system for tutoring and assessment}} |
|
139 \end{itemize} |
|
140 \end{frame} |
|
141 |
|
142 |
|
143 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
144 \section{Material Creation} |
|
145 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
146 |
|
147 \subsection{steps} |
|
148 \begin{frame} |
|
149 \frametitle{Course Material Creation {\normalsize Iterations}} %tasks? work flow? |
|
150 \begin{spacing}{1.3} |
|
151 \begin{enumerate} |
|
152 \item Problem Analysis\\ |
|
153 {\small Variants of problem solving steps} %example partial fractions |
|
154 \item \textbf{Analysis of mechanized knowledge}\\ |
|
155 {\small Existing and missing knowledge} |
|
156 \item \textbf{Programming in a TP based language (TP-PL)} |
|
157 \item Additional Content\\ |
|
158 {\small Multimedia explanations for underlying knowledge} |
|
159 \end{enumerate} |
|
160 \end{spacing} |
|
161 \end{frame} |
|
162 |
|
163 \subsection{issues} |
|
164 \begin{frame} |
|
165 \frametitle{Issues to Accomplish {\normalsize Information Collection}} |
|
166 \begin{spacing}{1.3} |
|
167 \begin{itemize} |
|
168 \item What knowledge is mechanized in Isabelle?\\ |
|
169 {\small Theorems, Definitions, Numbers,\ldots} |
|
170 \item What knowledge is mechanized in {\isac{}}?\\ |
|
171 {\small Problem specifications, Programs,\ldots} |
|
172 \item What additional explanations are required?\\ |
|
173 {\small Figures, Examples,\ldots} |
|
174 \end{itemize} |
|
175 \end{spacing} |
|
176 \end{frame} |
|
177 |
|
178 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
179 \section{Details} |
|
180 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
181 |
|
182 \subsection{Technical Survey} |
|
183 %\begin{frame} |
|
184 % \frametitle{Technical Survey I {\normalsize Mechanizing Knowledge}} |
|
185 % \begin{spacing}{1.5} |
|
186 % \begin{itemize} |
|
187 % \item Not enough knowledge is mechanized\\ |
|
188 % {\small Equation Solving, Integrals,\ldots} |
|
189 % \item Computer Mathematicians required!\\ |
|
190 % {\small Mathematics: Equation solving, Engineer: Z-Transform} |
|
191 % \item RISC Linz, Mathematics TU Graz |
|
192 % \end{itemize} |
|
193 % \end{spacing} |
|
194 %\end{frame} |
|
195 |
|
196 %\begin{frame} |
|
197 % \frametitle{Technical Survey II {\normalsize Representation Problems} } |
|
198 % \begin{spacing}{1.9} |
|
199 % \begin{itemize} |
|
200 % \item Different brackets have different meanings\\ |
|
201 % {\small $u[n]$ is a specific function application :) } |
|
202 % \item We need Symbols, Indizes and Hochzahlen |
|
203 % \item Different Representations for different purpos %winkel in polar oder kartesischen koordinaten usw. |
|
204 % \end{itemize} |
|
205 % \end{spacing} |
|
206 %\end{frame} |
|
207 |
|
208 \begin{frame} |
|
209 \frametitle{Representation Problems} |
|
210 \begin{spacing}{1.4} |
|
211 \begin{center} |
|
212 |
|
213 \begin{itemize} |
|
214 \item Can meaning of symbols be varied?\\ |
|
215 {\small $u[n]$ is a specific function in Signal Processing} |
|
216 \item Simplification, tricks and beauty |
|
217 \end{itemize} |
|
218 |
|
219 {\small $X\cdot(a+b)+Y\cdot(c+d)=aX+bX+cY+dY$}\\ |
|
220 \vspace{3mm} |
|
221 {\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)=$}\\ |
|
222 {\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)$} $} |
|
223 |
|
224 |
|
225 \end{center} |
|
226 \end{spacing} |
|
227 \end{frame} |
|
228 |
|
229 \subsection{Demonstration} |
|
230 \begin{frame} |
|
231 \frametitle{Demonstration} |
|
232 \begin{spacing}{1.5} |
|
233 \begin{itemize} |
|
234 \item Backend |
|
235 \begin{itemize} |
|
236 \item Equation solving |
|
237 \item Notation problems, Working with Rulesets |
|
238 \item Framework expansion |
|
239 \item My Work |
|
240 \end{itemize} |
|
241 \end{itemize} |
|
242 \end{spacing} |
|
243 \end{frame} |
|
244 |
|
245 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
246 \section{Summary} |
|
247 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
248 |
|
249 \subsection{conclusion} |
|
250 \begin{frame} |
|
251 \frametitle{Conclusion} |
|
252 \begin{spacing}{1.2} |
|
253 \begin{itemize} |
|
254 \item Proof of concept for TP-PL succesfull |
|
255 \item Usability of TP-PL not sufficient |
|
256 \item Requirements for improved usability clarified |
|
257 \vspace{5mm} |
|
258 \item Unacceptable to spend 200h on 1 program |
|
259 \item \isac{} pointed at my own error |
|
260 \end{itemize} |
|
261 \end{spacing} |
|
262 \end{frame} |
|
263 |
|
264 \subsection{contact} |
|
265 \begin{frame} |
|
266 \frametitle{Contact} |
|
267 \begin{spacing}{1.7} |
|
268 \begin{tabular}{lr} |
|
269 Isabelle & \small \texttt{\href{isabelle.in.tum.de}{isabelle.in.tum.de}}\\ |
|
270 The {\isac}-Project & \small \texttt{\href{www.ist.tugraz.at/isac}{www.ist.tugraz.at/isac}}\\ |
|
271 Project leader & \small \texttt{\href{mailto:wneuper@ist.tugraz.at}{wneuper@ist.tugraz.at}}\\ |
|
272 Jan Rocnik & \small \texttt{\href{mailto:jan.rocnik@student.tugraz.at}{jan.rocnik@student.tugraz.at}} |
|
273 \end{tabular} |
|
274 \end{spacing} |
|
275 \end{frame} |
|
276 |
|
277 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
278 \end{document} |
|
279 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
280 |
|
281 %% EOF |