jan@42381: \documentclass[%
jan@42381: %handout, % prints handouts (=no animations, for printed version)
jan@42381: %mathserif
jan@42381: %xcolor=pst,
jan@42381: 14pt
jan@42381: % fleqn
jan@42381: ]{beamer}
jan@42381: 
jan@42381: \usepackage{beamerthemedefault}
jan@42381: 
jan@42420: \usepackage{color}
jan@42420: \definecolor{lgray}{RGB}{238,238,238}
jan@42420: 
jan@42381: \useoutertheme[subsection=false]{smoothbars}
jan@42381: \useinnertheme{circles}
jan@42381: 
jan@42381: \setbeamercolor{block title}{fg=black,bg=gray}
jan@42381: \setbeamercolor{block title alerted}{use=alerted text,fg=black,bg=alerted text.fg!75!bg}
jan@42381: \setbeamercolor{block title example}{use=example text,fg=black,bg=example text.fg!75!bg}
jan@42381: \setbeamercolor{block body}{parent=normal text,use=block title,bg=block title.bg!25!bg}
jan@42381: \setbeamercolor{block body alerted}{parent=normal text,use=block title alerted,bg=block title alerted.bg!25!bg}
jan@42381: \setbeamercolor{block body example}{parent=normal text,use=block title example,bg=block title example.bg!25!bg}
jan@42381: 
jan@42401: %activate hyperlinks at the end
jan@42381: %\usepackage{hyperref}
jan@42381: 
jan@42381: \usepackage[english]{babel}
jan@42381: \usepackage[utf8]{inputenc}
jan@42381: \usepackage{array}
jan@42381: \usepackage{setspace}
jan@42381: 
jan@42381: \definecolor{tug}{rgb}{0.96862,0.14509,0.27450}
jan@42381: 
jan@42381: \def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
jan@42381: \def\sisac{{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}}
jan@42381: 
jan@42381: \setbeamertemplate{headline}[text line]{
jan@42381: 	\begin{beamercolorbox}[wd=\paperwidth,ht=8ex,dp=4ex]{}
jan@42381: 		\insertnavigation{0.85\paperwidth} 
jan@42381: 		\raisebox{-10pt}{\includegraphics[width=15mm]{tuglogo}}\vskip2pt
jan@42381: 		\hskip-1pt\rule{\paperwidth}{0.3pt}
jan@42381: 	\end{beamercolorbox}
jan@42381: }
jan@42381: 
jan@42381: \setbeamertemplate{navigation symbols}{}
jan@42381: 
jan@42381: \definecolor{gray}{rgb}{0.8,0.8,0.8}
jan@42381: \setbeamercolor{footline}{fg=black,bg=gray}
jan@42381: 
jan@42381: % Fusszeile mit Autor, Titel und Foliennummer / Gesamtfolienzahl
jan@42381: \setbeamertemplate{footline}[text line]{
jan@42381: 	\hskip-1pt
jan@42381: 	\begin{beamercolorbox}[wd=\paperwidth]{footline}
jan@42381: 			\rule{\paperwidth}{0.3pt}
jan@42381: 			\colorbox{tug}{\rule{3pt}{0pt}\rule{0pt}{3pt}}
jan@42381: 			\textbf{\rule{0pt}{5pt}\insertshortauthor\hfill\insertshortinstitute\hfill%
jan@42381: 					\insertshorttitle\rule{1em}{0pt}}
jan@42381: 			\rule{\paperwidth}{0.3pt}
jan@42381: 	\end{beamercolorbox}
jan@42381: 	\begin{beamercolorbox}[wd=\paperwidth,ht=2ex,dp=2ex]{white}
jan@42381: 	\end{beamercolorbox}
jan@42381: }%
jan@42381: 
jan@42381: %% Titelblatt-Einstellungen
jan@42381: \institute[IST, SPSC]{Institute for Software Technology\\Institute of Signal Processing and Speech Communication\\Graz University of Technology}
jan@42381: \title[ISAC for Signal Processing]{Interactive Course Material for\\ Signal Processing based on\\ Isabelle/\isac}
jan@42381: \subtitle{Baccalaureate Thesis}
jan@42381: \author{Jan Rocnik}
jan@42401: \date{\today}
jan@42381: 
jan@42381: % Subject and Keywords for PDF
jan@42418: \subject{Final presentation of Baccalaureate Thesis}
jan@42418: \keywords{Isac, Isabelle, ist, spsc, thesis, course material}
jan@42381: 
jan@42381: \titlegraphic{\includegraphics[width=20mm]{tuglogo}}
jan@42381: 
jan@42381: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
jan@42381: \begin{document}
jan@42381: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
jan@42381: 
jan@42381: \begin{frame}[plain]
jan@42381:   \frametitle{}
jan@42381:   \titlepage
jan@42381: \end{frame}
jan@42381: 
jan@42381: 
jan@42381: 
jan@42381: \begin{frame}
jan@42381:   \frametitle{Contents}
jan@42401:   \begin{spacing}{0.3}
jan@42381:         \tableofcontents[hideallsubsections %
jan@42381:                         % ,pausesections
jan@42381:                         ] % erzeugt Inhaltsverzeichnis
jan@42401:   \end{spacing}
jan@42381: \end{frame}
jan@42381: 
jan@42381: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
jan@42381: \section{Introduction}
jan@42381: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
jan@42381: 
jan@42381: \subsection{isabelle}
jan@42381: \begin{frame}
jan@42418: 	\frametitle{What is Isabelle?}
jan@42381: 	\begin{spacing}{1.5}
jan@42402: 		\begin{itemize}
jan@42402: 			\item Generic Proof Assistant
jan@42418: 			\item Formula proofing in logical calculus
jan@42402: 			\item Developed in Cambridge, Muenchen and Paris
jan@42402: 		\end{itemize}
jan@42381: 	\end{spacing}
jan@42381: \end{frame}
jan@42381: 
jan@42381: \subsection{isac}
jan@42381: \begin{frame}
jan@42401: 	\frametitle{What is {\isac}?}
jan@42381: 	\begin{spacing}{1.5}
jan@42402: 		\begin{itemize}
jan@42402: 			\item \textcolor{tug}{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal A}$}belle for~{}\textcolor{tug}{${\cal C}$}alculations
jan@42418: 			\item Interactive Course Material
jan@42402: 			\item Learning Coach
jan@42420: 			\item Developed at Austrian Universities
jan@42402: 		\end{itemize}
jan@42381: 	\end{spacing}
jan@42381: \end{frame}
jan@42381: 
jan@42401: \subsection{motivation}
jan@42401: \begin{frame}
jan@42420: 	\frametitle{Motivation - {\isac{}}'s~Potential}
jan@42401: 	\begin{itemize}
jan@42420: 		\item Stepwise solving of engineering problems\\
jan@42402: 					{\small $\rightarrow$ \textcolor{tug}{Consistent Framework}}
jan@42401: 		\item Explaining underlying knowledge\\
jan@42402: 					{\small $\rightarrow$  \textcolor{tug}{Transparent Content, Access to Multimedia Content}}
jan@42402: 		\item Checking steps input by the student\\
jan@42402: 					{\small $\rightarrow$ \textcolor{tug}{Proof Situation}}
jan@42402: 		\item Assessing stepwise problem solving\\
jan@42402: 					{\small $\rightarrow$ \textcolor{tug}{One system for tutoring and assessment}}
jan@42401: 	\end{itemize}
jan@42401: \end{frame}
jan@42401: 
jan@42381: 
jan@42381: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
jan@42381: \section{Thesis Definition}
jan@42381: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
jan@42381: 
jan@42381: \begin{frame}
jan@42401: 	\frametitle{Thesis Definition}
jan@42401: 	%---> Follow up thesis abstract! <---%
jan@42402: 	\begin{spacing}{1.2}
jan@42402: 		\begin{itemize}
jan@42402: 			\item Creation of interactive course material\\
jan@42420: 						{\small Based on problems given by SPSC}
jan@42402: 			\item Content should be usable\ldots
jan@42402: 			\begin{itemize}
jan@42420: 				\item in Signalprocessing Problem Classes
jan@42420: 				\item in \emph{STEOP}
jan@42402: 			\end{itemize}
jan@42402: 			\item Guideline for upcoming TP-Programmers.
jan@42402: 			\item Feedback of usability\\
jan@42402: 			      {\small (TP-Programming-Language)}
jan@42402: 		\end{itemize}
jan@42402: 	\end{spacing}
jan@42381: \end{frame}
jan@42381: 
jan@42381: \subsection{issues}
jan@42381: \begin{frame}
jan@42401: 	\frametitle{Issues to Accomplish I}
jan@42402: 	\begin{spacing}{1.4}
jan@42402: 		\begin{itemize}
jan@42418: 			\item What knowledge is mechanized in Isabelle?\\
jan@42402: 						{\small How about new?}
jan@42402: 			\item What problems are implemented in {\sisac{}}?\\
jan@42402: 						{\small How about new?}
jan@42402: 			\item What is the effort?
jan@42402: 		\end{itemize}
jan@42402: 	\end{spacing}
jan@42401: \end{frame}
jan@42401: 
jan@42401: \begin{frame}
jan@42401: 	\frametitle{Issues to Accomplish II}
jan@42401: \begin{spacing}{1.4}
jan@42381: \begin{itemize}
jan@42402: 	\item How look calculations like?\\
jan@42401: 				{\small Ansatzs, Subproblems?}
jan@42402: 	\item How are problems specified?\\
jan@42401: 				{\small Given, Pre-/Postcondition, Find?}
jan@42418: 	\item What is the contents of the interactive course material?\\
jan@42418: 				{\small Figures, Explanations,\ldots}
jan@42381: \end{itemize}
jan@42401: \end{spacing}
jan@42381: \end{frame}
jan@42381: 
jan@42381: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
jan@42402: \section{Details}
jan@42381: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
jan@42381: 
jan@42418: \subsection{Technical Survey}
jan@42402: \begin{frame}
jan@42418: 	\frametitle{Technical Survey I {\normalsize Mechanizing Knowledge}}
jan@42402: 	\begin{spacing}{1.5}
jan@42402: 		\begin{itemize}
jan@42402: 			\item Not enough knowledge is mechanized\\
jan@42402: 						{\small Equation Solving, Integrals,\ldots}
jan@42420: 			\item Computer Mathematicians required!\\
jan@42420: 						{\small Mathematics: Equation solving, Engineer: Z-Transform}
jan@42420: 			\item RISC Linz, Mathematics TU Graz
jan@42402: 		\end{itemize}
jan@42402: 	\end{spacing}
jan@42402: \end{frame}
jan@42402: 
jan@42402: \begin{frame}
jan@42418: 	\frametitle{Technical Survey II {\normalsize Notation Problems} }
jan@42402: 	\begin{spacing}{1.5}
jan@42402: 		\begin{itemize}
jan@42402: 			\item Different brackets have different meanings\\
jan@42418: 						{\small $u[n] \neq u(n)$\ldots in Math; but also in the source code}
jan@42420: 			\item Simplification, tricks and beauty\\
jan@42420: 						{\small $X\cdot(a+b)+Y\cdot(c+d)=aX+bX+cY+dY$}\\
jan@42420: 						{\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@42420: 						{\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@42402: 		\end{itemize}
jan@42402: 	\end{spacing}
jan@42402: \end{frame}
jan@42402: 
jan@42402: \subsection{Demonstration}
jan@42381: \begin{frame}
jan@42401: 	\frametitle{Demonstration of {\isac}}
jan@42381: 	\begin{spacing}{1.5}
jan@42402: 		\begin{itemize}
jan@42418: 			\item {\Large Development Environment} (Backend)
jan@42402: 			\vspace{15mm}
jan@42402: 			\item {\Large Math Assistant} (Frontend)
jan@42402: 		\end{itemize}
jan@42381: 	\end{spacing}
jan@42381: \end{frame}
jan@42381: 
jan@42381: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
jan@42381: \section{Summary}
jan@42381: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
jan@42381: 
jan@42401: \subsection{Accomplished Work}
jan@42381: \begin{frame}
jan@42401: 	\frametitle{Accomplished Work}
jan@42381: 	\begin{itemize}
jan@42401:       \item Partial Fractions\\ {\small Theorems, Specification, Program}
jan@42401:       \item Inverse Z-Transform with Partial Fractions\\ {\small Theorems, Specification, Program}
jan@42418:       \item Isabelle Theory indicating issues\\ {\small Preparation for {\sisac{}}-developers}
jan@42381: 	\end{itemize}
jan@42381: \end{frame}
jan@42381: 
jan@42381: \subsection{Partially Accomplished}
jan@42381: \begin{frame}
jan@42381: 	\frametitle{Partially Accomplished}
jan@42401: 	\begin{spacing}{1.4}
jan@42402: 		\begin{itemize}
jan@42402: 	     \item Guidelines for Upcoming TP-Programmers\\
jan@42418: 	           {\small \textbf{Note:} Development environment and languages changes} 
jan@42402: 	     \item Examples
jan@42402: 		\end{itemize}
jan@42401: 	\end{spacing}
jan@42381: \end{frame}
jan@42381: 
jan@42381: \subsection{Not Accomplished}
jan@42381: \begin{frame}
jan@42381: 	\frametitle{Not Accomplished}
jan@42401: 	\begin{spacing}{1.2}
jan@42402: 		\begin{itemize}
jan@42418: 	    \item Content of interactive course material\\
jan@42418: 	    			{\small Figures, Explanations,\ldots}
jan@42402: 	    \item A sufficient count of implementations
jan@42402: 	    \item No support of labs and lectures atm
jan@42402: 	    \item No material for \emph{STEOP} atm
jan@42402: 		\end{itemize}
jan@42401: 	\end{spacing}
jan@42381: \end{frame}
jan@42381: 
jan@42381: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
jan@42381: \section{Conclusion}
jan@42381: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
jan@42381: 
jan@42381: \begin{frame}
jan@42418: 	\frametitle{Conclusion}
jan@42401: 	\begin{spacing}{1.2}
jan@42402: 	    \begin{itemize}
jan@42420: 				\item TP-based language not ready
jan@42420: 				\item Programming guideline not yet sufficient
jan@42420: 				\item Hope for usability in enginieering studies
jan@42402: 				\vspace{5mm}
jan@42420: 				\item Hard to spend 200h on 1 programm
jan@42420: 				\item \isac{} pointed at my own error
jan@42402: 			\end{itemize}
jan@42401: 		\end{spacing}
jan@42381: \end{frame}
jan@42381: 
jan@42381: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
jan@42381: \end{document}
jan@42381: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
jan@42381: 
jan@42381: %% EOF