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_cadgme.tex
author Jan Rocnik <jan.rocnik@student.tugraz.at>
Sun, 17 Jun 2012 22:36:27 +0200
changeset 42442 d44ba224ceb0
child 42444 2768aa42a383
permissions -rwxr-xr-x
added first version of cadgme presentation 
     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 \usepackage{url}

    32 

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

    34 

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

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

    37 

    38 \setbeamertemplate{headline}[text line]{

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

    40 		\insertnavigation{0.85\paperwidth} 

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

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

    43 	\end{beamercolorbox}

    44 }

    45 

    46 \setbeamertemplate{navigation symbols}{}

    47 

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

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

    50 

    51 % Fusszeile mit Autor, Titel und Foliennummer / Gesamtfolienzahl

    52 \setbeamertemplate{footline}[text line]{

    53 	\hskip-1pt

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

    55 			\rule{\paperwidth}{0.3pt}

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

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

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

    59 			\rule{\paperwidth}{0.3pt}

    60 	\end{beamercolorbox}

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

    62 	\end{beamercolorbox}

    63 }%

    64 

    65 %% Titelblatt-Einstellungen

    66 \institute[IST]{Institute for Software Technology\\Graz University of Technology}

    67 \title[ISAC for Signal Processing]{Interactive Course Material by TP-based Programming}

    68 \subtitle{A Case Study}

    69 \author{Jan Ro\v{c}nik}

    70 \date{24. June 2012}

    71 

    72 % Subject and Keywords for PDF

    73 \subject{CADGME Presentation}

    74 \keywords{interactive course material, signal processing, z transform, TP-based programming

    75 language, Lucas-Interpreter, Theorem Proving}

    76 

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

    78 

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

    80 \begin{document}

    81 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    82 

    83 \begin{frame}[plain]

    84   \frametitle{}

    85   \titlepage

    86 \end{frame}

    87 

    88 

    89 

    90 %\begin{frame}

    91 %  \frametitle{Contents}

    92 %  \begin{spacing}{0.3}

    93 %        \tableofcontents[hideallsubsections %

    94 %                        % ,pausesections

    95 %                        ] % erzeugt Inhaltsverzeichnis

    96 %  \end{spacing}

    97 %\end{frame}

    98 

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

   100 \section{Introduction}

   101 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   102 

   103 \subsection{isabelle}

   104 \begin{frame}

   105 	\frametitle{What is Isabelle?}

   106 	\begin{spacing}{1.5}

   107 		\begin{itemize}

   108 			\item Generic Proof Assistant

   109 			\item Formula proofing in logical calculus

   110 			\item Developed in Cambridge, Muenchen and Paris

   111 		\end{itemize}

   112 	\end{spacing}

   113 \end{frame}

   114 

   115 \subsection{isac}

   116 \begin{frame}

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

   118 	\begin{spacing}{1.5}

   119 		\begin{itemize}

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

   121 			\item Interactive Course Material

   122 			\item Learning Coach

   123 			\item Developed at Austrian Universities

   124 		\end{itemize}

   125 	\end{spacing}

   126 \end{frame}

   127 

   128 \subsection{motivation}

   129 \begin{frame}

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

   131 	\begin{itemize}

   132 		\item Stepwise solving of engineering problems\\

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

   134 		\item Explaining underlying knowledge\\

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

   136 		\item Checking steps input by the student\\

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

   138 		\item Assessing stepwise problem solving\\

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

   140 	\end{itemize}

   141 \end{frame}

   142 

   143 

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

   145 \section{Material Creation}

   146 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   147 

   148 \begin{frame}

   149 	\frametitle{Work flow}

   150 	\begin{spacing}{1.8}

   151 		\begin{itemize}

   152 			\item Problem Analysis

   153 			\item Information Collection

   154 			\item \textbf{TP-Programming}

   155 			\item Documentation

   156 		\end{itemize}

   157 	\end{spacing}

   158 \end{frame}

   159 

   160 \subsection{issues}

   161 \begin{frame}

   162 	\frametitle{Issues to Accomplish I}

   163 	\begin{spacing}{1.4}

   164 		\begin{itemize}

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

   166 						{\small How about new?}

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

   168 						{\small How about new?}

   169 			\item What is the effort?

   170 		\end{itemize}

   171 	\end{spacing}

   172 \end{frame}

   173 

   174 \begin{frame}

   175 	\frametitle{Issues to Accomplish II}

   176 \begin{spacing}{1.4}

   177 \begin{itemize}

   178 	\item How look calculations like?\\

   179 				{\small Ansatzs, Subproblems?}

   180 	\item How are problems specified?\\

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

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

   183 				{\small Figures, Explanations,\ldots}

   184 \end{itemize}

   185 \end{spacing}

   186 \end{frame}

   187 

   188 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   189 \section{Details}

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

   191 

   192 \subsection{Technical Survey}

   193 \begin{frame}

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

   195 	\begin{spacing}{1.5}

   196 		\begin{itemize}

   197 			\item Not enough knowledge is mechanized\\

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

   199 			\item Computer Mathematicians required!\\

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

   201 			\item RISC Linz, Mathematics TU Graz

   202 		\end{itemize}

   203 	\end{spacing}

   204 \end{frame}

   205 

   206 \begin{frame}

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

   208 	\begin{spacing}{1.5}

   209 		\begin{itemize}

   210 			\item Different brackets have different meanings\\

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

   212 			\item Simplification, tricks and beauty\\

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

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

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

   216 		\end{itemize}

   217 	\end{spacing}

   218 \end{frame}

   219 

   220 \subsection{Demonstration}

   221 \begin{frame}

   222 	\frametitle{Demonstration of {\isac}}

   223 	\begin{spacing}{1.5}

   224 		\begin{itemize}

   225 			\item TODO

   226 		\end{itemize}

   227 	\end{spacing}

   228 \end{frame}

   229 

   230 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   231 \section{Summary}

   232 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   233 

   234 \begin{frame}

   235 	\frametitle{Conclusion}

   236 	\begin{spacing}{1.2}

   237 	    \begin{itemize}

   238 				\item TP-based language not ready

   239 				\item Programming guideline not yet sufficient

   240 				\item Hope for usability in enginieering studies

   241 				\vspace{5mm}

   242 				\item Hard to spend 200h on 1 programm

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

   244 			\end{itemize}

   245 		\end{spacing}

   246 \end{frame}

   247 

   248 

   249 \begin{frame}

   250 	\frametitle{Contact}

   251 	\begin{spacing}{1.2}

   252 	    \begin{itemize}

   253 				\item Isabelle \href{isabelle.in.tum.de}{isabelle.in.tum.de}

   254 				\item The {\sisac}-Project: \href{www.ist.tugraz.at/isac}{www.ist.tugraz.at/isac}

   255 				\item Projectleader: \href{mailto:neuper@ist.tugraz.at}{neuper@ist.tugraz.at}

   256 				\item Jan Rocnik: \href{mailto:jan.rocnik@student.tugraz.at}{jan.rocnik@student.tugraz.at}

   257 			\end{itemize}

   258 		\end{spacing}

   259 \end{frame}

   260 

   261 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   262 \end{document}

   263 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   264 

   265 %% EOF
wneuper/isa