Mercurial Mercurial > wneuper > isa / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
doc-src/isac/jrocnik/jrocnik_present2.tex
author Jan Rocnik <jan.rocnik@student.tugraz.at>
Sun, 06 May 2012 16:13:11 +0200
changeset 42418 3f8317297717
parent 42403 b7ffe4adf05c
child 42420 5e4e8a93c12a
permissions -rwxr-xr-x
tuned present-2 
     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 \useoutertheme[subsection=false]{smoothbars}

    12 \useinnertheme{circles}

    13 

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

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

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

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

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

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

    20 

    21 %activate hyperlinks at the end

    22 %\usepackage{hyperref}

    23 

    24 \usepackage[english]{babel}

    25 \usepackage[utf8]{inputenc}

    26 \usepackage{array}

    27 \usepackage{setspace}

    28 

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

    30 

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

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

    33 

    34 \setbeamertemplate{headline}[text line]{

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

    36 		\insertnavigation{0.85\paperwidth} 

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

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

    39 	\end{beamercolorbox}

    40 }

    41 

    42 \setbeamertemplate{navigation symbols}{}

    43 

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

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

    46 

    47 % Fusszeile mit Autor, Titel und Foliennummer / Gesamtfolienzahl

    48 \setbeamertemplate{footline}[text line]{

    49 	\hskip-1pt

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

    51 			\rule{\paperwidth}{0.3pt}

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

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

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

    55 			\rule{\paperwidth}{0.3pt}

    56 	\end{beamercolorbox}

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

    58 	\end{beamercolorbox}

    59 }%

    60 

    61 %% Titelblatt-Einstellungen

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

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

    64 \subtitle{Baccalaureate Thesis}

    65 \author{Jan Rocnik}

    66 \date{\today}

    67 

    68 % Subject and Keywords for PDF

    69 \subject{Final presentation of Baccalaureate Thesis}

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

    71 

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

    73 

    74 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    75 \begin{document}

    76 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    77 

    78 \begin{frame}[plain]

    79   \frametitle{}

    80   \titlepage

    81 \end{frame}

    82 

    83 

    84 

    85 \begin{frame}

    86   \frametitle{Contents}

    87   \begin{spacing}{0.3}

    88         \tableofcontents[hideallsubsections %

    89                         % ,pausesections

    90                         ] % erzeugt Inhaltsverzeichnis

    91   \end{spacing}

    92 \end{frame}

    93 

    94 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    95 \section{Introduction}

    96 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    97 

    98 \subsection{isabelle}

    99 \begin{frame}

   100 	\frametitle{What is Isabelle?}

   101 	\begin{spacing}{1.5}

   102 		\begin{itemize}

   103 			\item Generic Proof Assistant

   104 			\item Formula proofing in logical calculus

   105 			\item Developed in Cambridge, Muenchen and Paris

   106 		\end{itemize}

   107 	\end{spacing}

   108 \end{frame}

   109 

   110 \subsection{isac}

   111 \begin{frame}

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

   113 	\begin{spacing}{1.5}

   114 		\begin{itemize}

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

   116 			\item Interactive Course Material

   117 			\item Learning Coach

   118 			\item Developed at TU Graz

   119 		\end{itemize}

   120 	\end{spacing}

   121 \end{frame}

   122 

   123 \subsection{motivation}

   124 \begin{frame}

   125 	\frametitle{Motivation - {\isac{}}~Assessing Advances}

   126 	\begin{itemize}

   127 		\item Stepwise solving engineering problems\\

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

   129 		\item Explaining underlying knowledge\\

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

   131 		\item Checking steps input by the student\\

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

   133 		\item Assessing stepwise problem solving\\

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

   135 	\end{itemize}

   136 \end{frame}

   137 

   138 

   139 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   140 \section{Thesis Definition}

   141 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   142 

   143 \begin{frame}

   144 	\frametitle{Thesis Definition}

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

   146 	\begin{spacing}{1.2}

   147 		\begin{itemize}

   148 			\item Creation of interactive course material\\

   149 						{\small Based on given tasks}

   150 			\item Content should be usable\ldots

   151 			\begin{itemize}

   152 				\item at specific lectures

   153 				\item for \emph{STEOP}

   154 			\end{itemize}

   155 			\item Guideline for upcoming TP-Programmers.

   156 			\item Feedback of usability\\

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

   158 		\end{itemize}

   159 	\end{spacing}

   160 \end{frame}

   161 

   162 \subsection{issues}

   163 \begin{frame}

   164 	\frametitle{Issues to Accomplish I}

   165 	\begin{spacing}{1.4}

   166 		\begin{itemize}

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

   168 						{\small How about new?}

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

   170 						{\small How about new?}

   171 			\item What is the effort?

   172 		\end{itemize}

   173 	\end{spacing}

   174 \end{frame}

   175 

   176 \begin{frame}

   177 	\frametitle{Issues to Accomplish II}

   178 \begin{spacing}{1.4}

   179 \begin{itemize}

   180 	\item How look calculations like?\\

   181 				{\small Ansatzs, Subproblems?}

   182 	\item How are problems specified?\\

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

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

   185 				{\small Figures, Explanations,\ldots}

   186 \end{itemize}

   187 \end{spacing}

   188 \end{frame}

   189 

   190 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   191 \section{Details}

   192 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   193 

   194 \subsection{Technical Survey}

   195 \begin{frame}

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

   197 	\begin{spacing}{1.5}

   198 		\begin{itemize}

   199 			\item Not enough knowledge is mechanized\\

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

   201 			\item Problems on mechanization\\

   202 						{\small Mathematical (Knowledge), Technical (Documentation)}

   203 			\item Biggest task is finding manpower

   204 		\end{itemize}

   205 	\end{spacing}

   206 \end{frame}

   207 

   208 \begin{frame}

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

   210 	\begin{spacing}{1.5}

   211 		\begin{itemize}

   212 			\item Different brackets have different meanings\\

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

   214 			\item Operators are already in use

   215 			\item Tricks on similarisation and beauty\\

   216 						{\small Different similarisations for different purpose}

   217 		\end{itemize}

   218 	\end{spacing}

   219 \end{frame}

   220 

   221 \subsection{Demonstration}

   222 \begin{frame}

   223 	\frametitle{Demonstration of {\isac}}

   224 	\begin{spacing}{1.5}

   225 		\begin{itemize}

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

   227 			\vspace{15mm}

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

   229 		\end{itemize}

   230 	\end{spacing}

   231 \end{frame}

   232 

   233 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   234 \section{Summary}

   235 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   236 

   237 \subsection{Accomplished Work}

   238 \begin{frame}

   239 	\frametitle{Accomplished Work}

   240 	\begin{itemize}

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

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

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

   244 	\end{itemize}

   245 \end{frame}

   246 

   247 \subsection{Partially Accomplished}

   248 \begin{frame}

   249 	\frametitle{Partially Accomplished}

   250 	\begin{spacing}{1.4}

   251 		\begin{itemize}

   252 	     \item Guidelines for Upcoming TP-Programmers\\

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

   254 	     \item Examples

   255 		\end{itemize}

   256 	\end{spacing}

   257 \end{frame}

   258 

   259 \subsection{Not Accomplished}

   260 \begin{frame}

   261 	\frametitle{Not Accomplished}

   262 	\begin{spacing}{1.2}

   263 		\begin{itemize}

   264 	    \item Content of interactive course material\\

   265 	    			{\small Figures, Explanations,\ldots}

   266 	    \item A sufficient count of implementations

   267 	    \item No support of labs and lectures atm

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

   269 		\end{itemize}

   270 	\end{spacing}

   271 \end{frame}

   272 

   273 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   274 \section{Conclusion}

   275 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   276 

   277 \begin{frame}

   278 	\frametitle{Conclusion}

   279 	\begin{spacing}{1.2}

   280 	    \begin{itemize}

   281 				\item TP-Programming language not ready

   282 				\item Not well documented

   283 				\item Gorgeous idea but still a long way

   284 				\vspace{5mm}

   285 				\item Hard to get familiar

   286 				\item Found mistakes in own work

   287 			\end{itemize}

   288 		\end{spacing}

   289 \end{frame}

   290 

   291 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   292 \end{document}

   293 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   294 

   295 %% EOF
wneuper/isa