diff -r 7f3760f39bdc -r f8845fc8f38d src/Doc/isac/jrocnik/jrocnik_cadgme.tex --- a/src/Doc/isac/jrocnik/jrocnik_cadgme.tex Mon Sep 16 12:27:20 2013 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,281 +0,0 @@ -\documentclass[% -%handout, % prints handouts (=no animations, for printed version) -%mathserif -%xcolor=pst, -14pt -% fleqn -]{beamer} - -\usepackage{beamerthemedefault} - -\usepackage{color} -\definecolor{lgray}{RGB}{238,238,238} -\definecolor{gray}{rgb}{0.8,0.8,0.8} - -\useoutertheme[subsection=false]{smoothbars} -%\useinnertheme{circles} - -\setbeamercolor{block title}{fg=black,bg=gray} -\setbeamercolor{block title alerted}{use=alerted text,fg=black,bg=alerted text.fg!75!bg} -\setbeamercolor{block title example}{use=example text,fg=black,bg=example text.fg!75!bg} -\setbeamercolor{block body}{parent=normal text,use=block title,bg=block title.bg!25!bg} -\setbeamercolor{block body alerted}{parent=normal text,use=block title alerted,bg=block title alerted.bg!25!bg} -\setbeamercolor{block body example}{parent=normal text,use=block title example,bg=block title example.bg!25!bg} - -%activate hyperlinks at the end -%\usepackage{hyperref} - -\usepackage[english]{babel} -\usepackage[utf8]{inputenc} -\usepackage{array} -\usepackage{setspace} -\usepackage{url} - -\definecolor{tug}{rgb}{0.96862,0.14509,0.27450} - -\def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$} -\def\sisac{{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}} - -\setbeamertemplate{headline}[text line]{ - \begin{beamercolorbox}[wd=\paperwidth,ht=8ex,dp=4ex]{} - \insertnavigation{0.85\paperwidth} - \raisebox{-10pt}{\includegraphics[width=15mm]{tuglogo}}\vskip2pt - \hskip-1pt\rule{\paperwidth}{0.3pt} - \end{beamercolorbox} -} - -\setbeamertemplate{navigation symbols}{} -\setbeamercolor{footline}{fg=black,bg=gray} - -% Fusszeile mit Autor, Titel und Foliennummer / Gesamtfolienzahl -\setbeamertemplate{footline}[text line]{ - \hskip-1pt - \begin{beamercolorbox}[wd=\paperwidth]{footline} - \rule{\paperwidth}{0.3pt} - \colorbox{tug}{\rule{3pt}{0pt}\rule{0pt}{3pt}} - \textbf{\rule{0pt}{5pt}\insertshortauthor\hfill\insertshortinstitute\hfill% - \insertshorttitle\rule{1em}{0pt}} - \rule{\paperwidth}{0.3pt} - \end{beamercolorbox} - \begin{beamercolorbox}[wd=\paperwidth,ht=2ex,dp=2ex]{white} - \end{beamercolorbox} -}% - -%% Titelblatt-Einstellungen -\institute[IST]{Institute for Software Technology\\Graz University of Technology} -\title[ISAC for Signal Processing]{Interactive Course Material by TP-based Programming} -\subtitle{A Case Study} -\author{Jan Ro\v{c}nik} -\date{24. June 2012} - -% Subject and Keywords for PDF -\subject{CADGME Presentation} -\keywords{interactive course material, signal processing, z transform, TP-based programming -language, Lucas-Interpreter, Theorem Proving} - -\titlegraphic{\includegraphics[width=20mm]{tuglogo}} - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\begin{document} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -\begin{frame}[plain] - \frametitle{} - \titlepage -\end{frame} - - - -%\begin{frame} -% \frametitle{Contents} -% \begin{spacing}{0.3} -% \tableofcontents[hideallsubsections % -% % ,pausesections -% ] % erzeugt Inhaltsverzeichnis -% \end{spacing} -%\end{frame} - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\section{Introduction} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -\subsection{isabelle} -\begin{frame} - \frametitle{What is Isabelle?} - \begin{spacing}{2} - \begin{itemize} - \item Interactive Theorem Prover (Interactice TP) - \item Large body of mechanized math knowledge - \item Developed in Cambridge, Munich and Paris - \end{itemize} - \end{spacing} -\end{frame} - -\subsection{isac} -\begin{frame} - \frametitle{What is {\isac}?} - \begin{spacing}{1.7} - \begin{itemize} - \item \textcolor{tug}{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal A}$}belle for~{}\textcolor{tug}{${\cal C}$}alculations - \item Interactive Course Material - \item Learning Coach - \item Developed at Austrian Universities - \end{itemize} - \end{spacing} -\end{frame} - -\subsection{motivation} -\begin{frame} - \frametitle{{\isac{}} for Interactive Course Material} - \begin{itemize} - \item Stepwise solving of engineering problems\\ - {\small $\rightarrow$ \textcolor{tug}{One Framework for all phases of problem solving}} - \item Explaining underlying knowledge\\ - {\small $\rightarrow$ \textcolor{tug}{Transparent Content, Access to Multimedia Content}} - \item Checking steps input by the student\\ - {\small $\rightarrow$ \textcolor{tug}{Proof Situation}} - \item Assessing stepwise problem solving\\ - {\small $\rightarrow$ \textcolor{tug}{One system for tutoring and assessment}} - \end{itemize} -\end{frame} - - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\section{Material Creation} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -\subsection{steps} -\begin{frame} - \frametitle{Course Material Creation {\normalsize Iterations}} %tasks? work flow? - \begin{spacing}{1.3} - \begin{enumerate} - \item Problem Analysis\\ - {\small Variants of problem solving steps} %example partial fractions - \item \textbf{Analysis of mechanized knowledge}\\ - {\small Existing and missing knowledge} - \item \textbf{Programming in a TP based language (TP-PL)} - \item Additional Content\\ - {\small Multimedia explanations for underlying knowledge} - \end{enumerate} - \end{spacing} -\end{frame} - -\subsection{issues} -\begin{frame} - \frametitle{Issues to Accomplish {\normalsize Information Collection}} - \begin{spacing}{1.3} - \begin{itemize} - \item What knowledge is mechanized in Isabelle?\\ - {\small Theorems, Definitions, Numbers,\ldots} - \item What knowledge is mechanized in {\isac{}}?\\ - {\small Problem specifications, Programs,\ldots} - \item What additional explanations are required?\\ - {\small Figures, Examples,\ldots} - \end{itemize} - \end{spacing} -\end{frame} - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\section{Details} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -\subsection{Technical Survey} -%\begin{frame} -% \frametitle{Technical Survey I {\normalsize Mechanizing Knowledge}} -% \begin{spacing}{1.5} -% \begin{itemize} -% \item Not enough knowledge is mechanized\\ -% {\small Equation Solving, Integrals,\ldots} -% \item Computer Mathematicians required!\\ -% {\small Mathematics: Equation solving, Engineer: Z-Transform} -% \item RISC Linz, Mathematics TU Graz -% \end{itemize} -% \end{spacing} -%\end{frame} - -%\begin{frame} -% \frametitle{Technical Survey II {\normalsize Representation Problems} } -% \begin{spacing}{1.9} -% \begin{itemize} -% \item Different brackets have different meanings\\ -% {\small $u[n]$ is a specific function application :) } -% \item We need Symbols, Indizes and Hochzahlen -% \item Different Representations for different purpos %winkel in polar oder kartesischen koordinaten usw. -% \end{itemize} -% \end{spacing} -%\end{frame} - -\begin{frame} - \frametitle{Representation Problems} - \begin{spacing}{1.4} - \begin{center} - - \begin{itemize} - \item Can meaning of symbols be varied?\\ - {\small $u[n]$ is a specific function in Signal Processing} - \item Simplification, tricks and beauty - \end{itemize} - - {\small $X\cdot(a+b)+Y\cdot(c+d)=aX+bX+cY+dY$}\\ - \vspace{3mm} - {\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)=$}\\ - {\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)$} $} - - - \end{center} - \end{spacing} -\end{frame} - -\subsection{Demonstration} -\begin{frame} - \frametitle{Demonstration} - \begin{spacing}{1.5} - \begin{itemize} - \item Backend - \begin{itemize} - \item Equation solving - \item Notation problems, Working with Rulesets - \item Framework expansion - \item My Work - \end{itemize} - \end{itemize} - \end{spacing} -\end{frame} - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\section{Summary} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -\subsection{conclusion} -\begin{frame} - \frametitle{Conclusion} - \begin{spacing}{1.2} - \begin{itemize} - \item Proof of concept for TP-PL succesfull - \item Usability of TP-PL not sufficient - \item Requirements for improved usability clarified - \vspace{5mm} - \item Unacceptable to spend 200h on 1 program - \item \isac{} pointed at my own error - \end{itemize} - \end{spacing} -\end{frame} - -\subsection{contact} -\begin{frame} - \frametitle{Contact} - \begin{spacing}{1.7} - \begin{tabular}{lr} - Isabelle & \small \texttt{\href{isabelle.in.tum.de}{isabelle.in.tum.de}}\\ - The {\isac}-Project & \small \texttt{\href{www.ist.tugraz.at/isac}{www.ist.tugraz.at/isac}}\\ - Project leader & \small \texttt{\href{mailto:wneuper@ist.tugraz.at}{wneuper@ist.tugraz.at}}\\ - Jan Rocnik & \small \texttt{\href{mailto:jan.rocnik@student.tugraz.at}{jan.rocnik@student.tugraz.at}} - \end{tabular} - \end{spacing} -\end{frame} - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\end{document} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -%% EOF \ No newline at end of file