1.1 --- a/doc-src/isac/jrocnik/jrocnik_present2.tex Sun Jul 14 15:02:09 2013 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,299 +0,0 @@
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