wneuper/isa: doc-isac/jrocnik/final/jrocnik

     2 \documentclass{beamer}

     5 \mode<presentation>

6 {

     7   \usetheme{Hannover}

     8   \setbeamercovered{transparent}

9 }

    11 \usepackage[english]{babel}

    12 \usepackage[utf8]{inputenc}

    13 \usepackage{times}

    14 \usepackage[T1]{fontenc}

    16 \def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}

    17 \def\sisac{{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}}

    19 \title[SPSC in \isac] % (optional, use only with long paper titles)

    20 {Interactive Course Material\\ for Signal Processing\\ based on Isabelle/\isac}

    22 \subtitle{Baccalaureate Thesis}

    24 \author[Ro\v{c}nik]

    25 {Jan Rocnik}

    27 \institute % (optional, but mostly needed)

    28 {

    29   Technische Universit\"at Graz\\

    30   Institut f\"ur TODO

    31 }

    33 % If you have a file called "university-logo-filename.xxx", where xxx

    34 % is a graphic format that can be processed by latex or pdflatex,

    35 % resp., then you can add a logo as follows:

    37 % \pgfdeclareimage[height=0.5cm]{university-logo}{university-logo-filename}

    38 % \logo{\pgfuseimage{university-logo}}

    42 % Delete this, if you do not want the table of contents to pop up at

    43 % the beginning of each subsection:

    44 \AtBeginSubsection[]

    45 {

    46   \begin{frame}<beamer>{Outline}

    47     \tableofcontents[currentsection,currentsubsection]

    48   \end{frame}

    49 }

    51 \begin{document}

    53 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    54 %%												Title Page                             %%

    55 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    57 \begin{frame}

    58   \titlepage

    59 \end{frame}

    61 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    62 %%												Table of Contents                      %%

    63 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    65 \begin{frame}{Outline}

    66   \tableofcontents

    67   % You might wish to add the option [pausesections]

    68 \end{frame}

    70 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    71 %%---------------------------------------------------------------%%

    72 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    74 \section[Intro]{Introduction}

    76 \begin{frame}{Issues to be Accomplished}

    78 \begin{itemize}

    80 \item What knowledge is already mechanised in \emph{Isabelle}?

    81 \item How can missing theorems and definitions be mechanised?

    82 \item What is the effort for such mechanisation?

    83 \item How do calculations look like, by using mechanised knowledge?

    84 \item What problems and subproblems have to be solved?

    85 \item Which problems are already implemented in \sisac?

    86 \item How are the new problems specified (\sisac)?

    87 \item Which variantes of programms in \sisac\ solve the problems?

    88 \item What is the contents of the interactiv course material (Figures, etc.)?

    90 \end{itemize}

    91 \end{frame}

    93 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    94 %%---------------------------------------------------------------%%

    95 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    97 \section[Fourier]{Fourier transformation}

    98 \subsection[Fourier]{Fourier transform}

   100 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   101 %%												Fourier INTRO                          %%

   102 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   104 \begin{frame}\frametitle{Fourier Transformation: Introduction}

   105 Possibilities:

   106 \begin{itemize}

   107 \item Transform operation by using property-tables

   108 \item Transform operation by using integral

   109 \end{itemize}

   110 Also Important:

   111 \begin{itemize}

   112 \item Visualisation?!

   113 \end{itemize}

   114 \end{frame}

   116 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   117 %%										Transform expl   SPEC                      %%

   118 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   120 \begin{frame}\frametitle{Fourier Transformation: Specification}

   121 {\footnotesize

   123 Determine the fourier transform for the given rectangular impulse:

   125 \begin{center}

   126 $x(t)= \left\{

   127      \begin{array}{lr}

   128        1 & -1\leq t\leq1\\

   129        0 & else

   130      \end{array}

   131    \right.$

   132 \end{center}

   134 \hrulefill

   136 \begin{tabbing}

   137 1\=postcond \=: \= \= $\;\;\;\;$\=\kill

   138 \>given    \>:\>  piecewise\_function \\

   139 \>         \> \>  \>$fun (x (t::real),\ x=1\ ((t>=-1)\ \&\ (t<=1)),\ x=0)$\\

   140 \>precond  \>:\>  TODO\\

   141 \>find     \>:\>  $X(j\cdot\omega)$\\

   142 \>postcond \>:\>  TODO\\

   143 \end{tabbing}

   145 }

   146 \end{frame}

   148 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   149 %%												Transform expl   REQ                   %%

   150 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   152 \begin{frame}\frametitle{Fourier Transform: Development effort}

   153 {\small

   154 \begin{center}

   155 \begin{tabular}{l|l|r}

   156 requirements            & comments             &effort\\ \hline\hline

   157 solving Intrgrals		    & simple via propertie table     &     20\\

   158                         & \emph{real}          &    MT\\ \hline

   159 transformation table    & simple transform     &    20\\ \hline

   160 visualisation						& backend							 &    10\\ \hline

   161 example collection      & with explanations    &    20\\ \hline\hline

   162                         &                      & 70-80\\

   163 \end{tabular}

   164 \end{center}

   165 effort --- in 45min units\\

   166 MT --- thesis ``Integrals'' (mathematics)

   167 }

   168 \end{frame}

   170 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   171 %%--------------------FOURIER---Conclusion-----------------------%%

   172 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   174 \begin{frame}{Fourier Transformation: Summary}

   175 \begin{itemize}

   177 \item Standard integrals can be solved with tables

   178 \item No real integration (yet avaible)

   179 \item Math \emph{tricks} difficult to implement

   182 \end{itemize}

   183 \end{frame}

   185 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   186 %-----------------------------------------------------------------%

   187 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   189 \section[LTI Systems]{LTI systems}

   190 \subsection[Convolution]{Convolution (Faltung)}

   192 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   193 %%												LTI INTRO				                       %%

   194 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   196 \begin{frame}\frametitle{Convolution: Introduction}

   197 \begin{itemize}

   198 \item Calculation include sums

   199 \item Demonstrative examples

   200 \item Visualisation is important

   201 \end{itemize}

   202 \end{frame}

   204 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   205 %%												LTI SPEC				                       %%

   206 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   208 \begin{frame}\frametitle{Convolution: Specification}

   209 {\footnotesize

   211 Consider the two discrete-time, linear and time-invariant (LTI) systems with the following impulse response:

   213 \begin{center}

   214 $h_1[n]=\left(\frac{3}{5}\right)^n\cdot u[n]$\\

   215 $h_1[n]=\left(-\frac{2}{3}\right)^n\cdot u[n]$

   216 \end{center}

   218 The two systems are cascaded seriell. Derive the impulse respinse of the overall system $h_c[n]$.

   220 \hrulefill

   222 \begin{tabbing}

   223 1\=postcond \=: \= \= $\;\;\;\;$\=\kill

   224 \>given    \>:\>  Signals h1[n], h2[n] \\

   225 \>         \> \>  \>((h1[n]=(3/5)\textasciicircum{}n*u[n]),\,h2[n]=(-2/3)\textasciicircum{}n*u[n]))\\

   227 \>precond  \>:\>  TODO\\

   228 \>find     \>:\>  $h1[n]\,*\,h2[n]$\\

   229 \>postcond \>:\>  TODO\\

   230 \end{tabbing}

   232 }

   233 \end{frame}

   235 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   236 %%												LTI REQ  				                       %%

   237 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   239 \begin{frame}\frametitle{Convolution: Development effort}

   240 {\small

   241 \begin{center}

   242 \begin{tabular}{l|l|r}

   243 requirements            & comments             &effort\\ \hline\hline

   244 simplify rationals      & \sisac               &     0\\ \hline

   245 define $\sum\limits_{i=0}^{n}i$ & partly \sisac  &    10\\ \hline

   246 simplify sum			      & termorder            &    10\\

   247                         & simplify rules       &    20\\

   248                         & use simplify rationals&     0\\ \hline

   249 index adjustments       & with unit step       &      10\\ \hline

   250 example collection      & with explanations    &    20\\ \hline\hline

   251                         &                      & 70-90\\

   252 \end{tabular}

   253 \end{center}

   254 effort --- in 45min units\\

   255 }

   256 \end{frame}

   258 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   259 %%--------------------LTI-------Conclusion-----------------------%%

   260 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   262 \begin{frame}{Convolution: Summary}

   263 \begin{itemize}

   265 \item Standard example

   266 \item Straight forward

   267 \item Challenge are sum limits

   269 \end{itemize}

   270 \end{frame}

   272 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   273 %-----------------------------------------------------------------%

   274 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   276 \section[Z-transform]{Z-Transform}

   277 \subsection[(Inverse) Z-Transform]{(Inverse) Z-Transform}

   279 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   280 %%												Z-Transform  INTRO                     %%

   281 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   283 \begin{frame}\frametitle{(Inverse) ${\cal Z}$-Transformation: Introduction}

   284 \begin{itemize}

   285 \item Pure Transformation is simple to realise with Z-Transform Properties (Table)

   286 \item Partial Fraction are just math simplifications

   287 \end{itemize}

   288 \end{frame}

   290 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   291 %%												Z-Transform  SPEC                      %%

   292 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   294 \begin{frame}\frametitle{(Inverse) Z-Transformation: Specification}

   295 {\footnotesize

   297 Determine the inverse z transform of the following expression. Hint: applay the partial fraction expansion.

   299 \begin{center}

   300 $X(z)=\frac{3}{z-\frac{1}{4}-\frac{1}{8}z^{-1}},\ \ x[n]$ is absolute summable

   301 \end{center}

   304 \hrulefill

   306 \begin{tabbing}

   307 1\=postcond \=: \= \= $\;\;\;\;$\=\kill

   308 \>given    \>:\>  Expression of z \\

   309 \>         \> \>  \>(X (z::complex),3/(z-1/4-1/8\,z\textasciicircum{}(-1)))\\

   310 \>precond  \>:\>  TODO\\

   311 \>find     \>:\>  Expression of n\\

   312 \>         \> \>  \>$h[n]$\\

   313 \>postcond \>:\>  TODO\\

   314 \end{tabbing}

   316 }

   317 \end{frame}

   319 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   320 %%												Z expl		REQ	                         %%

   321 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   324 \begin{frame}\frametitle{(Inverse) Z-Transformation: Development effort}

   325 {\small

   326 \begin{center}

   327 \begin{tabular}{l|l|r}

   328 requirements            & comments             &effort\\ \hline\hline

   329 solve for part.fract.   & \sisac: degree 2     &     0\\

   330                         & complex nomminators  &    30\\

   331                         & degree > 2           &    MT\\ \hline

   332 simplify polynomial     & \sisac               &     0\\

   333 simplify rational       & \sisac               &     0\\ \hline

   334 part.fract.decomposition& degree 2             &      \\

   335                         & specification, method&    30\\ \hline

   336 ${\cal Z}^{-1}$ table    &                       &   20\\

   337                         & explanations, figures&    20\\ \hline

   338 example collection      & with explanations    &    20\\ \hline\hline

   339                         &                      & 90-120\\

   340 %                        &                      & 1 MT

   341 \end{tabular}

   342 \end{center}

   343 effort --- in 45min units\\

   344 MT --- thesis ``factorization'' (mathematics)

   345 }

   346 \end{frame}

   348 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   349 %%--------------------Z-TRANS---Conclusion-----------------------%%

   350 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   352 \begin{frame}{(Inverse) Z-Transformation: Summary}

   353 \begin{itemize}

   355 \item No \emph{higher} math operations

   356 \item Different subproblems of math (equation systems, etc.)

   357 \item Both directions have the same effort

   359 \end{itemize}

   360 \end{frame}

   362 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   363 %-----------------------------------------------------------------%

   364 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   366 \section[Conclusions]{Conclusions}

   368 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   369 %--------------------------DEMONSTRATION--------------------------%

   370 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   372 \begin{frame}{Demonstration}

   374 \centering{Demonstration}

   376 \end{frame}

   378 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   379 %--------------------------CONCLUSION-----------------------------%

   380 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   382 \begin{frame}{Conclusions}

   384 Design Challanges:

   386 {\small

   387 \begin{itemize}

   389 \item Pre and Post conditions

   390 \item Exact mathematic behind functions

   391 \item Accurate mathematic notation

   393 \end{itemize}

   394 }

   396 Goals:

   397 {\small

   398 \begin{itemize}

   400 \item Spot the power of \sisac

   401 \item Implementation of generell but simple math problems

   402 \item Setting up a good first guideline (documentation) for furher problem implemenations

   404 \end{itemize}

   406 \centering{Efforts are only approximations, due we have no \emph{real} experience data!}

   407 }

   409 \end{frame}

   411 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   412 %--------------------------TIME LINE------------------------------%

   413 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   415 \begin{frame}{Comming up}

   417 {\small

   418 \begin{tabular}{l r}

   420 Juli 2011 & project startup\\

   421 Juli 2011 & information collection, 1st presentation\\

   422 August 2011 & extern traineeship\\

   423 September 2011 & main work\\

   424 after Oktober & finishing, documentation\\

   426 \end{tabular}

   427 }

   429 \end{frame}

   432 \end{document}

author	Walther Neuper <neuper@ist.tugraz.at>
	Tue, 17 Sep 2013 09:50:52 +0200
changeset 52107	f8845fc8f38d
parent 52058	src/Doc/isac/jrocnik/final/jrocnik_present1.tex@83aff4cb984a
permissions	-rwxr-xr-x