Mercurial Mercurial > wneuper > isa / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
doc-isac/jrocnik/final/jrocnik_present2.tex
author Walther Neuper <neuper@ist.tugraz.at>
Tue, 17 Sep 2013 09:50:52 +0200
changeset 52107 f8845fc8f38d
parent 52058 src/Doc/isac/jrocnik/final/jrocnik_present2.tex@83aff4cb984a
permissions -rwxr-xr-x
separated Isac documentation (~~/doc-isac) from Isabelle documentation (~~/src/Doc) 
     1 \documentclass[%

     2 %handout, % prints handouts (=no animations, for printed version)

     3 %mathserif

     4 %xcolor=pst,

     5 14pt

     6 % fleqn

     7 ]{beamer}

     8 

     9 \usepackage{beamerthemedefault}

    10 

    11 \usepackage{color}

    12 \definecolor{lgray}{RGB}{238,238,238}

    13 

    14 \useoutertheme[subsection=false]{smoothbars}

    15 \useinnertheme{circles}

    16 

    17 \setbeamercolor{block title}{fg=black,bg=gray}

    18 \setbeamercolor{block title alerted}{use=alerted text,fg=black,bg=alerted text.fg!75!bg}

    19 \setbeamercolor{block title example}{use=example text,fg=black,bg=example text.fg!75!bg}

    20 \setbeamercolor{block body}{parent=normal text,use=block title,bg=block title.bg!25!bg}

    21 \setbeamercolor{block body alerted}{parent=normal text,use=block title alerted,bg=block title alerted.bg!25!bg}

    22 \setbeamercolor{block body example}{parent=normal text,use=block title example,bg=block title example.bg!25!bg}

    23 

    24 %activate hyperlinks at the end

    25 %\usepackage{hyperref}

    26 

    27 \usepackage[english]{babel}

    28 \usepackage[utf8]{inputenc}

    29 \usepackage{array}

    30 \usepackage{setspace}

    31 

    32 \definecolor{tug}{rgb}{0.96862,0.14509,0.27450}

    33 

    34 \def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}

    35 \def\sisac{{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}}

    36 

    37 \setbeamertemplate{headline}[text line]{

    38 	\begin{beamercolorbox}[wd=\paperwidth,ht=8ex,dp=4ex]{}

    39 		\insertnavigation{0.85\paperwidth} 

    40 		\raisebox{-10pt}{\includegraphics[width=15mm]{tuglogo}}\vskip2pt

    41 		\hskip-1pt\rule{\paperwidth}{0.3pt}

    42 	\end{beamercolorbox}

    43 }

    44 

    45 \setbeamertemplate{navigation symbols}{}

    46 

    47 \definecolor{gray}{rgb}{0.8,0.8,0.8}

    48 \setbeamercolor{footline}{fg=black,bg=gray}

    49 

    50 % Fusszeile mit Autor, Titel und Foliennummer / Gesamtfolienzahl

    51 \setbeamertemplate{footline}[text line]{

    52 	\hskip-1pt

    53 	\begin{beamercolorbox}[wd=\paperwidth]{footline}

    54 			\rule{\paperwidth}{0.3pt}

    55 			\colorbox{tug}{\rule{3pt}{0pt}\rule{0pt}{3pt}}

    56 			\textbf{\rule{0pt}{5pt}\insertshortauthor\hfill\insertshortinstitute\hfill%

    57 					\insertshorttitle\rule{1em}{0pt}}

    58 			\rule{\paperwidth}{0.3pt}

    59 	\end{beamercolorbox}

    60 	\begin{beamercolorbox}[wd=\paperwidth,ht=2ex,dp=2ex]{white}

    61 	\end{beamercolorbox}

    62 }%

    63 

    64 %% Titelblatt-Einstellungen

    65 \institute[IST, SPSC]{Institute for Software Technology\\Institute of Signal Processing and Speech Communication\\Graz University of Technology}

    66 \title[ISAC for Signal Processing]{Interactive Course Material for\\ Signal Processing based on\\ Isabelle/\isac}

    67 \subtitle{Baccalaureate Thesis}

    68 \author{Jan Rocnik}

    69 \date{\today}

    70 

    71 % Subject and Keywords for PDF

    72 \subject{Final presentation of Baccalaureate Thesis}

    73 \keywords{Isac, Isabelle, ist, spsc, thesis, course material}

    74 

    75 \titlegraphic{\includegraphics[width=20mm]{tuglogo}}

    76 

    77 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    78 \begin{document}

    79 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    80 

    81 \begin{frame}[plain]

    82   \frametitle{}

    83   \titlepage

    84 \end{frame}

    85 

    86 

    87 

    88 \begin{frame}

    89   \frametitle{Contents}

    90   \begin{spacing}{0.3}

    91         \tableofcontents[hideallsubsections %

    92                         % ,pausesections

    93                         ] % erzeugt Inhaltsverzeichnis

    94   \end{spacing}

    95 \end{frame}

    96 

    97 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    98 \section{Introduction}

    99 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   100 

   101 \subsection{isabelle}

   102 \begin{frame}

   103 	\frametitle{What is Isabelle?}

   104 	\begin{spacing}{1.5}

   105 		\begin{itemize}

   106 			\item Generic Proof Assistant

   107 			\item Formula proofing in logical calculus

   108 			\item Developed in Cambridge, Muenchen and Paris

   109 		\end{itemize}

   110 	\end{spacing}

   111 \end{frame}

   112 

   113 \subsection{isac}

   114 \begin{frame}

   115 	\frametitle{What is {\isac}?}

   116 	\begin{spacing}{1.5}

   117 		\begin{itemize}

   118 			\item \textcolor{tug}{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal A}$}belle for~{}\textcolor{tug}{${\cal C}$}alculations

   119 			\item Interactive Course Material

   120 			\item Learning Coach

   121 			\item Developed at Austrian Universities

   122 		\end{itemize}

   123 	\end{spacing}

   124 \end{frame}

   125 

   126 \subsection{motivation}

   127 \begin{frame}

   128 	\frametitle{Motivation - {\isac{}}'s~Potential}

   129 	\begin{itemize}

   130 		\item Stepwise solving of engineering problems\\

   131 					{\small $\rightarrow$ \textcolor{tug}{Consistent Framework}}

   132 		\item Explaining underlying knowledge\\

   133 					{\small $\rightarrow$  \textcolor{tug}{Transparent Content, Access to Multimedia Content}}

   134 		\item Checking steps input by the student\\

   135 					{\small $\rightarrow$ \textcolor{tug}{Proof Situation}}

   136 		\item Assessing stepwise problem solving\\

   137 					{\small $\rightarrow$ \textcolor{tug}{One system for tutoring and assessment}}

   138 	\end{itemize}

   139 \end{frame}

   140 

   141 

   142 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   143 \section{Thesis Definition}

   144 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   145 

   146 \begin{frame}

   147 	\frametitle{Thesis Definition}

   148 	%---> Follow up thesis abstract! <---%

   149 	\begin{spacing}{1.2}

   150 		\begin{itemize}

   151 			\item Creation of interactive course material\\

   152 						{\small Based on problems given by SPSC}

   153 			\item Content should be usable\ldots

   154 			\begin{itemize}

   155 				\item in Signalprocessing Problem Classes

   156 				\item in \emph{STEOP}

   157 			\end{itemize}

   158 			\item Guideline for upcoming TP-Programmers.

   159 			\item Feedback of usability\\

   160 			      {\small (TP-Programming-Language)}

   161 		\end{itemize}

   162 	\end{spacing}

   163 \end{frame}

   164 

   165 \subsection{issues}

   166 \begin{frame}

   167 	\frametitle{Issues to Accomplish I}

   168 	\begin{spacing}{1.4}

   169 		\begin{itemize}

   170 			\item What knowledge is mechanized in Isabelle?\\

   171 						{\small How about new?}

   172 			\item What problems are implemented in {\sisac{}}?\\

   173 						{\small How about new?}

   174 			\item What is the effort?

   175 		\end{itemize}

   176 	\end{spacing}

   177 \end{frame}

   178 

   179 \begin{frame}

   180 	\frametitle{Issues to Accomplish II}

   181 \begin{spacing}{1.4}

   182 \begin{itemize}

   183 	\item How look calculations like?\\

   184 				{\small Ansatzs, Subproblems?}

   185 	\item How are problems specified?\\

   186 				{\small Given, Pre-/Postcondition, Find?}

   187 	\item What is the contents of the interactive course material?\\

   188 				{\small Figures, Explanations,\ldots}

   189 \end{itemize}

   190 \end{spacing}

   191 \end{frame}

   192 

   193 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   194 \section{Details}

   195 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   196 

   197 \subsection{Technical Survey}

   198 \begin{frame}

   199 	\frametitle{Technical Survey I {\normalsize Mechanizing Knowledge}}

   200 	\begin{spacing}{1.5}

   201 		\begin{itemize}

   202 			\item Not enough knowledge is mechanized\\

   203 						{\small Equation Solving, Integrals,\ldots}

   204 			\item Computer Mathematicians required!\\

   205 						{\small Mathematics: Equation solving, Engineer: Z-Transform}

   206 			\item RISC Linz, Mathematics TU Graz

   207 		\end{itemize}

   208 	\end{spacing}

   209 \end{frame}

   210 

   211 \begin{frame}

   212 	\frametitle{Technical Survey II {\normalsize Notation Problems} }

   213 	\begin{spacing}{1.5}

   214 		\begin{itemize}

   215 			\item Different brackets have different meanings\\

   216 						{\small $u[n] \neq u(n)$\ldots in Math; but also in the source code}

   217 			\item Simplification, tricks and beauty\\

   218 						{\small $X\cdot(a+b)+Y\cdot(c+d)=aX+bX+cY+dY$}\\

   219 						{\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)=$}\\

   220 						{\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)$} $}

   221 		\end{itemize}

   222 	\end{spacing}

   223 \end{frame}

   224 

   225 \subsection{Demonstration}

   226 \begin{frame}

   227 	\frametitle{Demonstration of {\isac}}

   228 	\begin{spacing}{1.5}

   229 		\begin{itemize}

   230 			\item {\Large Development Environment} (Backend)

   231 			\vspace{15mm}

   232 			\item {\Large Math Assistant} (Frontend)

   233 		\end{itemize}

   234 	\end{spacing}

   235 \end{frame}

   236 

   237 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   238 \section{Summary}

   239 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   240 

   241 \subsection{Accomplished Work}

   242 \begin{frame}

   243 	\frametitle{Accomplished Work}

   244 	\begin{itemize}

   245       \item Partial Fractions\\ {\small Theorems, Specification, Program}

   246       \item Inverse Z-Transform with Partial Fractions\\ {\small Theorems, Specification, Program}

   247       \item Isabelle Theory indicating issues\\ {\small Preparation for {\sisac{}}-developers}

   248 	\end{itemize}

   249 \end{frame}

   250 

   251 \subsection{Partially Accomplished}

   252 \begin{frame}

   253 	\frametitle{Partially Accomplished}

   254 	\begin{spacing}{1.4}

   255 		\begin{itemize}

   256 	     \item Guidelines for Upcoming TP-Programmers\\

   257 	           {\small \textbf{Note:} Development environment and languages changes} 

   258 	     \item Examples

   259 		\end{itemize}

   260 	\end{spacing}

   261 \end{frame}

   262 

   263 \subsection{Not Accomplished}

   264 \begin{frame}

   265 	\frametitle{Not Accomplished}

   266 	\begin{spacing}{1.2}

   267 		\begin{itemize}

   268 	    \item Content of interactive course material\\

   269 	    			{\small Figures, Explanations,\ldots}

   270 	    \item A sufficient count of implementations

   271 	    \item No support of labs and lectures atm

   272 	    \item No material for \emph{STEOP} atm

   273 		\end{itemize}

   274 	\end{spacing}

   275 \end{frame}

   276 

   277 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   278 \section{Conclusion}

   279 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   280 

   281 \begin{frame}

   282 	\frametitle{Conclusion}

   283 	\begin{spacing}{1.2}

   284 	    \begin{itemize}

   285 				\item TP-based language not ready

   286 				\item Programming guideline not yet sufficient

   287 				\item Hope for usability in enginieering studies

   288 				\vspace{5mm}

   289 				\item Hard to spend 200h on 1 programm

   290 				\item \isac{} pointed at my own error

   291 			\end{itemize}

   292 		\end{spacing}

   293 \end{frame}

   294 

   295 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   296 \end{document}

   297 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   298 

   299 %% EOF
wneuper/isa