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}