1.1 --- a/doc-src/isac/jrocnik/jrocnik_cadgme.tex Thu Jun 21 20:48:36 2012 +0200
1.2 +++ b/doc-src/isac/jrocnik/jrocnik_cadgme.tex Fri Aug 31 19:19:07 2012 +0200
1.3 @@ -104,9 +104,9 @@
1.4 \frametitle{What is Isabelle?}
1.5 \begin{spacing}{2}
1.6 \begin{itemize}
1.7 - \item Generic Proof Assistant
1.8 - \item Formula proofing in logical calculus
1.9 - \item Developed in Cambridge, Muenchen and Paris
1.10 + \item Interactive Theorem Prover (Interactice TP)
1.11 + \item Large body of mechanized math knowledge
1.12 + \item Developed in Cambridge, Munich and Paris
1.13 \end{itemize}
1.14 \end{spacing}
1.15 \end{frame}
1.16 @@ -126,10 +126,10 @@
1.17
1.18 \subsection{motivation}
1.19 \begin{frame}
1.20 - \frametitle{Motivation - {\isac{}}'s~Potential}
1.21 + \frametitle{{\isac{}} for Interactive Course Material}
1.22 \begin{itemize}
1.23 \item Stepwise solving of engineering problems\\
1.24 - {\small $\rightarrow$ \textcolor{tug}{Consistent Framework}}
1.25 + {\small $\rightarrow$ \textcolor{tug}{One Framework for all phases of problem solving}}
1.26 \item Explaining underlying knowledge\\
1.27 {\small $\rightarrow$ \textcolor{tug}{Transparent Content, Access to Multimedia Content}}
1.28 \item Checking steps input by the student\\
1.29 @@ -144,17 +144,18 @@
1.30 \section{Material Creation}
1.31 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.32
1.33 +\subsection{steps}
1.34 \begin{frame}
1.35 \frametitle{Course Material Creation {\normalsize Iterations}} %tasks? work flow?
1.36 \begin{spacing}{1.3}
1.37 \begin{enumerate}
1.38 \item Problem Analysis\\
1.39 - {\small Calculation possiblities, Featured Steps} %example partial fractions
1.40 - \item Information Collection\\
1.41 - {\small Possiblies and Challanges in {\sisac{}}}
1.42 - \item \textbf{TP-Programming}
1.43 - \item Documentation\\
1.44 - {\small Representation of underlying knowledge in the system}
1.45 + {\small Variants of problem solving steps} %example partial fractions
1.46 + \item \textbf{Analysis of mechanized knowledge}\\
1.47 + {\small Existing and missing knowledge}
1.48 + \item \textbf{Programming in a TP based language (TP-PL)}
1.49 + \item Additional Content\\
1.50 + {\small Multimedia explanations for underlying knowledge}
1.51 \end{enumerate}
1.52 \end{spacing}
1.53 \end{frame}
1.54 @@ -165,11 +166,11 @@
1.55 \begin{spacing}{1.3}
1.56 \begin{itemize}
1.57 \item What knowledge is mechanized in Isabelle?\\
1.58 - {\small How about new?}
1.59 - \item What problems are implemented in {\sisac{}}?\\
1.60 - {\small How about new?}
1.61 - \item What is the contents of the interactive course material?\\
1.62 - {\small Figures, Explanations,\ldots}
1.63 + {\small Theorems, Definitions, Numbers,\ldots}
1.64 + \item What knowledge is mechanized in {\isac{}}?\\
1.65 + {\small Problem specifications, Programs,\ldots}
1.66 + \item What additional explanations are required?\\
1.67 + {\small Figures, Examples,\ldots}
1.68 \end{itemize}
1.69 \end{spacing}
1.70 \end{frame}
1.71 @@ -179,52 +180,58 @@
1.72 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.73
1.74 \subsection{Technical Survey}
1.75 -\begin{frame}
1.76 - \frametitle{Technical Survey I {\normalsize Mechanizing Knowledge}}
1.77 - \begin{spacing}{1.5}
1.78 - \begin{itemize}
1.79 - \item Not enough knowledge is mechanized\\
1.80 - {\small Equation Solving, Integrals,\ldots}
1.81 - \item Computer Mathematicians required!\\
1.82 - {\small Mathematics: Equation solving, Engineer: Z-Transform}
1.83 - \item RISC Linz, Mathematics TU Graz
1.84 - \end{itemize}
1.85 - \end{spacing}
1.86 -\end{frame}
1.87 +%\begin{frame}
1.88 +% \frametitle{Technical Survey I {\normalsize Mechanizing Knowledge}}
1.89 +% \begin{spacing}{1.5}
1.90 +% \begin{itemize}
1.91 +% \item Not enough knowledge is mechanized\\
1.92 +% {\small Equation Solving, Integrals,\ldots}
1.93 +% \item Computer Mathematicians required!\\
1.94 +% {\small Mathematics: Equation solving, Engineer: Z-Transform}
1.95 +% \item RISC Linz, Mathematics TU Graz
1.96 +% \end{itemize}
1.97 +% \end{spacing}
1.98 +%\end{frame}
1.99 +
1.100 +%\begin{frame}
1.101 +% \frametitle{Technical Survey II {\normalsize Representation Problems} }
1.102 +% \begin{spacing}{1.9}
1.103 +% \begin{itemize}
1.104 +% \item Different brackets have different meanings\\
1.105 +% {\small $u[n]$ is a specific function application :) }
1.106 +% \item We need Symbols, Indizes and Hochzahlen
1.107 +% \item Different Representations for different purpos %winkel in polar oder kartesischen koordinaten usw.
1.108 +% \end{itemize}
1.109 +% \end{spacing}
1.110 +%\end{frame}
1.111
1.112 \begin{frame}
1.113 - \frametitle{Technical Survey II {\normalsize Representation Problems} }
1.114 - \begin{spacing}{1.9}
1.115 - \begin{itemize}
1.116 - \item Different brackets have different meanings\\
1.117 - {\small $u[n] \neq u(n)$\ldots in Math; but also in the source code}
1.118 - \item We need Symbols, Indizes and Hochzahlen
1.119 - \item Different Representations for different purpos %winkel in polar oder kartesischen koordinaten usw.
1.120 - \end{itemize}
1.121 - \end{spacing}
1.122 -\end{frame}
1.123 -
1.124 -\begin{frame}
1.125 - \frametitle{Technical Survey III {\normalsize Notation Problems} }
1.126 - \begin{spacing}{1.8}
1.127 + \frametitle{Representation Problems}
1.128 + \begin{spacing}{1.4}
1.129 \begin{center}
1.130 - Simplification, tricks and beauty\\
1.131 - \vspace{7mm}
1.132 +
1.133 + \begin{itemize}
1.134 + \item Can meaning of symbols be varied?\\
1.135 + {\small $u[n]$ is a specific function in Signal Processing}
1.136 + \item Simplification, tricks and beauty
1.137 + \end{itemize}
1.138 +
1.139 {\small $X\cdot(a+b)+Y\cdot(c+d)=aX+bX+cY+dY$}\\
1.140 \vspace{3mm}
1.141 {\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.142 {\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.143 +
1.144 +
1.145 \end{center}
1.146 \end{spacing}
1.147 \end{frame}
1.148
1.149 \subsection{Demonstration}
1.150 \begin{frame}
1.151 - \frametitle{Demonstration of {\isac}}
1.152 + \frametitle{Demonstration}
1.153 \begin{spacing}{1.5}
1.154 \begin{itemize}
1.155 - \item Frontend - {\small The shiny side\ldots}
1.156 - \item Backend - {\small The dark side\ldots}
1.157 + \item Backend
1.158 \begin{itemize}
1.159 \item Equation solving
1.160 \item Notation problems, Working with Rulesets
1.161 @@ -244,12 +251,11 @@
1.162 \frametitle{Conclusion}
1.163 \begin{spacing}{1.2}
1.164 \begin{itemize}
1.165 - \item TP-based language not ready
1.166 - \item Programming guideline not yet sufficient
1.167 - \item Hope for usability in enginieering studies
1.168 - \item Wide range of interested people
1.169 + \item Proof of concept for TP-PL succesfull
1.170 + \item Usability of TP-PL not sufficient
1.171 + \item Requirements for improved usability clarified
1.172 \vspace{5mm}
1.173 - \item Hard to spend 200h on 1 programm
1.174 + \item Unacceptable to spend 200h on 1 program
1.175 \item \isac{} pointed at my own error
1.176 \end{itemize}
1.177 \end{spacing}
1.178 @@ -262,7 +268,7 @@
1.179 \begin{tabular}{lr}
1.180 Isabelle & \small \texttt{\href{isabelle.in.tum.de}{isabelle.in.tum.de}}\\
1.181 The {\isac}-Project & \small \texttt{\href{www.ist.tugraz.at/isac}{www.ist.tugraz.at/isac}}\\
1.182 - Projectleader & \small \texttt{\href{mailto:neuper@ist.tugraz.at}{neuper@ist.tugraz.at}}\\
1.183 + Project leader & \small \texttt{\href{mailto:wneuper@ist.tugraz.at}{wneuper@ist.tugraz.at}}\\
1.184 Jan Rocnik & \small \texttt{\href{mailto:jan.rocnik@student.tugraz.at}{jan.rocnik@student.tugraz.at}}
1.185 \end{tabular}
1.186 \end{spacing}