21 % does not look nice, try deleting the line with the fontenc. |
21 % does not look nice, try deleting the line with the fontenc. |
22 |
22 |
23 \def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$} |
23 \def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$} |
24 \def\sisac{{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}} |
24 \def\sisac{{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}} |
25 |
25 |
26 \title[TODO] % (optional, use only with long paper titles) |
26 \title[SPSC in \isac] % (optional, use only with long paper titles) |
27 {TODO} |
27 {Interactive Course Material\\ for Signal Processing\\ based on Isabelle/\isac} |
28 |
28 |
29 \subtitle{TODO} |
29 \subtitle{Baccalaureate Thesis} |
30 |
30 |
31 \author[Rocnik] % (optional, use only with lots of authors) |
31 \author[Rocnik] % (optional, use only with lots of authors) |
32 {Jan~Rocnik} |
32 {Jan~Rocnik} |
33 % - Give the names in the same order as the appear in the paper. |
33 % - Give the names in the same order as the appear in the paper. |
34 % - Use the \inst{?} command only if the authors have different |
34 % - Use the \inst{?} command only if the authors have different |
94 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
94 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
95 |
95 |
96 \begin{frame}{Outline} |
96 \begin{frame}{Outline} |
97 \tableofcontents |
97 \tableofcontents |
98 % You might wish to add the option [pausesections] |
98 % You might wish to add the option [pausesections] |
|
99 \end{frame} |
|
100 |
|
101 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
102 %%---------------------------------------------------------------%% |
|
103 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
104 |
|
105 \section[Intro]{Introduction} |
|
106 |
|
107 \begin{frame}{Introduction} |
|
108 Issues to be accomplished in this thesis: |
|
109 |
|
110 \begin{itemize} |
|
111 |
|
112 \item What knowledge is already mechanised in \emph{isabelle}? |
|
113 \item How can missing theorems and definitions be mechanised? |
|
114 \item What is the effort for such mechanisation? |
|
115 \item How do calculations look like, if using mechanised knowledge? |
|
116 \item What are the problems and subproblems to be solved? |
|
117 \item Which problems are already implemented in \sisac? |
|
118 \item How are the new Problems specified rigorously (\sisac)? |
|
119 \item Which variantes of programms in \sisac{} solving the problems? |
|
120 \item What is the contents of the interactiv course material (Figures, etc.)? |
|
121 |
|
122 \end{itemize} |
99 \end{frame} |
123 \end{frame} |
100 |
124 |
101 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
125 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
102 %%---------------------------------------------------------------%% |
126 %%---------------------------------------------------------------%% |
103 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
127 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
252 \end{center} |
276 \end{center} |
253 effort --- in 45min units\\ |
277 effort --- in 45min units\\ |
254 MT --- thesis ``Integrals'' (mathematics) |
278 MT --- thesis ``Integrals'' (mathematics) |
255 } |
279 } |
256 \end{frame} |
280 \end{frame} |
|
281 |
|
282 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
283 %%--------------------FOURIER---Conclusion-----------------------%% |
|
284 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
285 |
|
286 %\subsection[Summary]{Summary} |
|
287 |
|
288 \begin{frame}{Summary} |
|
289 todo |
|
290 |
|
291 \begin{itemize} |
|
292 |
|
293 \item todo |
|
294 |
|
295 \end{itemize} |
|
296 \end{frame} |
|
297 |
257 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
298 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
258 %-----------------------------------------------------------------% |
299 %-----------------------------------------------------------------% |
259 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
300 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
260 |
301 |
261 \section[Discrete time]{Discrete-time systems} |
302 \section[Discrete time]{Discrete-time systems} |