1.1 Binary file doc-src/isac/mlehnfeld/overview.odg has changed

     2.1 Binary file doc-src/isac/mlehnfeld/overview.png has changed

     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/doc-src/isac/mlehnfeld/presentation.tex	Fri May 27 12:04:21 2011 +0200
     3.3 @@ -0,0 +1,293 @@
     3.4 +% $Header: /cvsroot/latex-beamer/latex-beamer/solutions/conference-talks/conference-ornate-20min.en.tex,v 1.7 2007/01/28 20:48:23 tantau Exp $
     3.5 +
     3.6 +\documentclass{beamer}
     3.7 +
     3.8 +% This file is a solution template for:
     3.9 +
    3.10 +% - Talk at a conference/colloquium.
    3.11 +% - Talk length is about 20min.
    3.12 +% - Style is ornate.
    3.13 +
    3.14 +
    3.15 +
    3.16 +% Copyright 2004 by Till Tantau <tantau@users.sourceforge.net>.
    3.17 +%
    3.18 +% In principle, this file can be redistributed and/or modified under
    3.19 +% the terms of the GNU Public License, version 2.
    3.20 +%
    3.21 +% However, this file is supposed to be a template to be modified
    3.22 +% for your own needs. For this reason, if you use this file as a
    3.23 +% template and not specifically distribute it as part of a another
    3.24 +% package/program, I grant the extra permission to freely copy and
    3.25 +% modify this file as you see fit and even to delete this copyright
    3.26 +% notice.
    3.27 +
    3.28 +
    3.29 +\mode<presentation>
    3.30 +{
    3.31 +  \usetheme{Hannover}
    3.32 +  % or ...
    3.33 +
    3.34 +  \setbeamercovered{transparent}
    3.35 +  % or whatever (possibly just delete it)
    3.36 +}
    3.37 +
    3.38 +\usepackage[english]{babel}
    3.39 +% or whatever
    3.40 +
    3.41 +\usepackage[utf8]{inputenc}
    3.42 +% or whatever
    3.43 +
    3.44 +\usepackage{times}
    3.45 +\usepackage[T1]{fontenc}
    3.46 +% Or whatever. Note that the encoding and the font should match. If T1
    3.47 +% does not look nice, try deleting the line with the fontenc.
    3.48 +
    3.49 +\def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
    3.50 +\def\sisac{{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}}
    3.51 +
    3.52 +\title[\isac: Computation \& Deduction] % (optional, use only with long paper titles)
    3.53 +{Integrating Computation and Deduction\\
    3.54 +  in the \isac-System}
    3.55 +
    3.56 +\subtitle{Projektpraktikum: Introducing Isabelle's Contexts}
    3.57 +
    3.58 +\author[Lehnfeld, Neuper] % (optional, use only with lots of authors)
    3.59 +{Mathias~Lehnfeld\inst{1} \and Walther~Neuper\inst{2}}
    3.60 +% - Give the names in the same order as the appear in the paper.
    3.61 +% - Use the \inst{?} command only if the authors have different
    3.62 +%   affiliation.
    3.63 +
    3.64 +\institute % (optional, but mostly needed)
    3.65 +{
    3.66 +  \inst{1}%
    3.67 +  Vienna University of Technology
    3.68 +  \and
    3.69 +  \inst{2}%
    3.70 +  Institute of Software Technology\\
    3.71 +  Graz University of Technology
    3.72 +}
    3.73 +% - Use the \inst command only if there are several affiliations.
    3.74 +% - Keep it simple, no one is interested in your street address.
    3.75 +
    3.76 +% \date[CFP 2003] % (optional, should be abbreviation of conference name)
    3.77 +% {Conference on Fabulous Presentations, 2003}
    3.78 +% - Either use conference name or its abbreviation.
    3.79 +% - Not really informative to the audience, more for people (including
    3.80 +%   yourself) who are reading the slides online
    3.81 +
    3.82 +% \subject{Theoretical Computer Science}
    3.83 +% This is only inserted into the PDF information catalog. Can be left
    3.84 +% out.
    3.85 +
    3.86 +
    3.87 +
    3.88 +% If you have a file called "university-logo-filename.xxx", where xxx
    3.89 +% is a graphic format that can be processed by latex or pdflatex,
    3.90 +% resp., then you can add a logo as follows:
    3.91 +
    3.92 +% \pgfdeclareimage[height=0.5cm]{university-logo}{university-logo-filename}
    3.93 +% \logo{\pgfuseimage{university-logo}}
    3.94 +
    3.95 +
    3.96 +
    3.97 +% Delete this, if you do not want the table of contents to pop up at
    3.98 +% the beginning of each subsection:
    3.99 +\AtBeginSubsection[]
   3.100 +{
   3.101 +  \begin{frame}<beamer>{Outline}
   3.102 +    \tableofcontents[currentsection,currentsubsection]
   3.103 +  \end{frame}
   3.104 +}
   3.105 +
   3.106 +
   3.107 +% If you wish to uncover everything in a step-wise fashion, uncomment
   3.108 +% the following command:
   3.109 +
   3.110 +%\beamerdefaultoverlayspecification{<+->}
   3.111 +
   3.112 +
   3.113 +\begin{document}
   3.114 +
   3.115 +\begin{frame}
   3.116 +  \titlepage
   3.117 +\end{frame}
   3.118 +
   3.119 +\begin{frame}{Outline}
   3.120 +  \tableofcontents
   3.121 +  % You might wish to add the option [pausesections]
   3.122 +\end{frame}
   3.123 +
   3.124 +
   3.125 +% Structuring a talk is a difficult task and the following structure
   3.126 +% may not be suitable. Here are some rules that apply for this
   3.127 +% solution:
   3.128 +
   3.129 +% - Exactly two or three sections (other than the summary).
   3.130 +% - At *most* three subsections per section.
   3.131 +% - Talk about 30s to 2min per frame. So there should be between about
   3.132 +%   15 and 30 frames, all told.
   3.133 +
   3.134 +% - A conference audience is likely to know very little of what you
   3.135 +%   are going to talk about. So *simplify*!
   3.136 +% - In a 20min talk, getting the main ideas across is hard
   3.137 +%   enough. Leave out details, even if it means being less precise than
   3.138 +%   you think necessary.
   3.139 +% - If you omit details that are vital to the proof/implementation,
   3.140 +%   just say so once. Everybody will be happy with that.
   3.141 +
   3.142 +\section[Deduction - Isabelle]{Deduction - The Theorem Prover Isabelle}
   3.143 +
   3.144 +\subsection[CTP]{Computer Theorem Proving (CTP)}
   3.145 +
   3.146 +\begin{frame}{Computer Theorem Proving (CTP)}
   3.147 +  % - A title should summarize the slide in an understandable fashion
   3.148 +  %   for anyone how does not follow everything on the slide itself.
   3.149 +
   3.150 +  \begin{itemize}
   3.151 +  \item USA: ACL, PVS
   3.152 +  \item EU: Isabelle, Coq
   3.153 +  \item history: see 101118-risc.
   3.154 +  \item SW-engineering: program verification, proof obligations proven automatically (ATP), some interactively
   3.155 +  \item interactive provers comprise ATPs
   3.156 +  \end{itemize}
   3.157 +\end{frame}
   3.158 +
   3.159 +
   3.160 +\subsection{Isabelle/Isar}
   3.161 +
   3.162 +\begin{frame}{Isabelle/Isar}
   3.163 +Wikipedia \href{http://en.wikipedia.org/wiki/Isabelle_(theorem_prover)\\\#Example_proof}{Demo}\\
   3.164 +lines of code: Pure/  Sequents/ Tools/  Provers/ \\
   3.165 +in Knowledge/: everything else
   3.166 +\end{frame}
   3.167 +
   3.168 +\begin{frame}{Contexts}
   3.169 +	\begin{itemize}
   3.170 +	\item represent background for composing proofs
   3.171 +	\item contain declarations, results, ...
   3.172 +	\item created from theories
   3.173 +	\item theories are explicitly named data containers
   3.174 +	\end{itemize}
   3.175 +\end{frame}
   3.176 +
   3.177 +\section[\isac-System]{Computation - \isac-System}
   3.178 +
   3.179 +\subsection{Features of the \isac-System}
   3.180 +
   3.181 +\begin{frame}{Computation}
   3.182 +\begin{enumerate}
   3.183 +\item \alert{guides the user} step by step towards a solution\\
   3.184 +\uncover<2->{\textit{
   3.185 +Watching teachers calculate step by step is boring.\\
   3.186 +Operating on formulas by hand is hard, too.\\
   3.187 +Software can support {\bf independent learning}.
   3.188 +}}
   3.189 +\item \alert{checks user input} as generous and liberal as possible\\
   3.190 +\uncover<3->{\textit{
   3.191 +Active learning by {\bf trial and error} is most effective.\\
   3.192 +Programmers cannot foresee learners' input.\\
   3.193 +Theorem provers provide most general checking.
   3.194 +}}
   3.195 +\item \alert{explains steps} on request by the user\\
   3.196 +\uncover<4->{\textit{
   3.197 +Programmers also cannot foresee learners' questions.\\
   3.198 +A system must be {\bf transparent} for casual questions.\\
   3.199 +LCF-style provers have human readable knowledge.
   3.200 +}}
   3.201 +\end{enumerate}
   3.202 +\end{frame}
   3.203 +
   3.204 +\subsection{Lucas-Interpretation - Deduction \& Computation}
   3.205 +\begin{frame}{Lucas-Interpretation - Deduction \& Computation}
   3.206 +
   3.207 +\end{frame}
   3.208 +
   3.209 +
   3.210 +\begin{frame}{Title?}
   3.211 +\includegraphics[width=100mm]{overview.png}
   3.212 +\end{frame}
   3.213 +
   3.214 +
   3.215 +graphics movie
   3.216 +
   3.217 +%\begin{frame}{Make Titles Informative.}
   3.218 +%\end{frame}
   3.219 +
   3.220 +
   3.221 +%\subsection{Introduction of Isabelle's Context to \isac}
   3.222 +
   3.223 +%\begin{frame}{Make Titles Informative.}
   3.224 +%\end{frame}
   3.225 +
   3.226 +%\begin{frame}{Make Titles Informative.}
   3.227 +%\end{frame}
   3.228 +
   3.229 +%\begin{frame}{Make Titles Informative.}
   3.230 +%\end{frame}
   3.231 +
   3.232 +
   3.233 +
   3.234 +\section*{Summary}
   3.235 +
   3.236 +\begin{frame}{Summary}
   3.237 +
   3.238 +  % Keep the summary *very short*.
   3.239 +  \begin{itemize}
   3.240 +  \item
   3.241 +    The \alert{first main message} of your talk in one or two lines.
   3.242 +  \item
   3.243 +    The \alert{second main message} of your talk in one or two lines.
   3.244 +  \item
   3.245 +    Perhaps a \alert{third message}, but not more than that.
   3.246 +  \end{itemize}
   3.247 +
   3.248 +  % The following outlook is optional.
   3.249 +  \vskip0pt plus.5fill
   3.250 +  \begin{itemize}
   3.251 +  \item
   3.252 +    Outlook
   3.253 +    \begin{itemize}
   3.254 +    \item
   3.255 +      Something you haven't solved.
   3.256 +    \item
   3.257 +      Something else you haven't solved.
   3.258 +    \end{itemize}
   3.259 +  \end{itemize}
   3.260 +\end{frame}
   3.261 +
   3.262 +
   3.263 +
   3.264 +% All of the following is optional and typically not needed.
   3.265 +\appendix
   3.266 +\section<presentation>*{\appendixname}
   3.267 +\subsection<presentation>*{For Further Reading}
   3.268 +
   3.269 +\begin{frame}[allowframebreaks]
   3.270 +  \frametitle<presentation>{For Further Reading}
   3.271 +
   3.272 +  \begin{thebibliography}{10}
   3.273 +
   3.274 +  \beamertemplatebookbibitems
   3.275 +  % Start with overview books.
   3.276 +
   3.277 +  \bibitem{Author1990}
   3.278 +    A.~Author.
   3.279 +    \newblock {\em Handbook of Everything}.
   3.280 +    \newblock Some Press, 1990.
   3.281 +
   3.282 +
   3.283 +  \beamertemplatearticlebibitems
   3.284 +  % Followed by interesting articles. Keep the list short.
   3.285 +
   3.286 +  \bibitem{Someone2000}
   3.287 +    S.~Someone.
   3.288 +    \newblock On this and that.
   3.289 +    \newblock {\em Journal of This and That}, 2(1):50--100,
   3.290 +    2000.
   3.291 +  \end{thebibliography}
   3.292 +\end{frame}
   3.293 +
   3.294 +\end{document}
   3.295 +
   3.296 +