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