
diff -r 2768aa42a383 -r 94c9a0735e2f doc-src/isac/jrocnik/jrocnik_cadgme.tex
--- a/doc-src/isac/jrocnik/jrocnik_cadgme.tex	Thu Jun 21 20:48:36 2012 +0200
+++ b/doc-src/isac/jrocnik/jrocnik_cadgme.tex	Fri Aug 31 19:19:07 2012 +0200
@@ -104,9 +104,9 @@
 	\frametitle{What is Isabelle?}
 	\begin{spacing}{2}
 		\begin{itemize}
-			\item Generic Proof Assistant
-			\item Formula proofing in logical calculus
-			\item Developed in Cambridge, Muenchen and Paris
+			\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}
@@ -126,10 +126,10 @@
 
 \subsection{motivation}
 \begin{frame}
-	\frametitle{Motivation - {\isac{}}'s~Potential}
+	\frametitle{{\isac{}} for Interactive Course Material}
 	\begin{itemize}
 		\item Stepwise solving of engineering problems\\
-					{\small $\rightarrow$ \textcolor{tug}{Consistent Framework}}
+					{\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\\
@@ -144,17 +144,18 @@
 \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 Calculation possiblities, Featured Steps} %example partial fractions
-			\item Information Collection\\
-				{\small Possiblies and Challanges in {\sisac{}}}
-			\item \textbf{TP-Programming}			
-			\item Documentation\\
-				{\small Representation of underlying knowledge in the system}
+				{\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}
@@ -165,11 +166,11 @@
 	\begin{spacing}{1.3}
 		\begin{itemize}
 			\item What knowledge is mechanized in Isabelle?\\
-						{\small How about new?}
-			\item What problems are implemented in {\sisac{}}?\\
-						{\small How about new?}
-			\item What is the contents of the interactive course material?\\
-				{\small Figures, Explanations,\ldots}
+						{\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}
@@ -179,52 +180,58 @@
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 \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 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{Technical Survey II {\normalsize Representation Problems} }
-	\begin{spacing}{1.9}
-		\begin{itemize}
-			\item Different brackets have different meanings\\
-						{\small $u[n] \neq u(n)$\ldots in Math; but also in the source code}
-			\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{Technical Survey III {\normalsize Notation Problems} }
-	\begin{spacing}{1.8}
+	\frametitle{Representation Problems}
+	\begin{spacing}{1.4}
 		\begin{center}
-			Simplification, tricks and beauty\\
-			  \vspace{7mm}
+			
+			  \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 of {\isac}}
+	\frametitle{Demonstration}
 	\begin{spacing}{1.5}
 		\begin{itemize}
-			\item Frontend - {\small The shiny side\ldots}
-			\item Backend - {\small The dark side\ldots}
+			\item Backend
 			\begin{itemize}
 				\item Equation solving
 				\item Notation problems, Working with Rulesets
@@ -244,12 +251,11 @@
 	\frametitle{Conclusion}
 	\begin{spacing}{1.2}
 	    \begin{itemize}
-				\item TP-based language not ready
-				\item Programming guideline not yet sufficient
-				\item Hope for usability in enginieering studies
-				\item Wide range of interested people
+	    	\item Proof of concept for TP-PL succesfull
+				\item Usability of TP-PL not sufficient
+				\item Requirements for improved usability clarified
 				\vspace{5mm}
-				\item Hard to spend 200h on 1 programm
+				\item Unacceptable to spend 200h on 1 program
 				\item \isac{} pointed at my own error
 			\end{itemize}
 		\end{spacing}
@@ -262,7 +268,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}}\\
-				Projectleader & \small \texttt{\href{mailto:neuper@ist.tugraz.at}{neuper@ist.tugraz.at}}\\
+				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}




