2 %handout, % prints handouts (=no animations, for printed version)
9 \usepackage{beamerthemedefault}
12 \definecolor{lgray}{RGB}{238,238,238}
13 \definecolor{gray}{rgb}{0.8,0.8,0.8}
15 \useoutertheme[subsection=false]{smoothbars}
16 %\useinnertheme{circles}
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}
25 %activate hyperlinks at the end
26 %\usepackage{hyperref}
28 \usepackage[english]{babel}
29 \usepackage[utf8]{inputenc}
34 \definecolor{tug}{rgb}{0.96862,0.14509,0.27450}
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}$}}
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}
47 \setbeamertemplate{navigation symbols}{}
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]{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}
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}
76 \titlegraphic{\includegraphics[width=20mm]{tuglogo}}
78 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
80 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
90 % \frametitle{Contents}
91 % \begin{spacing}{0.3}
92 % \tableofcontents[hideallsubsections %
94 % ] % erzeugt Inhaltsverzeichnis
98 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
99 \section{Introduction}
100 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
102 \subsection{isabelle}
104 \frametitle{What is Isabelle?}
107 \item Interactive Theorem Prover (Interactice TP)
108 \item Large body of mechanized math knowledge
109 \item Developed in Cambridge, Munich and Paris
116 \frametitle{What is {\isac}?}
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
122 \item Developed at Austrian Universities
127 \subsection{motivation}
129 \frametitle{{\isac{}} for Interactive Course Material}
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}}
143 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
144 \section{Material Creation}
145 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
149 \frametitle{Course Material Creation {\normalsize Iterations}} %tasks? work flow?
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}
165 \frametitle{Issues to Accomplish {\normalsize Information Collection}}
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}
178 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
180 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
182 \subsection{Technical Survey}
184 % \frametitle{Technical Survey I {\normalsize Mechanizing Knowledge}}
185 % \begin{spacing}{1.5}
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
197 % \frametitle{Technical Survey II {\normalsize Representation Problems} }
198 % \begin{spacing}{1.9}
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.
209 \frametitle{Representation Problems}
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
219 {\small $X\cdot(a+b)+Y\cdot(c+d)=aX+bX+cY+dY$}\\
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)$} $}
229 \subsection{Demonstration}
231 \frametitle{Demonstration}
236 \item Equation solving
237 \item Notation problems, Working with Rulesets
238 \item Framework expansion
245 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
247 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
249 \subsection{conclusion}
251 \frametitle{Conclusion}
254 \item Proof of concept for TP-PL succesfull
255 \item Usability of TP-PL not sufficient
256 \item Requirements for improved usability clarified
258 \item Unacceptable to spend 200h on 1 program
259 \item \isac{} pointed at my own error
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}}
277 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
279 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%