
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




