1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/Doc/isac/jrocnik/jrocnik_cadgme.tex Sun Jul 14 14:48:14 2013 +0200
1.3 @@ -0,0 +1,281 @@
1.4 +\documentclass[%
1.5 +%handout, % prints handouts (=no animations, for printed version)
1.6 +%mathserif
1.7 +%xcolor=pst,
1.8 +14pt
1.9 +% fleqn
1.10 +]{beamer}
1.11 +
1.12 +\usepackage{beamerthemedefault}
1.13 +
1.14 +\usepackage{color}
1.15 +\definecolor{lgray}{RGB}{238,238,238}
1.16 +\definecolor{gray}{rgb}{0.8,0.8,0.8}
1.17 +
1.18 +\useoutertheme[subsection=false]{smoothbars}
1.19 +%\useinnertheme{circles}
1.20 +
1.21 +\setbeamercolor{block title}{fg=black,bg=gray}
1.22 +\setbeamercolor{block title alerted}{use=alerted text,fg=black,bg=alerted text.fg!75!bg}
1.23 +\setbeamercolor{block title example}{use=example text,fg=black,bg=example text.fg!75!bg}
1.24 +\setbeamercolor{block body}{parent=normal text,use=block title,bg=block title.bg!25!bg}
1.25 +\setbeamercolor{block body alerted}{parent=normal text,use=block title alerted,bg=block title alerted.bg!25!bg}
1.26 +\setbeamercolor{block body example}{parent=normal text,use=block title example,bg=block title example.bg!25!bg}
1.27 +
1.28 +%activate hyperlinks at the end
1.29 +%\usepackage{hyperref}
1.30 +
1.31 +\usepackage[english]{babel}
1.32 +\usepackage[utf8]{inputenc}
1.33 +\usepackage{array}
1.34 +\usepackage{setspace}
1.35 +\usepackage{url}
1.36 +
1.37 +\definecolor{tug}{rgb}{0.96862,0.14509,0.27450}
1.38 +
1.39 +\def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
1.40 +\def\sisac{{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}}
1.41 +
1.42 +\setbeamertemplate{headline}[text line]{
1.43 + \begin{beamercolorbox}[wd=\paperwidth,ht=8ex,dp=4ex]{}
1.44 + \insertnavigation{0.85\paperwidth}
1.45 + \raisebox{-10pt}{\includegraphics[width=15mm]{tuglogo}}\vskip2pt
1.46 + \hskip-1pt\rule{\paperwidth}{0.3pt}
1.47 + \end{beamercolorbox}
1.48 +}
1.49 +
1.50 +\setbeamertemplate{navigation symbols}{}
1.51 +\setbeamercolor{footline}{fg=black,bg=gray}
1.52 +
1.53 +% Fusszeile mit Autor, Titel und Foliennummer / Gesamtfolienzahl
1.54 +\setbeamertemplate{footline}[text line]{
1.55 + \hskip-1pt
1.56 + \begin{beamercolorbox}[wd=\paperwidth]{footline}
1.57 + \rule{\paperwidth}{0.3pt}
1.58 + \colorbox{tug}{\rule{3pt}{0pt}\rule{0pt}{3pt}}
1.59 + \textbf{\rule{0pt}{5pt}\insertshortauthor\hfill\insertshortinstitute\hfill%
1.60 + \insertshorttitle\rule{1em}{0pt}}
1.61 + \rule{\paperwidth}{0.3pt}
1.62 + \end{beamercolorbox}
1.63 + \begin{beamercolorbox}[wd=\paperwidth,ht=2ex,dp=2ex]{white}
1.64 + \end{beamercolorbox}
1.65 +}%
1.66 +
1.67 +%% Titelblatt-Einstellungen
1.68 +\institute[IST]{Institute for Software Technology\\Graz University of Technology}
1.69 +\title[ISAC for Signal Processing]{Interactive Course Material by TP-based Programming}
1.70 +\subtitle{A Case Study}
1.71 +\author{Jan Ro\v{c}nik}
1.72 +\date{24. June 2012}
1.73 +
1.74 +% Subject and Keywords for PDF
1.75 +\subject{CADGME Presentation}
1.76 +\keywords{interactive course material, signal processing, z transform, TP-based programming
1.77 +language, Lucas-Interpreter, Theorem Proving}
1.78 +
1.79 +\titlegraphic{\includegraphics[width=20mm]{tuglogo}}
1.80 +
1.81 +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.82 +\begin{document}
1.83 +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.84 +
1.85 +\begin{frame}[plain]
1.86 + \frametitle{}
1.87 + \titlepage
1.88 +\end{frame}
1.89 +
1.90 +
1.91 +
1.92 +%\begin{frame}
1.93 +% \frametitle{Contents}
1.94 +% \begin{spacing}{0.3}
1.95 +% \tableofcontents[hideallsubsections %
1.96 +% % ,pausesections
1.97 +% ] % erzeugt Inhaltsverzeichnis
1.98 +% \end{spacing}
1.99 +%\end{frame}
1.100 +
1.101 +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.102 +\section{Introduction}
1.103 +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.104 +
1.105 +\subsection{isabelle}
1.106 +\begin{frame}
1.107 + \frametitle{What is Isabelle?}
1.108 + \begin{spacing}{2}
1.109 + \begin{itemize}
1.110 + \item Interactive Theorem Prover (Interactice TP)
1.111 + \item Large body of mechanized math knowledge
1.112 + \item Developed in Cambridge, Munich and Paris
1.113 + \end{itemize}
1.114 + \end{spacing}
1.115 +\end{frame}
1.116 +
1.117 +\subsection{isac}
1.118 +\begin{frame}
1.119 + \frametitle{What is {\isac}?}
1.120 + \begin{spacing}{1.7}
1.121 + \begin{itemize}
1.122 + \item \textcolor{tug}{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal A}$}belle for~{}\textcolor{tug}{${\cal C}$}alculations
1.123 + \item Interactive Course Material
1.124 + \item Learning Coach
1.125 + \item Developed at Austrian Universities
1.126 + \end{itemize}
1.127 + \end{spacing}
1.128 +\end{frame}
1.129 +
1.130 +\subsection{motivation}
1.131 +\begin{frame}
1.132 + \frametitle{{\isac{}} for Interactive Course Material}
1.133 + \begin{itemize}
1.134 + \item Stepwise solving of engineering problems\\
1.135 + {\small $\rightarrow$ \textcolor{tug}{One Framework for all phases of problem solving}}
1.136 + \item Explaining underlying knowledge\\
1.137 + {\small $\rightarrow$ \textcolor{tug}{Transparent Content, Access to Multimedia Content}}
1.138 + \item Checking steps input by the student\\
1.139 + {\small $\rightarrow$ \textcolor{tug}{Proof Situation}}
1.140 + \item Assessing stepwise problem solving\\
1.141 + {\small $\rightarrow$ \textcolor{tug}{One system for tutoring and assessment}}
1.142 + \end{itemize}
1.143 +\end{frame}
1.144 +
1.145 +
1.146 +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.147 +\section{Material Creation}
1.148 +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.149 +
1.150 +\subsection{steps}
1.151 +\begin{frame}
1.152 + \frametitle{Course Material Creation {\normalsize Iterations}} %tasks? work flow?
1.153 + \begin{spacing}{1.3}
1.154 + \begin{enumerate}
1.155 + \item Problem Analysis\\
1.156 + {\small Variants of problem solving steps} %example partial fractions
1.157 + \item \textbf{Analysis of mechanized knowledge}\\
1.158 + {\small Existing and missing knowledge}
1.159 + \item \textbf{Programming in a TP based language (TP-PL)}
1.160 + \item Additional Content\\
1.161 + {\small Multimedia explanations for underlying knowledge}
1.162 + \end{enumerate}
1.163 + \end{spacing}
1.164 +\end{frame}
1.165 +
1.166 +\subsection{issues}
1.167 +\begin{frame}
1.168 + \frametitle{Issues to Accomplish {\normalsize Information Collection}}
1.169 + \begin{spacing}{1.3}
1.170 + \begin{itemize}
1.171 + \item What knowledge is mechanized in Isabelle?\\
1.172 + {\small Theorems, Definitions, Numbers,\ldots}
1.173 + \item What knowledge is mechanized in {\isac{}}?\\
1.174 + {\small Problem specifications, Programs,\ldots}
1.175 + \item What additional explanations are required?\\
1.176 + {\small Figures, Examples,\ldots}
1.177 + \end{itemize}
1.178 + \end{spacing}
1.179 +\end{frame}
1.180 +
1.181 +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.182 +\section{Details}
1.183 +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.184 +
1.185 +\subsection{Technical Survey}
1.186 +%\begin{frame}
1.187 +% \frametitle{Technical Survey I {\normalsize Mechanizing Knowledge}}
1.188 +% \begin{spacing}{1.5}
1.189 +% \begin{itemize}
1.190 +% \item Not enough knowledge is mechanized\\
1.191 +% {\small Equation Solving, Integrals,\ldots}
1.192 +% \item Computer Mathematicians required!\\
1.193 +% {\small Mathematics: Equation solving, Engineer: Z-Transform}
1.194 +% \item RISC Linz, Mathematics TU Graz
1.195 +% \end{itemize}
1.196 +% \end{spacing}
1.197 +%\end{frame}
1.198 +
1.199 +%\begin{frame}
1.200 +% \frametitle{Technical Survey II {\normalsize Representation Problems} }
1.201 +% \begin{spacing}{1.9}
1.202 +% \begin{itemize}
1.203 +% \item Different brackets have different meanings\\
1.204 +% {\small $u[n]$ is a specific function application :) }
1.205 +% \item We need Symbols, Indizes and Hochzahlen
1.206 +% \item Different Representations for different purpos %winkel in polar oder kartesischen koordinaten usw.
1.207 +% \end{itemize}
1.208 +% \end{spacing}
1.209 +%\end{frame}
1.210 +
1.211 +\begin{frame}
1.212 + \frametitle{Representation Problems}
1.213 + \begin{spacing}{1.4}
1.214 + \begin{center}
1.215 +
1.216 + \begin{itemize}
1.217 + \item Can meaning of symbols be varied?\\
1.218 + {\small $u[n]$ is a specific function in Signal Processing}
1.219 + \item Simplification, tricks and beauty
1.220 + \end{itemize}
1.221 +
1.222 + {\small $X\cdot(a+b)+Y\cdot(c+d)=aX+bX+cY+dY$}\\
1.223 + \vspace{3mm}
1.224 + {\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)=$}\\
1.225 + {\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)$} $}
1.226 +
1.227 +
1.228 + \end{center}
1.229 + \end{spacing}
1.230 +\end{frame}
1.231 +
1.232 +\subsection{Demonstration}
1.233 +\begin{frame}
1.234 + \frametitle{Demonstration}
1.235 + \begin{spacing}{1.5}
1.236 + \begin{itemize}
1.237 + \item Backend
1.238 + \begin{itemize}
1.239 + \item Equation solving
1.240 + \item Notation problems, Working with Rulesets
1.241 + \item Framework expansion
1.242 + \item My Work
1.243 + \end{itemize}
1.244 + \end{itemize}
1.245 + \end{spacing}
1.246 +\end{frame}
1.247 +
1.248 +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.249 +\section{Summary}
1.250 +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.251 +
1.252 +\subsection{conclusion}
1.253 +\begin{frame}
1.254 + \frametitle{Conclusion}
1.255 + \begin{spacing}{1.2}
1.256 + \begin{itemize}
1.257 + \item Proof of concept for TP-PL succesfull
1.258 + \item Usability of TP-PL not sufficient
1.259 + \item Requirements for improved usability clarified
1.260 + \vspace{5mm}
1.261 + \item Unacceptable to spend 200h on 1 program
1.262 + \item \isac{} pointed at my own error
1.263 + \end{itemize}
1.264 + \end{spacing}
1.265 +\end{frame}
1.266 +
1.267 +\subsection{contact}
1.268 +\begin{frame}
1.269 + \frametitle{Contact}
1.270 + \begin{spacing}{1.7}
1.271 + \begin{tabular}{lr}
1.272 + Isabelle & \small \texttt{\href{isabelle.in.tum.de}{isabelle.in.tum.de}}\\
1.273 + The {\isac}-Project & \small \texttt{\href{www.ist.tugraz.at/isac}{www.ist.tugraz.at/isac}}\\
1.274 + Project leader & \small \texttt{\href{mailto:wneuper@ist.tugraz.at}{wneuper@ist.tugraz.at}}\\
1.275 + Jan Rocnik & \small \texttt{\href{mailto:jan.rocnik@student.tugraz.at}{jan.rocnik@student.tugraz.at}}
1.276 + \end{tabular}
1.277 + \end{spacing}
1.278 +\end{frame}
1.279 +
1.280 +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.281 +\end{document}
1.282 +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.283 +
1.284 +%% EOF
1.285 \ No newline at end of file