1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/doc-src/isac/jrocnik/jrocnik_cadgme.tex Sun Jun 17 22:36:27 2012 +0200
1.3 @@ -0,0 +1,265 @@
1.4 +\documentclass[%
1.5 +%handout, % prints handouts (=no animations, for printed version)
1.6 +%mathserif
1.7 +%xcolor=pst,
1.8 +14pt
1.9 +% fleqn
1.10 +]{beamer}
1.11 +
1.12 +\usepackage{beamerthemedefault}
1.13 +
1.14 +\usepackage{color}
1.15 +\definecolor{lgray}{RGB}{238,238,238}
1.16 +
1.17 +\useoutertheme[subsection=false]{smoothbars}
1.18 +\useinnertheme{circles}
1.19 +
1.20 +\setbeamercolor{block title}{fg=black,bg=gray}
1.21 +\setbeamercolor{block title alerted}{use=alerted text,fg=black,bg=alerted text.fg!75!bg}
1.22 +\setbeamercolor{block title example}{use=example text,fg=black,bg=example text.fg!75!bg}
1.23 +\setbeamercolor{block body}{parent=normal text,use=block title,bg=block title.bg!25!bg}
1.24 +\setbeamercolor{block body alerted}{parent=normal text,use=block title alerted,bg=block title alerted.bg!25!bg}
1.25 +\setbeamercolor{block body example}{parent=normal text,use=block title example,bg=block title example.bg!25!bg}
1.26 +
1.27 +%activate hyperlinks at the end
1.28 +%\usepackage{hyperref}
1.29 +
1.30 +\usepackage[english]{babel}
1.31 +\usepackage[utf8]{inputenc}
1.32 +\usepackage{array}
1.33 +\usepackage{setspace}
1.34 +\usepackage{url}
1.35 +
1.36 +\definecolor{tug}{rgb}{0.96862,0.14509,0.27450}
1.37 +
1.38 +\def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
1.39 +\def\sisac{{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}}
1.40 +
1.41 +\setbeamertemplate{headline}[text line]{
1.42 + \begin{beamercolorbox}[wd=\paperwidth,ht=8ex,dp=4ex]{}
1.43 + \insertnavigation{0.85\paperwidth}
1.44 + \raisebox{-10pt}{\includegraphics[width=15mm]{tuglogo}}\vskip2pt
1.45 + \hskip-1pt\rule{\paperwidth}{0.3pt}
1.46 + \end{beamercolorbox}
1.47 +}
1.48 +
1.49 +\setbeamertemplate{navigation symbols}{}
1.50 +
1.51 +\definecolor{gray}{rgb}{0.8,0.8,0.8}
1.52 +\setbeamercolor{footline}{fg=black,bg=gray}
1.53 +
1.54 +% Fusszeile mit Autor, Titel und Foliennummer / Gesamtfolienzahl
1.55 +\setbeamertemplate{footline}[text line]{
1.56 + \hskip-1pt
1.57 + \begin{beamercolorbox}[wd=\paperwidth]{footline}
1.58 + \rule{\paperwidth}{0.3pt}
1.59 + \colorbox{tug}{\rule{3pt}{0pt}\rule{0pt}{3pt}}
1.60 + \textbf{\rule{0pt}{5pt}\insertshortauthor\hfill\insertshortinstitute\hfill%
1.61 + \insertshorttitle\rule{1em}{0pt}}
1.62 + \rule{\paperwidth}{0.3pt}
1.63 + \end{beamercolorbox}
1.64 + \begin{beamercolorbox}[wd=\paperwidth,ht=2ex,dp=2ex]{white}
1.65 + \end{beamercolorbox}
1.66 +}%
1.67 +
1.68 +%% Titelblatt-Einstellungen
1.69 +\institute[IST]{Institute for Software Technology\\Graz University of Technology}
1.70 +\title[ISAC for Signal Processing]{Interactive Course Material by TP-based Programming}
1.71 +\subtitle{A Case Study}
1.72 +\author{Jan Ro\v{c}nik}
1.73 +\date{24. June 2012}
1.74 +
1.75 +% Subject and Keywords for PDF
1.76 +\subject{CADGME Presentation}
1.77 +\keywords{interactive course material, signal processing, z transform, TP-based programming
1.78 +language, Lucas-Interpreter, Theorem Proving}
1.79 +
1.80 +\titlegraphic{\includegraphics[width=20mm]{tuglogo}}
1.81 +
1.82 +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.83 +\begin{document}
1.84 +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.85 +
1.86 +\begin{frame}[plain]
1.87 + \frametitle{}
1.88 + \titlepage
1.89 +\end{frame}
1.90 +
1.91 +
1.92 +
1.93 +%\begin{frame}
1.94 +% \frametitle{Contents}
1.95 +% \begin{spacing}{0.3}
1.96 +% \tableofcontents[hideallsubsections %
1.97 +% % ,pausesections
1.98 +% ] % erzeugt Inhaltsverzeichnis
1.99 +% \end{spacing}
1.100 +%\end{frame}
1.101 +
1.102 +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.103 +\section{Introduction}
1.104 +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.105 +
1.106 +\subsection{isabelle}
1.107 +\begin{frame}
1.108 + \frametitle{What is Isabelle?}
1.109 + \begin{spacing}{1.5}
1.110 + \begin{itemize}
1.111 + \item Generic Proof Assistant
1.112 + \item Formula proofing in logical calculus
1.113 + \item Developed in Cambridge, Muenchen and Paris
1.114 + \end{itemize}
1.115 + \end{spacing}
1.116 +\end{frame}
1.117 +
1.118 +\subsection{isac}
1.119 +\begin{frame}
1.120 + \frametitle{What is {\isac}?}
1.121 + \begin{spacing}{1.5}
1.122 + \begin{itemize}
1.123 + \item \textcolor{tug}{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal A}$}belle for~{}\textcolor{tug}{${\cal C}$}alculations
1.124 + \item Interactive Course Material
1.125 + \item Learning Coach
1.126 + \item Developed at Austrian Universities
1.127 + \end{itemize}
1.128 + \end{spacing}
1.129 +\end{frame}
1.130 +
1.131 +\subsection{motivation}
1.132 +\begin{frame}
1.133 + \frametitle{Motivation - {\isac{}}'s~Potential}
1.134 + \begin{itemize}
1.135 + \item Stepwise solving of engineering problems\\
1.136 + {\small $\rightarrow$ \textcolor{tug}{Consistent Framework}}
1.137 + \item Explaining underlying knowledge\\
1.138 + {\small $\rightarrow$ \textcolor{tug}{Transparent Content, Access to Multimedia Content}}
1.139 + \item Checking steps input by the student\\
1.140 + {\small $\rightarrow$ \textcolor{tug}{Proof Situation}}
1.141 + \item Assessing stepwise problem solving\\
1.142 + {\small $\rightarrow$ \textcolor{tug}{One system for tutoring and assessment}}
1.143 + \end{itemize}
1.144 +\end{frame}
1.145 +
1.146 +
1.147 +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.148 +\section{Material Creation}
1.149 +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.150 +
1.151 +\begin{frame}
1.152 + \frametitle{Work flow}
1.153 + \begin{spacing}{1.8}
1.154 + \begin{itemize}
1.155 + \item Problem Analysis
1.156 + \item Information Collection
1.157 + \item \textbf{TP-Programming}
1.158 + \item Documentation
1.159 + \end{itemize}
1.160 + \end{spacing}
1.161 +\end{frame}
1.162 +
1.163 +\subsection{issues}
1.164 +\begin{frame}
1.165 + \frametitle{Issues to Accomplish I}
1.166 + \begin{spacing}{1.4}
1.167 + \begin{itemize}
1.168 + \item What knowledge is mechanized in Isabelle?\\
1.169 + {\small How about new?}
1.170 + \item What problems are implemented in {\sisac{}}?\\
1.171 + {\small How about new?}
1.172 + \item What is the effort?
1.173 + \end{itemize}
1.174 + \end{spacing}
1.175 +\end{frame}
1.176 +
1.177 +\begin{frame}
1.178 + \frametitle{Issues to Accomplish II}
1.179 +\begin{spacing}{1.4}
1.180 +\begin{itemize}
1.181 + \item How look calculations like?\\
1.182 + {\small Ansatzs, Subproblems?}
1.183 + \item How are problems specified?\\
1.184 + {\small Given, Pre-/Postcondition, Find?}
1.185 + \item What is the contents of the interactive course material?\\
1.186 + {\small Figures, Explanations,\ldots}
1.187 +\end{itemize}
1.188 +\end{spacing}
1.189 +\end{frame}
1.190 +
1.191 +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.192 +\section{Details}
1.193 +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.194 +
1.195 +\subsection{Technical Survey}
1.196 +\begin{frame}
1.197 + \frametitle{Technical Survey I {\normalsize Mechanizing Knowledge}}
1.198 + \begin{spacing}{1.5}
1.199 + \begin{itemize}
1.200 + \item Not enough knowledge is mechanized\\
1.201 + {\small Equation Solving, Integrals,\ldots}
1.202 + \item Computer Mathematicians required!\\
1.203 + {\small Mathematics: Equation solving, Engineer: Z-Transform}
1.204 + \item RISC Linz, Mathematics TU Graz
1.205 + \end{itemize}
1.206 + \end{spacing}
1.207 +\end{frame}
1.208 +
1.209 +\begin{frame}
1.210 + \frametitle{Technical Survey II {\normalsize Notation Problems} }
1.211 + \begin{spacing}{1.5}
1.212 + \begin{itemize}
1.213 + \item Different brackets have different meanings\\
1.214 + {\small $u[n] \neq u(n)$\ldots in Math; but also in the source code}
1.215 + \item Simplification, tricks and beauty\\
1.216 + {\small $X\cdot(a+b)+Y\cdot(c+d)=aX+bX+cY+dY$}\\
1.217 + {\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)=$}\\
1.218 + {\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)$} $}
1.219 + \end{itemize}
1.220 + \end{spacing}
1.221 +\end{frame}
1.222 +
1.223 +\subsection{Demonstration}
1.224 +\begin{frame}
1.225 + \frametitle{Demonstration of {\isac}}
1.226 + \begin{spacing}{1.5}
1.227 + \begin{itemize}
1.228 + \item TODO
1.229 + \end{itemize}
1.230 + \end{spacing}
1.231 +\end{frame}
1.232 +
1.233 +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.234 +\section{Summary}
1.235 +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.236 +
1.237 +\begin{frame}
1.238 + \frametitle{Conclusion}
1.239 + \begin{spacing}{1.2}
1.240 + \begin{itemize}
1.241 + \item TP-based language not ready
1.242 + \item Programming guideline not yet sufficient
1.243 + \item Hope for usability in enginieering studies
1.244 + \vspace{5mm}
1.245 + \item Hard to spend 200h on 1 programm
1.246 + \item \isac{} pointed at my own error
1.247 + \end{itemize}
1.248 + \end{spacing}
1.249 +\end{frame}
1.250 +
1.251 +
1.252 +\begin{frame}
1.253 + \frametitle{Contact}
1.254 + \begin{spacing}{1.2}
1.255 + \begin{itemize}
1.256 + \item Isabelle \href{isabelle.in.tum.de}{isabelle.in.tum.de}
1.257 + \item The {\sisac}-Project: \href{www.ist.tugraz.at/isac}{www.ist.tugraz.at/isac}
1.258 + \item Projectleader: \href{mailto:neuper@ist.tugraz.at}{neuper@ist.tugraz.at}
1.259 + \item Jan Rocnik: \href{mailto:jan.rocnik@student.tugraz.at}{jan.rocnik@student.tugraz.at}
1.260 + \end{itemize}
1.261 + \end{spacing}
1.262 +\end{frame}
1.263 +
1.264 +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.265 +\end{document}
1.266 +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.267 +
1.268 +%% EOF
1.269 \ No newline at end of file