doc-src/isac/jrocnik/present-1.tex
branchdecompose-isar
changeset 42163 3bf084f80641
parent 42159 9d8a198bb471
child 42173 f12d4153b305
     1.1 --- a/doc-src/isac/jrocnik/present-1.tex	Fri Jul 22 10:26:39 2011 +0200
     1.2 +++ b/doc-src/isac/jrocnik/present-1.tex	Fri Jul 22 12:07:01 2011 +0200
     1.3 @@ -23,10 +23,10 @@
     1.4  \def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
     1.5  \def\sisac{{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}}
     1.6  
     1.7 -\title[TODO] % (optional, use only with long paper titles)
     1.8 -{TODO}
     1.9 +\title[SPSC in \isac] % (optional, use only with long paper titles)
    1.10 +{Interactive Course Material\\ for Signal Processing\\ based on Isabelle/\isac}
    1.11  
    1.12 -\subtitle{TODO}
    1.13 +\subtitle{Baccalaureate Thesis}
    1.14  
    1.15  \author[Rocnik] % (optional, use only with lots of authors)
    1.16  {Jan~Rocnik}
    1.17 @@ -102,6 +102,30 @@
    1.18  %%---------------------------------------------------------------%%
    1.19  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    1.20  
    1.21 +\section[Intro]{Introduction}
    1.22 +
    1.23 +\begin{frame}{Introduction}
    1.24 +Issues to be accomplished in this thesis:
    1.25 +
    1.26 +\begin{itemize}
    1.27 +
    1.28 +\item What knowledge is already mechanised in \emph{isabelle}?
    1.29 +\item How can missing theorems and definitions be mechanised?
    1.30 +\item What is the effort for such mechanisation?
    1.31 +\item How do calculations look like, if using mechanised knowledge?
    1.32 +\item What are the problems and subproblems to be solved?
    1.33 +\item Which problems are already implemented in \sisac?
    1.34 +\item How are the new Problems specified rigorously (\sisac)?
    1.35 +\item Which variantes of programms in \sisac{} solving the problems?
    1.36 +\item What is the contents of the interactiv course material (Figures, etc.)?
    1.37 +
    1.38 +\end{itemize}
    1.39 +\end{frame}
    1.40 +
    1.41 +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    1.42 +%%---------------------------------------------------------------%%
    1.43 +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    1.44 +
    1.45  \section[Fourier]{Fourier transform}
    1.46  
    1.47  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    1.48 @@ -181,7 +205,7 @@
    1.49  \begin{center}
    1.50  $x(t)= \left\{
    1.51       \begin{array}{lr}
    1.52 -       1 & -1\leq t\geq1\\
    1.53 +       1 & -1\leq t\leq1\\
    1.54         0 & else
    1.55       \end{array}
    1.56     \right.$
    1.57 @@ -254,6 +278,23 @@
    1.58  MT --- thesis ``Integrals'' (mathematics)
    1.59  }
    1.60  \end{frame}
    1.61 +
    1.62 +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    1.63 +%%--------------------FOURIER---Conclusion-----------------------%%
    1.64 +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    1.65 +
    1.66 +%\subsection[Summary]{Summary}
    1.67 +
    1.68 +\begin{frame}{Summary}
    1.69 +todo
    1.70 +
    1.71 +\begin{itemize}
    1.72 +
    1.73 +\item todo
    1.74 +
    1.75 +\end{itemize}
    1.76 +\end{frame}
    1.77 +
    1.78  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    1.79  %-----------------------------------------------------------------%
    1.80  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    1.81 @@ -421,7 +462,6 @@
    1.82  }
    1.83  \end{frame}
    1.84  
    1.85 -
    1.86  \end{document}
    1.87  
    1.88