142 |
142 |
143 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
143 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
144 \section{Material Creation} |
144 \section{Material Creation} |
145 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
145 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
146 |
146 |
|
147 \subsection{steps} |
147 \begin{frame} |
148 \begin{frame} |
148 \frametitle{Course Material Creation {\normalsize Iterations}} %tasks? work flow? |
149 \frametitle{Course Material Creation {\normalsize Iterations}} %tasks? work flow? |
149 \begin{spacing}{1.3} |
150 \begin{spacing}{1.3} |
150 \begin{enumerate} |
151 \begin{enumerate} |
151 \item Problem Analysis\\ |
152 \item Problem Analysis\\ |
152 {\small Calculation possiblities, Featured Steps} %example partial fractions |
153 {\small Variants of problem solving steps} %example partial fractions |
153 \item Information Collection\\ |
154 \item \textbf{Analysis of mechanized knowledge}\\ |
154 {\small Possiblies and Challanges in {\sisac{}}} |
155 {\small Existing and missing knowledge} |
155 \item \textbf{TP-Programming} |
156 \item \textbf{Programming in a TP based language (TP-PL)} |
156 \item Documentation\\ |
157 \item Additional Content\\ |
157 {\small Representation of underlying knowledge in the system} |
158 {\small Multimedia explanations for underlying knowledge} |
158 \end{enumerate} |
159 \end{enumerate} |
159 \end{spacing} |
160 \end{spacing} |
160 \end{frame} |
161 \end{frame} |
161 |
162 |
162 \subsection{issues} |
163 \subsection{issues} |
163 \begin{frame} |
164 \begin{frame} |
164 \frametitle{Issues to Accomplish {\normalsize Information Collection}} |
165 \frametitle{Issues to Accomplish {\normalsize Information Collection}} |
165 \begin{spacing}{1.3} |
166 \begin{spacing}{1.3} |
166 \begin{itemize} |
167 \begin{itemize} |
167 \item What knowledge is mechanized in Isabelle?\\ |
168 \item What knowledge is mechanized in Isabelle?\\ |
168 {\small How about new?} |
169 {\small Theorems, Definitions, Numbers,\ldots} |
169 \item What problems are implemented in {\sisac{}}?\\ |
170 \item What knowledge is mechanized in {\isac{}}?\\ |
170 {\small How about new?} |
171 {\small Problem specifications, Programs,\ldots} |
171 \item What is the contents of the interactive course material?\\ |
172 \item What additional explanations are required?\\ |
172 {\small Figures, Explanations,\ldots} |
173 {\small Figures, Examples,\ldots} |
173 \end{itemize} |
174 \end{itemize} |
174 \end{spacing} |
175 \end{spacing} |
175 \end{frame} |
176 \end{frame} |
176 |
177 |
177 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
178 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
178 \section{Details} |
179 \section{Details} |
179 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
180 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
180 |
181 |
181 \subsection{Technical Survey} |
182 \subsection{Technical Survey} |
182 \begin{frame} |
183 %\begin{frame} |
183 \frametitle{Technical Survey I {\normalsize Mechanizing Knowledge}} |
184 % \frametitle{Technical Survey I {\normalsize Mechanizing Knowledge}} |
184 \begin{spacing}{1.5} |
185 % \begin{spacing}{1.5} |
185 \begin{itemize} |
186 % \begin{itemize} |
186 \item Not enough knowledge is mechanized\\ |
187 % \item Not enough knowledge is mechanized\\ |
187 {\small Equation Solving, Integrals,\ldots} |
188 % {\small Equation Solving, Integrals,\ldots} |
188 \item Computer Mathematicians required!\\ |
189 % \item Computer Mathematicians required!\\ |
189 {\small Mathematics: Equation solving, Engineer: Z-Transform} |
190 % {\small Mathematics: Equation solving, Engineer: Z-Transform} |
190 \item RISC Linz, Mathematics TU Graz |
191 % \item RISC Linz, Mathematics TU Graz |
191 \end{itemize} |
192 % \end{itemize} |
192 \end{spacing} |
193 % \end{spacing} |
193 \end{frame} |
194 %\end{frame} |
194 |
195 |
195 \begin{frame} |
196 %\begin{frame} |
196 \frametitle{Technical Survey II {\normalsize Representation Problems} } |
197 % \frametitle{Technical Survey II {\normalsize Representation Problems} } |
197 \begin{spacing}{1.9} |
198 % \begin{spacing}{1.9} |
198 \begin{itemize} |
199 % \begin{itemize} |
199 \item Different brackets have different meanings\\ |
200 % \item Different brackets have different meanings\\ |
200 {\small $u[n] \neq u(n)$\ldots in Math; but also in the source code} |
201 % {\small $u[n]$ is a specific function application :) } |
201 \item We need Symbols, Indizes and Hochzahlen |
202 % \item We need Symbols, Indizes and Hochzahlen |
202 \item Different Representations for different purpos %winkel in polar oder kartesischen koordinaten usw. |
203 % \item Different Representations for different purpos %winkel in polar oder kartesischen koordinaten usw. |
203 \end{itemize} |
204 % \end{itemize} |
204 \end{spacing} |
205 % \end{spacing} |
205 \end{frame} |
206 %\end{frame} |
206 |
207 |
207 \begin{frame} |
208 \begin{frame} |
208 \frametitle{Technical Survey III {\normalsize Notation Problems} } |
209 \frametitle{Representation Problems} |
209 \begin{spacing}{1.8} |
210 \begin{spacing}{1.4} |
210 \begin{center} |
211 \begin{center} |
211 Simplification, tricks and beauty\\ |
212 |
212 \vspace{7mm} |
213 \begin{itemize} |
|
214 \item Can meaning of symbols be varied?\\ |
|
215 {\small $u[n]$ is a specific function in Signal Processing} |
|
216 \item Simplification, tricks and beauty |
|
217 \end{itemize} |
|
218 |
213 {\small $X\cdot(a+b)+Y\cdot(c+d)=aX+bX+cY+dY$}\\ |
219 {\small $X\cdot(a+b)+Y\cdot(c+d)=aX+bX+cY+dY$}\\ |
214 \vspace{3mm} |
220 \vspace{3mm} |
215 {\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)=$}\\ |
221 {\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)=$}\\ |
216 {\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)$} $} |
222 {\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)$} $} |
|
223 |
|
224 |
217 \end{center} |
225 \end{center} |
218 \end{spacing} |
226 \end{spacing} |
219 \end{frame} |
227 \end{frame} |
220 |
228 |
221 \subsection{Demonstration} |
229 \subsection{Demonstration} |
222 \begin{frame} |
230 \begin{frame} |
223 \frametitle{Demonstration of {\isac}} |
231 \frametitle{Demonstration} |
224 \begin{spacing}{1.5} |
232 \begin{spacing}{1.5} |
225 \begin{itemize} |
233 \begin{itemize} |
226 \item Frontend - {\small The shiny side\ldots} |
234 \item Backend |
227 \item Backend - {\small The dark side\ldots} |
|
228 \begin{itemize} |
235 \begin{itemize} |
229 \item Equation solving |
236 \item Equation solving |
230 \item Notation problems, Working with Rulesets |
237 \item Notation problems, Working with Rulesets |
231 \item Framework expansion |
238 \item Framework expansion |
232 \item My Work |
239 \item My Work |