1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/doc-isac/jrocnik/final/jrocnik_present2.tex Tue Sep 17 09:50:52 2013 +0200
1.3 @@ -0,0 +1,299 @@
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 +
1.17 +\useoutertheme[subsection=false]{smoothbars}
1.18 +\useinnertheme{circles}
1.19 +
1.20 +\setbeamercolor{block title}{fg=black,bg=gray}
1.21 +\setbeamercolor{block title alerted}{use=alerted text,fg=black,bg=alerted text.fg!75!bg}
1.22 +\setbeamercolor{block title example}{use=example text,fg=black,bg=example text.fg!75!bg}
1.23 +\setbeamercolor{block body}{parent=normal text,use=block title,bg=block title.bg!25!bg}
1.24 +\setbeamercolor{block body alerted}{parent=normal text,use=block title alerted,bg=block title alerted.bg!25!bg}
1.25 +\setbeamercolor{block body example}{parent=normal text,use=block title example,bg=block title example.bg!25!bg}
1.26 +
1.27 +%activate hyperlinks at the end
1.28 +%\usepackage{hyperref}
1.29 +
1.30 +\usepackage[english]{babel}
1.31 +\usepackage[utf8]{inputenc}
1.32 +\usepackage{array}
1.33 +\usepackage{setspace}
1.34 +
1.35 +\definecolor{tug}{rgb}{0.96862,0.14509,0.27450}
1.36 +
1.37 +\def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
1.38 +\def\sisac{{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}}
1.39 +
1.40 +\setbeamertemplate{headline}[text line]{
1.41 + \begin{beamercolorbox}[wd=\paperwidth,ht=8ex,dp=4ex]{}
1.42 + \insertnavigation{0.85\paperwidth}
1.43 + \raisebox{-10pt}{\includegraphics[width=15mm]{tuglogo}}\vskip2pt
1.44 + \hskip-1pt\rule{\paperwidth}{0.3pt}
1.45 + \end{beamercolorbox}
1.46 +}
1.47 +
1.48 +\setbeamertemplate{navigation symbols}{}
1.49 +
1.50 +\definecolor{gray}{rgb}{0.8,0.8,0.8}
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, SPSC]{Institute for Software Technology\\Institute of Signal Processing and Speech Communication\\Graz University of Technology}
1.69 +\title[ISAC for Signal Processing]{Interactive Course Material for\\ Signal Processing based on\\ Isabelle/\isac}
1.70 +\subtitle{Baccalaureate Thesis}
1.71 +\author{Jan Rocnik}
1.72 +\date{\today}
1.73 +
1.74 +% Subject and Keywords for PDF
1.75 +\subject{Final presentation of Baccalaureate Thesis}
1.76 +\keywords{Isac, Isabelle, ist, spsc, thesis, course material}
1.77 +
1.78 +\titlegraphic{\includegraphics[width=20mm]{tuglogo}}
1.79 +
1.80 +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.81 +\begin{document}
1.82 +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.83 +
1.84 +\begin{frame}[plain]
1.85 + \frametitle{}
1.86 + \titlepage
1.87 +\end{frame}
1.88 +
1.89 +
1.90 +
1.91 +\begin{frame}
1.92 + \frametitle{Contents}
1.93 + \begin{spacing}{0.3}
1.94 + \tableofcontents[hideallsubsections %
1.95 + % ,pausesections
1.96 + ] % erzeugt Inhaltsverzeichnis
1.97 + \end{spacing}
1.98 +\end{frame}
1.99 +
1.100 +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.101 +\section{Introduction}
1.102 +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.103 +
1.104 +\subsection{isabelle}
1.105 +\begin{frame}
1.106 + \frametitle{What is Isabelle?}
1.107 + \begin{spacing}{1.5}
1.108 + \begin{itemize}
1.109 + \item Generic Proof Assistant
1.110 + \item Formula proofing in logical calculus
1.111 + \item Developed in Cambridge, Muenchen and Paris
1.112 + \end{itemize}
1.113 + \end{spacing}
1.114 +\end{frame}
1.115 +
1.116 +\subsection{isac}
1.117 +\begin{frame}
1.118 + \frametitle{What is {\isac}?}
1.119 + \begin{spacing}{1.5}
1.120 + \begin{itemize}
1.121 + \item \textcolor{tug}{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal A}$}belle for~{}\textcolor{tug}{${\cal C}$}alculations
1.122 + \item Interactive Course Material
1.123 + \item Learning Coach
1.124 + \item Developed at Austrian Universities
1.125 + \end{itemize}
1.126 + \end{spacing}
1.127 +\end{frame}
1.128 +
1.129 +\subsection{motivation}
1.130 +\begin{frame}
1.131 + \frametitle{Motivation - {\isac{}}'s~Potential}
1.132 + \begin{itemize}
1.133 + \item Stepwise solving of engineering problems\\
1.134 + {\small $\rightarrow$ \textcolor{tug}{Consistent Framework}}
1.135 + \item Explaining underlying knowledge\\
1.136 + {\small $\rightarrow$ \textcolor{tug}{Transparent Content, Access to Multimedia Content}}
1.137 + \item Checking steps input by the student\\
1.138 + {\small $\rightarrow$ \textcolor{tug}{Proof Situation}}
1.139 + \item Assessing stepwise problem solving\\
1.140 + {\small $\rightarrow$ \textcolor{tug}{One system for tutoring and assessment}}
1.141 + \end{itemize}
1.142 +\end{frame}
1.143 +
1.144 +
1.145 +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.146 +\section{Thesis Definition}
1.147 +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.148 +
1.149 +\begin{frame}
1.150 + \frametitle{Thesis Definition}
1.151 + %---> Follow up thesis abstract! <---%
1.152 + \begin{spacing}{1.2}
1.153 + \begin{itemize}
1.154 + \item Creation of interactive course material\\
1.155 + {\small Based on problems given by SPSC}
1.156 + \item Content should be usable\ldots
1.157 + \begin{itemize}
1.158 + \item in Signalprocessing Problem Classes
1.159 + \item in \emph{STEOP}
1.160 + \end{itemize}
1.161 + \item Guideline for upcoming TP-Programmers.
1.162 + \item Feedback of usability\\
1.163 + {\small (TP-Programming-Language)}
1.164 + \end{itemize}
1.165 + \end{spacing}
1.166 +\end{frame}
1.167 +
1.168 +\subsection{issues}
1.169 +\begin{frame}
1.170 + \frametitle{Issues to Accomplish I}
1.171 + \begin{spacing}{1.4}
1.172 + \begin{itemize}
1.173 + \item What knowledge is mechanized in Isabelle?\\
1.174 + {\small How about new?}
1.175 + \item What problems are implemented in {\sisac{}}?\\
1.176 + {\small How about new?}
1.177 + \item What is the effort?
1.178 + \end{itemize}
1.179 + \end{spacing}
1.180 +\end{frame}
1.181 +
1.182 +\begin{frame}
1.183 + \frametitle{Issues to Accomplish II}
1.184 +\begin{spacing}{1.4}
1.185 +\begin{itemize}
1.186 + \item How look calculations like?\\
1.187 + {\small Ansatzs, Subproblems?}
1.188 + \item How are problems specified?\\
1.189 + {\small Given, Pre-/Postcondition, Find?}
1.190 + \item What is the contents of the interactive course material?\\
1.191 + {\small Figures, Explanations,\ldots}
1.192 +\end{itemize}
1.193 +\end{spacing}
1.194 +\end{frame}
1.195 +
1.196 +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.197 +\section{Details}
1.198 +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.199 +
1.200 +\subsection{Technical Survey}
1.201 +\begin{frame}
1.202 + \frametitle{Technical Survey I {\normalsize Mechanizing Knowledge}}
1.203 + \begin{spacing}{1.5}
1.204 + \begin{itemize}
1.205 + \item Not enough knowledge is mechanized\\
1.206 + {\small Equation Solving, Integrals,\ldots}
1.207 + \item Computer Mathematicians required!\\
1.208 + {\small Mathematics: Equation solving, Engineer: Z-Transform}
1.209 + \item RISC Linz, Mathematics TU Graz
1.210 + \end{itemize}
1.211 + \end{spacing}
1.212 +\end{frame}
1.213 +
1.214 +\begin{frame}
1.215 + \frametitle{Technical Survey II {\normalsize Notation Problems} }
1.216 + \begin{spacing}{1.5}
1.217 + \begin{itemize}
1.218 + \item Different brackets have different meanings\\
1.219 + {\small $u[n] \neq u(n)$\ldots in Math; but also in the source code}
1.220 + \item Simplification, tricks and beauty\\
1.221 + {\small $X\cdot(a+b)+Y\cdot(c+d)=aX+bX+cY+dY$}\\
1.222 + {\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.223 + {\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.224 + \end{itemize}
1.225 + \end{spacing}
1.226 +\end{frame}
1.227 +
1.228 +\subsection{Demonstration}
1.229 +\begin{frame}
1.230 + \frametitle{Demonstration of {\isac}}
1.231 + \begin{spacing}{1.5}
1.232 + \begin{itemize}
1.233 + \item {\Large Development Environment} (Backend)
1.234 + \vspace{15mm}
1.235 + \item {\Large Math Assistant} (Frontend)
1.236 + \end{itemize}
1.237 + \end{spacing}
1.238 +\end{frame}
1.239 +
1.240 +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.241 +\section{Summary}
1.242 +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.243 +
1.244 +\subsection{Accomplished Work}
1.245 +\begin{frame}
1.246 + \frametitle{Accomplished Work}
1.247 + \begin{itemize}
1.248 + \item Partial Fractions\\ {\small Theorems, Specification, Program}
1.249 + \item Inverse Z-Transform with Partial Fractions\\ {\small Theorems, Specification, Program}
1.250 + \item Isabelle Theory indicating issues\\ {\small Preparation for {\sisac{}}-developers}
1.251 + \end{itemize}
1.252 +\end{frame}
1.253 +
1.254 +\subsection{Partially Accomplished}
1.255 +\begin{frame}
1.256 + \frametitle{Partially Accomplished}
1.257 + \begin{spacing}{1.4}
1.258 + \begin{itemize}
1.259 + \item Guidelines for Upcoming TP-Programmers\\
1.260 + {\small \textbf{Note:} Development environment and languages changes}
1.261 + \item Examples
1.262 + \end{itemize}
1.263 + \end{spacing}
1.264 +\end{frame}
1.265 +
1.266 +\subsection{Not Accomplished}
1.267 +\begin{frame}
1.268 + \frametitle{Not Accomplished}
1.269 + \begin{spacing}{1.2}
1.270 + \begin{itemize}
1.271 + \item Content of interactive course material\\
1.272 + {\small Figures, Explanations,\ldots}
1.273 + \item A sufficient count of implementations
1.274 + \item No support of labs and lectures atm
1.275 + \item No material for \emph{STEOP} atm
1.276 + \end{itemize}
1.277 + \end{spacing}
1.278 +\end{frame}
1.279 +
1.280 +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.281 +\section{Conclusion}
1.282 +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.283 +
1.284 +\begin{frame}
1.285 + \frametitle{Conclusion}
1.286 + \begin{spacing}{1.2}
1.287 + \begin{itemize}
1.288 + \item TP-based language not ready
1.289 + \item Programming guideline not yet sufficient
1.290 + \item Hope for usability in enginieering studies
1.291 + \vspace{5mm}
1.292 + \item Hard to spend 200h on 1 programm
1.293 + \item \isac{} pointed at my own error
1.294 + \end{itemize}
1.295 + \end{spacing}
1.296 +\end{frame}
1.297 +
1.298 +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.299 +\end{document}
1.300 +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.301 +
1.302 +%% EOF
1.303 \ No newline at end of file