e0726734@42027: % $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 $
e0726734@42027: 
e0726734@42027: \documentclass{beamer}
e0726734@42027: 
e0726734@42027: % This file is a solution template for:
e0726734@42027: 
e0726734@42027: % - Talk at a conference/colloquium.
e0726734@42027: % - Talk length is about 20min.
e0726734@42027: % - Style is ornate.
e0726734@42027: 
e0726734@42027: 
e0726734@42027: 
e0726734@42027: % Copyright 2004 by Till Tantau <tantau@users.sourceforge.net>.
e0726734@42027: %
e0726734@42027: % In principle, this file can be redistributed and/or modified under
e0726734@42027: % the terms of the GNU Public License, version 2.
e0726734@42027: %
e0726734@42027: % However, this file is supposed to be a template to be modified
e0726734@42027: % for your own needs. For this reason, if you use this file as a
e0726734@42027: % template and not specifically distribute it as part of a another
e0726734@42027: % package/program, I grant the extra permission to freely copy and
e0726734@42027: % modify this file as you see fit and even to delete this copyright
e0726734@42027: % notice.
e0726734@42027: 
e0726734@42027: 
e0726734@42027: \mode<presentation>
e0726734@42027: {
e0726734@42027:   \usetheme{Hannover}
e0726734@42027:   % or ...
e0726734@42027: 
e0726734@42027:   \setbeamercovered{transparent}
e0726734@42027:   % or whatever (possibly just delete it)
e0726734@42027: }
e0726734@42027: 
e0726734@42027: \usepackage[english]{babel}
e0726734@42027: % or whatever
e0726734@42027: 
e0726734@42027: \usepackage[utf8]{inputenc}
e0726734@42027: % or whatever
e0726734@42027: 
e0726734@42027: \usepackage{times}
e0726734@42027: \usepackage[T1]{fontenc}
e0726734@42027: % Or whatever. Note that the encoding and the font should match. If T1
e0726734@42027: % does not look nice, try deleting the line with the fontenc.
e0726734@42027: 
e0726734@42027: \def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
e0726734@42027: \def\sisac{{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}}
e0726734@42027: 
e0726734@42027: \title[\isac: Computation \& Deduction] % (optional, use only with long paper titles)
e0726734@42027: {Integrating Computation and Deduction\\
e0726734@42027:   in the \isac-System}
e0726734@42027: 
e0726734@42027: \subtitle{Projektpraktikum: Introducing Isabelle's Contexts}
e0726734@42027: 
e0726734@42027: \author[Lehnfeld, Neuper] % (optional, use only with lots of authors)
e0726734@42027: {Mathias~Lehnfeld\inst{1} \and Walther~Neuper\inst{2}}
e0726734@42027: % - Give the names in the same order as the appear in the paper.
e0726734@42027: % - Use the \inst{?} command only if the authors have different
e0726734@42027: %   affiliation.
e0726734@42027: 
e0726734@42027: \institute % (optional, but mostly needed)
e0726734@42027: {
e0726734@42027:   \inst{1}%
e0726734@42027:   Vienna University of Technology
e0726734@42027:   \and
e0726734@42027:   \inst{2}%
e0726734@42027:   Institute of Software Technology\\
e0726734@42027:   Graz University of Technology
e0726734@42027: }
e0726734@42027: % - Use the \inst command only if there are several affiliations.
e0726734@42027: % - Keep it simple, no one is interested in your street address.
e0726734@42027: 
e0726734@42027: % \date[CFP 2003] % (optional, should be abbreviation of conference name)
e0726734@42027: % {Conference on Fabulous Presentations, 2003}
e0726734@42027: % - Either use conference name or its abbreviation.
e0726734@42027: % - Not really informative to the audience, more for people (including
e0726734@42027: %   yourself) who are reading the slides online
e0726734@42027: 
e0726734@42027: % \subject{Theoretical Computer Science}
e0726734@42027: % This is only inserted into the PDF information catalog. Can be left
e0726734@42027: % out.
e0726734@42027: 
e0726734@42027: 
e0726734@42027: 
e0726734@42027: % If you have a file called "university-logo-filename.xxx", where xxx
e0726734@42027: % is a graphic format that can be processed by latex or pdflatex,
e0726734@42027: % resp., then you can add a logo as follows:
e0726734@42027: 
e0726734@42027: % \pgfdeclareimage[height=0.5cm]{university-logo}{university-logo-filename}
e0726734@42027: % \logo{\pgfuseimage{university-logo}}
e0726734@42027: 
e0726734@42027: 
e0726734@42027: 
e0726734@42027: % Delete this, if you do not want the table of contents to pop up at
e0726734@42027: % the beginning of each subsection:
e0726734@42027: \AtBeginSubsection[]
e0726734@42027: {
e0726734@42027:   \begin{frame}<beamer>{Outline}
e0726734@42027:     \tableofcontents[currentsection,currentsubsection]
e0726734@42027:   \end{frame}
e0726734@42027: }
e0726734@42027: 
e0726734@42027: 
e0726734@42027: % If you wish to uncover everything in a step-wise fashion, uncomment
e0726734@42027: % the following command:
e0726734@42027: 
e0726734@42027: %\beamerdefaultoverlayspecification{<+->}
e0726734@42027: 
e0726734@42027: 
e0726734@42027: \begin{document}
e0726734@42027: 
e0726734@42027: \begin{frame}
e0726734@42027:   \titlepage
e0726734@42027: \end{frame}
e0726734@42027: 
e0726734@42027: \begin{frame}{Outline}
e0726734@42027:   \tableofcontents
e0726734@42027:   % You might wish to add the option [pausesections]
e0726734@42027: \end{frame}
e0726734@42027: 
e0726734@42027: 
e0726734@42027: % Structuring a talk is a difficult task and the following structure
e0726734@42027: % may not be suitable. Here are some rules that apply for this
e0726734@42027: % solution:
e0726734@42027: 
e0726734@42027: % - Exactly two or three sections (other than the summary).
e0726734@42027: % - At *most* three subsections per section.
e0726734@42027: % - Talk about 30s to 2min per frame. So there should be between about
e0726734@42027: %   15 and 30 frames, all told.
e0726734@42027: 
e0726734@42027: % - A conference audience is likely to know very little of what you
e0726734@42027: %   are going to talk about. So *simplify*!
e0726734@42027: % - In a 20min talk, getting the main ideas across is hard
e0726734@42027: %   enough. Leave out details, even if it means being less precise than
e0726734@42027: %   you think necessary.
e0726734@42027: % - If you omit details that are vital to the proof/implementation,
e0726734@42027: %   just say so once. Everybody will be happy with that.
e0726734@42027: 
e0726734@42027: \section[Deduction - Isabelle]{Deduction - The Theorem Prover Isabelle}
e0726734@42027: 
e0726734@42027: \subsection[CTP]{Computer Theorem Proving (CTP)}
e0726734@42027: 
e0726734@42027: \begin{frame}{Computer Theorem Proving (CTP)}
e0726734@42027:   % - A title should summarize the slide in an understandable fashion
e0726734@42027:   %   for anyone how does not follow everything on the slide itself.
e0726734@42027: 
e0726734@42027:   \begin{itemize}
e0726734@42027:   \item USA: ACL, PVS
e0726734@42027:   \item EU: Isabelle, Coq
e0726734@42027:   \item history: see 101118-risc.
e0726734@42027:   \item SW-engineering: program verification, proof obligations proven automatically (ATP), some interactively
e0726734@42027:   \item interactive provers comprise ATPs
e0726734@42027:   \end{itemize}
e0726734@42027: \end{frame}
e0726734@42027: 
e0726734@42027: 
e0726734@42027: \subsection{Isabelle/Isar}
e0726734@42027: 
e0726734@42027: \begin{frame}{Isabelle/Isar}
e0726734@42027: Wikipedia \href{http://en.wikipedia.org/wiki/Isabelle_(theorem_prover)\\\#Example_proof}{Demo}\\
e0726734@42027: lines of code: Pure/  Sequents/ Tools/  Provers/ \\
e0726734@42027: in Knowledge/: everything else
e0726734@42027: \end{frame}
e0726734@42027: 
e0726734@42027: \begin{frame}{Contexts}
e0726734@42027: 	\begin{itemize}
e0726734@42027: 	\item represent background for composing proofs
e0726734@42027: 	\item contain declarations, results, ...
e0726734@42027: 	\item created from theories
e0726734@42027: 	\item theories are explicitly named data containers
e0726734@42027: 	\end{itemize}
e0726734@42027: \end{frame}
e0726734@42027: 
e0726734@42027: \section[\isac-System]{Computation - \isac-System}
e0726734@42027: 
e0726734@42027: \subsection{Features of the \isac-System}
e0726734@42027: 
e0726734@42027: \begin{frame}{Computation}
e0726734@42027: \begin{enumerate}
e0726734@42027: \item \alert{guides the user} step by step towards a solution\\
e0726734@42027: \uncover<2->{\textit{
e0726734@42027: Watching teachers calculate step by step is boring.\\
e0726734@42027: Operating on formulas by hand is hard, too.\\
e0726734@42027: Software can support {\bf independent learning}.
e0726734@42027: }}
e0726734@42027: \item \alert{checks user input} as generous and liberal as possible\\
e0726734@42027: \uncover<3->{\textit{
e0726734@42027: Active learning by {\bf trial and error} is most effective.\\
e0726734@42027: Programmers cannot foresee learners' input.\\
e0726734@42027: Theorem provers provide most general checking.
e0726734@42027: }}
e0726734@42027: \item \alert{explains steps} on request by the user\\
e0726734@42027: \uncover<4->{\textit{
e0726734@42027: Programmers also cannot foresee learners' questions.\\
e0726734@42027: A system must be {\bf transparent} for casual questions.\\
e0726734@42027: LCF-style provers have human readable knowledge.
e0726734@42027: }}
e0726734@42027: \end{enumerate}
e0726734@42027: \end{frame}
e0726734@42027: 
e0726734@42027: \subsection{Lucas-Interpretation - Deduction \& Computation}
e0726734@42027: \begin{frame}{Lucas-Interpretation - Deduction \& Computation}
e0726734@42027: 
e0726734@42027: \end{frame}
e0726734@42027: 
e0726734@42027: 
e0726734@42027: \begin{frame}{Title?}
e0726734@42027: \includegraphics[width=100mm]{overview.png}
e0726734@42027: \end{frame}
e0726734@42027: 
e0726734@42027: 
e0726734@42027: graphics movie
e0726734@42027: 
e0726734@42027: %\begin{frame}{Make Titles Informative.}
e0726734@42027: %\end{frame}
e0726734@42027: 
e0726734@42027: 
e0726734@42027: %\subsection{Introduction of Isabelle's Context to \isac}
e0726734@42027: 
e0726734@42027: %\begin{frame}{Make Titles Informative.}
e0726734@42027: %\end{frame}
e0726734@42027: 
e0726734@42027: %\begin{frame}{Make Titles Informative.}
e0726734@42027: %\end{frame}
e0726734@42027: 
e0726734@42027: %\begin{frame}{Make Titles Informative.}
e0726734@42027: %\end{frame}
e0726734@42027: 
e0726734@42027: 
e0726734@42027: 
e0726734@42027: \section*{Summary}
e0726734@42027: 
e0726734@42027: \begin{frame}{Summary}
e0726734@42027: 
e0726734@42027:   % Keep the summary *very short*.
e0726734@42027:   \begin{itemize}
e0726734@42027:   \item
e0726734@42027:     The \alert{first main message} of your talk in one or two lines.
e0726734@42027:   \item
e0726734@42027:     The \alert{second main message} of your talk in one or two lines.
e0726734@42027:   \item
e0726734@42027:     Perhaps a \alert{third message}, but not more than that.
e0726734@42027:   \end{itemize}
e0726734@42027: 
e0726734@42027:   % The following outlook is optional.
e0726734@42027:   \vskip0pt plus.5fill
e0726734@42027:   \begin{itemize}
e0726734@42027:   \item
e0726734@42027:     Outlook
e0726734@42027:     \begin{itemize}
e0726734@42027:     \item
e0726734@42027:       Something you haven't solved.
e0726734@42027:     \item
e0726734@42027:       Something else you haven't solved.
e0726734@42027:     \end{itemize}
e0726734@42027:   \end{itemize}
e0726734@42027: \end{frame}
e0726734@42027: 
e0726734@42027: 
e0726734@42027: 
e0726734@42027: % All of the following is optional and typically not needed.
e0726734@42027: \appendix
e0726734@42027: \section<presentation>*{\appendixname}
e0726734@42027: \subsection<presentation>*{For Further Reading}
e0726734@42027: 
e0726734@42027: \begin{frame}[allowframebreaks]
e0726734@42027:   \frametitle<presentation>{For Further Reading}
e0726734@42027: 
e0726734@42027:   \begin{thebibliography}{10}
e0726734@42027: 
e0726734@42027:   \beamertemplatebookbibitems
e0726734@42027:   % Start with overview books.
e0726734@42027: 
e0726734@42027:   \bibitem{Author1990}
e0726734@42027:     A.~Author.
e0726734@42027:     \newblock {\em Handbook of Everything}.
e0726734@42027:     \newblock Some Press, 1990.
e0726734@42027: 
e0726734@42027: 
e0726734@42027:   \beamertemplatearticlebibitems
e0726734@42027:   % Followed by interesting articles. Keep the list short.
e0726734@42027: 
e0726734@42027:   \bibitem{Someone2000}
e0726734@42027:     S.~Someone.
e0726734@42027:     \newblock On this and that.
e0726734@42027:     \newblock {\em Journal of This and That}, 2(1):50--100,
e0726734@42027:     2000.
e0726734@42027:   \end{thebibliography}
e0726734@42027: \end{frame}
e0726734@42027: 
e0726734@42027: \end{document}
e0726734@42027: 
e0726734@42027: