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>
Thu, 21 Jun 2012 20:48:36 +0200
changeset 42444 2768aa42a383
parent 42442 d44ba224ceb0
child 42461 94c9a0735e2f
permissions -rwxr-xr-x
tuned 
     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 \definecolor{gray}{rgb}{0.8,0.8,0.8}

    14 

    15 \useoutertheme[subsection=false]{smoothbars}

    16 %\useinnertheme{circles}

    17 

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

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

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

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

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

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

    24 

    25 %activate hyperlinks at the end

    26 %\usepackage{hyperref}

    27 

    28 \usepackage[english]{babel}

    29 \usepackage[utf8]{inputenc}

    30 \usepackage{array}

    31 \usepackage{setspace}

    32 \usepackage{url}

    33 

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

    35 

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

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

    38 

    39 \setbeamertemplate{headline}[text line]{

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

    41 		\insertnavigation{0.85\paperwidth} 

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

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

    44 	\end{beamercolorbox}

    45 }

    46 

    47 \setbeamertemplate{navigation symbols}{}

    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]{Institute for Software Technology\\Graz University of Technology}

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

    67 \subtitle{A Case Study}

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

    69 \date{24. June 2012}

    70 

    71 % Subject and Keywords for PDF

    72 \subject{CADGME Presentation}

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

    74 language, Lucas-Interpreter, Theorem Proving}

    75 

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

    77 

    78 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    79 \begin{document}

    80 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    81 

    82 \begin{frame}[plain]

    83   \frametitle{}

    84   \titlepage

    85 \end{frame}

    86 

    87 

    88 

    89 %\begin{frame}

    90 %  \frametitle{Contents}

    91 %  \begin{spacing}{0.3}

    92 %        \tableofcontents[hideallsubsections %

    93 %                        % ,pausesections

    94 %                        ] % erzeugt Inhaltsverzeichnis

    95 %  \end{spacing}

    96 %\end{frame}

    97 

    98 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    99 \section{Introduction}

   100 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   101 

   102 \subsection{isabelle}

   103 \begin{frame}

   104 	\frametitle{What is Isabelle?}

   105 	\begin{spacing}{2}

   106 		\begin{itemize}

   107 			\item Generic Proof Assistant

   108 			\item Formula proofing in logical calculus

   109 			\item Developed in Cambridge, Muenchen and Paris

   110 		\end{itemize}

   111 	\end{spacing}

   112 \end{frame}

   113 

   114 \subsection{isac}

   115 \begin{frame}

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

   117 	\begin{spacing}{1.7}

   118 		\begin{itemize}

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

   120 			\item Interactive Course Material

   121 			\item Learning Coach

   122 			\item Developed at Austrian Universities

   123 		\end{itemize}

   124 	\end{spacing}

   125 \end{frame}

   126 

   127 \subsection{motivation}

   128 \begin{frame}

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

   130 	\begin{itemize}

   131 		\item Stepwise solving of engineering problems\\

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

   133 		\item Explaining underlying knowledge\\

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

   135 		\item Checking steps input by the student\\

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

   137 		\item Assessing stepwise problem solving\\

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

   139 	\end{itemize}

   140 \end{frame}

   141 

   142 

   143 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   144 \section{Material Creation}

   145 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   146 

   147 \begin{frame}

   148 	\frametitle{Course Material Creation {\normalsize Iterations}} %tasks? work flow?

   149 	\begin{spacing}{1.3}

   150 		\begin{enumerate}

   151 			\item Problem Analysis\\

   152 				{\small Calculation possiblities, Featured Steps} %example partial fractions

   153 			\item Information Collection\\

   154 				{\small Possiblies and Challanges in {\sisac{}}}

   155 			\item \textbf{TP-Programming}			

   156 			\item Documentation\\

   157 				{\small Representation of underlying knowledge in the system}

   158 		\end{enumerate}

   159 	\end{spacing}

   160 \end{frame}

   161 

   162 \subsection{issues}

   163 \begin{frame}

   164 	\frametitle{Issues to Accomplish {\normalsize Information Collection}}

   165 	\begin{spacing}{1.3}

   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 contents of the interactive course material?\\

   172 				{\small Figures, Explanations,\ldots}

   173 		\end{itemize}

   174 	\end{spacing}

   175 \end{frame}

   176 

   177 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   178 \section{Details}

   179 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   180 

   181 \subsection{Technical Survey}

   182 \begin{frame}

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

   184 	\begin{spacing}{1.5}

   185 		\begin{itemize}

   186 			\item Not enough knowledge is mechanized\\

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

   188 			\item Computer Mathematicians required!\\

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

   190 			\item RISC Linz, Mathematics TU Graz

   191 		\end{itemize}

   192 	\end{spacing}

   193 \end{frame}

   194 

   195 \begin{frame}

   196 	\frametitle{Technical Survey II {\normalsize Representation Problems} }

   197 	\begin{spacing}{1.9}

   198 		\begin{itemize}

   199 			\item Different brackets have different meanings\\

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

   201 			\item We need Symbols, Indizes and Hochzahlen

   202 			\item Different Representations for different purpos %winkel in polar oder kartesischen koordinaten usw.

   203 		\end{itemize}

   204 	\end{spacing}

   205 \end{frame}

   206 

   207 \begin{frame}

   208 	\frametitle{Technical Survey III {\normalsize Notation Problems} }

   209 	\begin{spacing}{1.8}

   210 		\begin{center}

   211 			Simplification, tricks and beauty\\

   212 			  \vspace{7mm}

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

   214 				\vspace{3mm}

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

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

   217 		\end{center}

   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 Frontend - {\small The shiny side\ldots}

   227 			\item Backend - {\small The dark side\ldots}

   228 			\begin{itemize}

   229 				\item Equation solving

   230 				\item Notation problems, Working with Rulesets

   231 				\item Framework expansion

   232 				\item My Work

   233 			\end{itemize}

   234 		\end{itemize}

   235 	\end{spacing}

   236 \end{frame}

   237 

   238 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   239 \section{Summary}

   240 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   241 

   242 \subsection{conclusion}

   243 \begin{frame}

   244 	\frametitle{Conclusion}

   245 	\begin{spacing}{1.2}

   246 	    \begin{itemize}

   247 				\item TP-based language not ready

   248 				\item Programming guideline not yet sufficient

   249 				\item Hope for usability in enginieering studies

   250 				\item Wide range of interested people

   251 				\vspace{5mm}

   252 				\item Hard to spend 200h on 1 programm

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

   254 			\end{itemize}

   255 		\end{spacing}

   256 \end{frame}

   257 

   258 \subsection{contact}

   259 \begin{frame}

   260 	\frametitle{Contact}

   261 	\begin{spacing}{1.7}

   262 	    \begin{tabular}{lr}

   263 				Isabelle & \small \texttt{\href{isabelle.in.tum.de}{isabelle.in.tum.de}}\\

   264 				The {\isac}-Project & \small \texttt{\href{www.ist.tugraz.at/isac}{www.ist.tugraz.at/isac}}\\

   265 				Projectleader & \small \texttt{\href{mailto:neuper@ist.tugraz.at}{neuper@ist.tugraz.at}}\\

   266 				Jan Rocnik & \small \texttt{\href{mailto:jan.rocnik@student.tugraz.at}{jan.rocnik@student.tugraz.at}}

   267 			\end{tabular}

   268 		\end{spacing}

   269 \end{frame}

   270 

   271 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   272 \end{document}

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

   274 

   275 %% EOF
wneuper/isa