equal
deleted
inserted
replaced
75 |
75 |
76 \begin{frame}{Issues to be Accomplished} |
76 \begin{frame}{Issues to be Accomplished} |
77 |
77 |
78 \begin{itemize} |
78 \begin{itemize} |
79 |
79 |
80 \item What knowledge is already mechanised in \emph{isabelle}? |
80 \item What knowledge is already mechanised in \emph{Isabelle}? |
81 \item How can missing theorems and definitions be mechanised? |
81 \item How can missing theorems and definitions be mechanised? |
82 \item What is the effort for such mechanisation? |
82 \item What is the effort for such mechanisation? |
83 \item How do calculations look like, by using mechanised knowledge? |
83 \item How do calculations look like, by using mechanised knowledge? |
84 \item What problems and subproblems have to be solved? |
84 \item What problems and subproblems have to be solved? |
85 \item Which problems are already implemented in \sisac? |
85 \item Which problems are already implemented in \sisac? |
171 |
171 |
172 \begin{frame}{Fourier Transformation: Summary} |
172 \begin{frame}{Fourier Transformation: Summary} |
173 \begin{itemize} |
173 \begin{itemize} |
174 |
174 |
175 \item Standard integrals can be solved with tables |
175 \item Standard integrals can be solved with tables |
176 \item No real integration (yet avaiible) |
176 \item No real integration (yet avaible) |
177 \item Math \emph{tricks} difficult to implement |
177 \item Math \emph{tricks} difficult to implement |
178 |
178 |
179 |
179 |
180 \end{itemize} |
180 \end{itemize} |
181 \end{frame} |
181 \end{frame} |
183 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
183 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
184 %-----------------------------------------------------------------% |
184 %-----------------------------------------------------------------% |
185 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
185 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
186 |
186 |
187 \section[LTI Systems]{LTI systems} |
187 \section[LTI Systems]{LTI systems} |
188 \subsection[Convolution]{Convolution} |
188 \subsection[Convolution]{Convolution (Faltung)} |
189 |
189 |
190 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
190 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
191 %% LTI INTRO %% |
191 %% LTI INTRO %% |
192 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
192 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
193 |
193 |
194 \begin{frame}\frametitle{Convolution: Introduction} |
194 \begin{frame}\frametitle{Convolution: Introduction} |
|
195 TODO!!! |
195 \begin{itemize} |
196 \begin{itemize} |
196 \item Calculation\ldots |
197 \item Calculation\ldots |
197 \item Visualisation\ldots |
198 \item Visualisation\ldots |
198 \end{itemize} |
199 \end{itemize} |
199 \begin{center} |
200 \begin{center} |
216 \end{center} |
217 \end{center} |
217 |
218 |
218 The two systems are cascaded seriell. Derive the impulse respinse of the overall system $h_c[n]$. |
219 The two systems are cascaded seriell. Derive the impulse respinse of the overall system $h_c[n]$. |
219 |
220 |
220 \hrulefill |
221 \hrulefill |
221 |
222 ??? |
222 \begin{tabbing} |
223 \begin{tabbing} |
223 1\=postcond \=: \= \= $\;\;\;\;$\=\kill |
224 1\=postcond \=: \= \= $\;\;\;\;$\=\kill |
224 \>given \>:\> Signals h1[n], h2[n] \\ |
225 \>given \>:\> Signals h1[n], h2[n] \\ |
225 \> \> \> \>((h1 (n::real),(3/5)\textasciicircum{}n\,u(n::real)),\,(h2 (n::real),(-2/3)\textasciicircum{}n\,u(n::real)))\\ |
226 \> \> \> \>((h1 (n::real),(3/5)\textasciicircum{}n\,u(n::real)),\,(h2 (n::real),(-2/3)\textasciicircum{}n\,u(n::real)))\\ |
226 %?(iterativer) datentyp in Isabelle/HOL |
227 %?(iterativer) datentyp in Isabelle/HOL |
261 |
262 |
262 \begin{frame}{Convolution: Summary} |
263 \begin{frame}{Convolution: Summary} |
263 \begin{itemize} |
264 \begin{itemize} |
264 |
265 |
265 \item Standard example |
266 \item Standard example |
266 \item Straight foreward |
267 \item Straight forward |
267 \item Challenge are sum limits |
268 \item Challenge are sum limits |
268 |
269 |
269 \end{itemize} |
270 \end{itemize} |
270 \end{frame} |
271 \end{frame} |
271 |
272 |
361 |
362 |
362 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
363 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
363 %-----------------------------------------------------------------% |
364 %-----------------------------------------------------------------% |
364 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
365 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
365 |
366 |
366 \section[Closing]{Closing} |
367 \section[Conclusions]{Conclusions} |
367 |
368 |
368 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
369 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
369 %--------------------------CONCLUSION-----------------------------% |
370 %--------------------------CONCLUSION-----------------------------% |
370 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
371 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
371 |
372 |