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}
2.1 --- a/test/Tools/isac/ADDTESTS/course/CADGME/example_1.thy Thu Jun 21 20:48:36 2012 +0200
2.2 +++ b/test/Tools/isac/ADDTESTS/course/CADGME/example_1.thy Fri Aug 31 19:19:07 2012 +0200
2.3 @@ -1,12 +1,4 @@
2.4 -(* Title: example_1
2.5 - Author: Jan Rocnik
2.6 - Description: The following Example can be used as an HOWTO on applying
2.7 - already implemented Subproblems. In example solving a
2.8 - linear equation.
2.9 - (c) copyright due to license terms.
2.10 -12345678901234567890123456789012345678901234567890123456789012345678901234567890
2.11 - 10 20 30 40 50 60 70 80
2.12 -*)
2.13 +
2.14
2.15 theory example_1 imports Isac
2.16 begin
2.17 @@ -15,25 +7,15 @@
2.18 text{*Setup equation, Calc Tree,\ldots*}
2.19
2.20 ML {*
2.21 - val equation = "equality (-1 + -2 * z + 8 * z ^^^ 2 = (0::real))";
2.22 - val expr = [ equation, "solveFor z", "solutions L"]; (*specification*)
2.23 - (*equality, bound variable, identifier for solution*)
2.24 -
2.25 + val expr = ["equality (-1 + -2 * z + 8 * z ^^^ 2 = (0::real))",
2.26 + "solveFor z", "solutions L"];
2.27 val (dI',pI',mI') =
2.28 ("Isac",
2.29 ["abcFormula","degree_2","polynomial","univariate","equation"],
2.30 ["no_met"]);
2.31 -
2.32 *}
2.33
2.34 -text{*Possible Check if the equation matches the designated Method*}
2.35 -
2.36 -ML {*
2.37 - match_pbl expr (get_pbt
2.38 - ["abcFormula","degree_2","polynomial","univariate","equation"]);
2.39 -*}
2.40 -
2.41 -text{*Step throuh the Calculation Tree*}
2.42 +text{*Step through the Calculation*}
2.43
2.44 ML {*
2.45 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(expr, (dI',pI',mI'))];
3.1 --- a/test/Tools/isac/ADDTESTS/course/CADGME/example_2.thy Thu Jun 21 20:48:36 2012 +0200
3.2 +++ b/test/Tools/isac/ADDTESTS/course/CADGME/example_2.thy Fri Aug 31 19:19:07 2012 +0200
3.3 @@ -1,11 +1,3 @@
3.4 -(* Title: example_2
3.5 - Author: Jan Rocnik
3.6 - Description: The following Example can be used as an HOWTO on generating
3.7 - Rulesets and applying them to terms.
3.8 - (c) copyright due to license terms.
3.9 -12345678901234567890123456789012345678901234567890123456789012345678901234567890
3.10 - 10 20 30 40 50 60 70 80
3.11 -*)
3.12
3.13 theory example_2 imports Isac
3.14 begin
4.1 --- a/test/Tools/isac/ADDTESTS/course/CADGME/example_3.thy Thu Jun 21 20:48:36 2012 +0200
4.2 +++ b/test/Tools/isac/ADDTESTS/course/CADGME/example_3.thy Fri Aug 31 19:19:07 2012 +0200
4.3 @@ -1,11 +1,4 @@
4.4 -(* Title: example_3
4.5 - Author: Jan Rocnik
4.6 - Description: The following Example can be used as an HOWTO on implementing
4.7 - new Functions within the ISAC-System.
4.8 - (c) copyright due to license terms.
4.9 -12345678901234567890123456789012345678901234567890123456789012345678901234567890
4.10 - 10 20 30 40 50 60 70 80
4.11 -*)
4.12 +
4.13
4.14 theory example_3 imports Isac
4.15 begin