1.1 --- a/doc-src/isac/jrocnik/present-1.tex Sat Jul 23 18:47:12 2011 +0200
1.2 +++ b/doc-src/isac/jrocnik/present-1.tex Sun Jul 24 19:38:53 2011 +0200
1.3 @@ -8,17 +8,10 @@
1.4 \setbeamercovered{transparent}
1.5 }
1.6
1.7 -%\usepackage{setspace} %for "\begin{onehalfspace}"
1.8 \usepackage[english]{babel}
1.9 -% or whatever
1.10 -
1.11 \usepackage[utf8]{inputenc}
1.12 -% or whatever
1.13 -
1.14 \usepackage{times}
1.15 \usepackage[T1]{fontenc}
1.16 -% Or whatever. Note that the encoding and the font should match. If T1
1.17 -% does not look nice, try deleting the line with the fontenc.
1.18
1.19 \def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
1.20 \def\sisac{{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}}
1.21 @@ -28,31 +21,14 @@
1.22
1.23 \subtitle{Baccalaureate Thesis}
1.24
1.25 -\author[Rocnik] % (optional, use only with lots of authors)
1.26 -{Jan~Rocnik}
1.27 -% - Give the names in the same order as the appear in the paper.
1.28 -% - Use the \inst{?} command only if the authors have different
1.29 -% affiliation.
1.30 +\author[Ro\v{c}nik]
1.31 +{Jan Rocnik}
1.32
1.33 \institute % (optional, but mostly needed)
1.34 {
1.35 Technische Universit\"at Graz\\
1.36 Institut f\"ur TODO
1.37 }
1.38 -% - Use the \inst command only if there are several affiliations.
1.39 -% - Keep it simple, no one is interested in your street address.
1.40 -
1.41 -% \date[CFP 2003] % (optional, should be abbreviation of conference name)
1.42 -% {Conference on Fabulous Presentations, 2003}
1.43 -% - Either use conference name or its abbreviation.
1.44 -% - Not really informative to the audience, more for people (including
1.45 -% yourself) who are reading the slides online
1.46 -
1.47 -% \subject{Theoretical Computer Science}
1.48 -% This is only inserted into the PDF information catalog. Can be left
1.49 -% out.
1.50 -
1.51 -
1.52
1.53 % If you have a file called "university-logo-filename.xxx", where xxx
1.54 % is a graphic format that can be processed by latex or pdflatex,
1.55 @@ -72,13 +48,6 @@
1.56 \end{frame}
1.57 }
1.58
1.59 -
1.60 -% If you wish to uncover everything in a step-wise fashion, uncomment
1.61 -% the following command:
1.62 -
1.63 -%\beamerdefaultoverlayspecification{<+->}
1.64 -
1.65 -
1.66 \begin{document}
1.67
1.68 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.69 @@ -104,19 +73,18 @@
1.70
1.71 \section[Intro]{Introduction}
1.72
1.73 -\begin{frame}{Introduction}
1.74 -Issues to be accomplished in this thesis:
1.75 +\begin{frame}{Issues to be Accomplished}
1.76
1.77 \begin{itemize}
1.78
1.79 \item What knowledge is already mechanised in \emph{isabelle}?
1.80 \item How can missing theorems and definitions be mechanised?
1.81 \item What is the effort for such mechanisation?
1.82 -\item How do calculations look like, if using mechanised knowledge?
1.83 -\item What are the problems and subproblems to be solved?
1.84 +\item How do calculations look like, by using mechanised knowledge?
1.85 +\item What problems and subproblems have to be solved?
1.86 \item Which problems are already implemented in \sisac?
1.87 -\item How are the new Problems specified rigorously (\sisac)?
1.88 -\item Which variantes of programms in \sisac{} solving the problems?
1.89 +\item How are the new problems specified (\sisac)?
1.90 +\item Which variantes of programms in \sisac\ solve the problems?
1.91 \item What is the contents of the interactiv course material (Figures, etc.)?
1.92
1.93 \end{itemize}
1.94 @@ -126,7 +94,8 @@
1.95 %%---------------------------------------------------------------%%
1.96 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.97
1.98 -\section[Fourier]{Fourier transform}
1.99 +\section[Fourier]{Fourier transformation}
1.100 +\subsection[Fourier]{Fourier transform}
1.101
1.102 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.103 %% Fourier INTRO %%
1.104 @@ -134,68 +103,20 @@
1.105
1.106 \begin{frame}\frametitle{Fourier Transformation: Introduction}
1.107 \begin{itemize}
1.108 -\item Transform operation by using property-tables $\rightarrow$ \emph{easy}
1.109 -\item Transform operation by using integral $\rightarrow$ \emph{difficult}
1.110 -\item No math \emph{tricks}
1.111 +\item Transform operation by using property-tables
1.112 +\item Transform operation by using integral
1.113 \item Important: Visualisation?!
1.114 \end{itemize}
1.115 \end{frame}
1.116
1.117 -\subsection[simple]{Fourier transform Example 1}
1.118 -
1.119 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.120 -%% Transform expl 1 SPEC %%
1.121 +%% Transform expl SPEC %%
1.122 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.123
1.124 -\begin{frame}\frametitle{Fourier Transform 1: Specification}
1.125 -{\footnotesize\it
1.126 -Fourier Transform
1.127 +\begin{frame}\frametitle{Fourier Transformation: Specification}
1.128 +{\footnotesize
1.129
1.130 -\hrulefill
1.131 -
1.132 -\begin{tabbing}
1.133 -1\=postcond \=: \= \= $\;\;\;\;$\=\kill
1.134 -\>given \>:\> Time continiues, not periodic Signal \\
1.135 -\> \> \> \>$(x (t::real), exp(-\,(\alpha::real\,+\,\alpha::imag)\,*\,t::real)*u(t::real))$\\
1.136 -\>precond \>:\> TODO\\
1.137 -\>find \>:\> $X(j\cdot\omega)$\\
1.138 -\>postcond \>:\> TODO\\
1.139 -\end{tabbing}
1.140 -
1.141 -}
1.142 -\end{frame}
1.143 -
1.144 -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.145 -%% Transform expl 1 REQ %%
1.146 -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.147 -
1.148 -\begin{frame}\frametitle{Fourier Transform 1: Development effort}
1.149 -{\small
1.150 -\begin{center}
1.151 -\begin{tabular}{l|l|r}
1.152 -requirements & comments &effort\\ \hline\hline
1.153 -solving Intrgrals & simple via propertie table & 20\\
1.154 - & \emph{real} & MT\\ \hline
1.155 -transformation table & simple transform & 20\\ \hline
1.156 -example collection & with explanations & 20\\ \hline\hline
1.157 - & & 60-80\\
1.158 -\end{tabular}
1.159 -\end{center}
1.160 -effort --- in 45min units\\
1.161 -MT --- thesis ``Integrals'' (mathematics)
1.162 -}
1.163 -\end{frame}
1.164 -
1.165 -\subsection[difficult]{Fourier transform Example 2}
1.166 -
1.167 -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.168 -%% Transform expl 2 SPEC %%
1.169 -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.170 -
1.171 -\begin{frame}\frametitle{Fourier Transform 2: Specification}
1.172 -{\footnotesize\it
1.173 -
1.174 -\textbf{(a)} Determine the fourier transform for the given rectangular impulse:
1.175 +Determine the fourier transform for the given rectangular impulse:
1.176
1.177 \begin{center}
1.178 $x(t)= \left\{
1.179 @@ -206,6 +127,8 @@
1.180 \right.$
1.181 \end{center}
1.182
1.183 +\hrulefill
1.184 +
1.185 \begin{tabbing}
1.186 1\=postcond \=: \= \= $\;\;\;\;$\=\kill
1.187 \>given \>:\> piecewise\_function \\
1.188 @@ -221,10 +144,10 @@
1.189 \end{frame}
1.190
1.191 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.192 -%% Transform expl 2 REQ %%
1.193 +%% Transform expl REQ %%
1.194 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.195
1.196 -\begin{frame}\frametitle{Fourier Transform 2: Development effort}
1.197 +\begin{frame}\frametitle{Fourier Transform: Development effort}
1.198 {\small
1.199 \begin{center}
1.200 \begin{tabular}{l|l|r}
1.201 @@ -246,12 +169,13 @@
1.202 %%--------------------FOURIER---Conclusion-----------------------%%
1.203 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.204
1.205 -\begin{frame}{Summary}
1.206 -todo
1.207 -
1.208 +\begin{frame}{Fourier Transformation: Summary}
1.209 \begin{itemize}
1.210
1.211 -\item todo
1.212 +\item Standard integrals can be solved with tables
1.213 +\item No real integration (yet avaiible)
1.214 +\item Math \emph{tricks} difficult to implement
1.215 +
1.216
1.217 \end{itemize}
1.218 \end{frame}
1.219 @@ -260,7 +184,7 @@
1.220 %-----------------------------------------------------------------%
1.221 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.222
1.223 -\section[Discrete time]{Discrete-time systems}
1.224 +\section[LTI Systems]{LTI systems}
1.225 \subsection[Convolution]{Convolution}
1.226
1.227 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.228 @@ -282,7 +206,7 @@
1.229 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.230
1.231 \begin{frame}\frametitle{Convolution: Specification}
1.232 -{\footnotesize\it
1.233 +{\footnotesize
1.234
1.235 Consider the two discrete-time, linear and time-invariant (LTI) systems with the following impulse response:
1.236
1.237 @@ -335,12 +259,12 @@
1.238 %%--------------------LTI-------Conclusion-----------------------%%
1.239 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.240
1.241 -\begin{frame}{Summary}
1.242 -todo
1.243 -
1.244 +\begin{frame}{Convolution: Summary}
1.245 \begin{itemize}
1.246
1.247 -\item todo
1.248 +\item Standard example
1.249 +\item Straight foreward
1.250 +\item Challenge are sum limits
1.251
1.252 \end{itemize}
1.253 \end{frame}
1.254 @@ -368,14 +292,15 @@
1.255 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.256
1.257 \begin{frame}\frametitle{(Inverse) Z-Transformation: Specification}
1.258 -{\footnotesize\it
1.259 +{\footnotesize
1.260
1.261 -Determine the inverse $\cal{z}$ transform of the following expression. Hint: applay the partial fraction expansion.
1.262 +Determine the inverse z transform of the following expression. Hint: applay the partial fraction expansion.
1.263
1.264 \begin{center}
1.265 $X(z)=\frac{3}{z-\frac{1}{4}-\frac{1}{8}z^{-1}},\ \ x[n]$ is absolute summable
1.266 \end{center}
1.267
1.268 +
1.269 \hrulefill
1.270
1.271 \begin{tabbing}
1.272 @@ -424,16 +349,76 @@
1.273 %%--------------------Z-TRANS---Conclusion-----------------------%%
1.274 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.275
1.276 -\begin{frame}{Summary}
1.277 -todo
1.278 -
1.279 +\begin{frame}{(Inverse) Z-Transformation: Summary}
1.280 \begin{itemize}
1.281
1.282 -\item todo
1.283 +\item No \emph{higher} math operations
1.284 +\item Different subproblems of math (equation systems, etc.)
1.285 +\item Both directions have the same effort
1.286
1.287 \end{itemize}
1.288 \end{frame}
1.289
1.290 +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.291 +%-----------------------------------------------------------------%
1.292 +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.293 +
1.294 +\section[Closing]{Closing}
1.295 +
1.296 +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.297 +%--------------------------CONCLUSION-----------------------------%
1.298 +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.299 +
1.300 +\begin{frame}{Conclusions}
1.301 +
1.302 +Design Challanges:
1.303 +
1.304 +{\small
1.305 +\begin{itemize}
1.306 +
1.307 +\item Pre and Post conditions
1.308 +\item Exact mathematic behind functions
1.309 +\item accurate mathematic notation
1.310 +
1.311 +\end{itemize}
1.312 +}
1.313 +
1.314 +Goals:
1.315 +{\small
1.316 +\begin{itemize}
1.317 +
1.318 +\item Spot the power of \sisac
1.319 +\item Implementation of generell but simple math problems
1.320 +\item Setting up a good first guideline (documentation) for furher problem implemenations
1.321 +
1.322 +\end{itemize}
1.323 +
1.324 +\centering{Efforts are only approximations, due we have no \emph{real} experience data!}
1.325 +}
1.326 +
1.327 +\end{frame}
1.328 +
1.329 +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.330 +%--------------------------TIME LINE------------------------------%
1.331 +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1.332 +
1.333 +\begin{frame}{Comming up}
1.334 +
1.335 +{\small
1.336 +\begin{tabular}{l r}
1.337 +
1.338 +Juli 2011 & project startup\\
1.339 +Juli 2011 & information collection, 1st presentation\\
1.340 +August 2011 & extern traineeship\\
1.341 +September 2011 & main work\\
1.342 +after Oktober & finishing, documentation\\
1.343 +
1.344 +\end{tabular}
1.345 +}
1.346 +
1.347 +\end{frame}
1.348 +
1.349 +
1.350 \end{document}
1.351
1.352
2.1 --- a/doc-src/isac/jrocnik/vorlage-bakkarbeit.tex Sat Jul 23 18:47:12 2011 +0200
2.2 +++ b/doc-src/isac/jrocnik/vorlage-bakkarbeit.tex Sun Jul 24 19:38:53 2011 +0200
2.3 @@ -77,7 +77,7 @@
2.4
2.5 \begin{figure} [htb]
2.6 \begin{center}
2.7 - \includegraphics[width=120mm]{overview.pdf}
2.8 +% \includegraphics[width=120mm]{overview.pdf}
2.9 \end{center}
2.10 \caption{Lucas-interpreter und Isabelle}
2.11 \label{architektur}