% $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 $

 \documentclass{beamer}

 % This file is a solution template for:

 % - Talk at a conference/colloquium.

 % - Talk length is about 20min.

 % - Style is ornate.

 % Copyright 2004 by Till Tantau <tantau@users.sourceforge.net>.

 %

 % In principle, this file can be redistributed and/or modified under

 % the terms of the GNU Public License, version 2.

 %

 % However, this file is supposed to be a template to be modified

 % for your own needs. For this reason, if you use this file as a

 % template and not specifically distribute it as part of a another

 % package/program, I grant the extra permission to freely copy and

 % modify this file as you see fit and even to delete this copyright

 % notice.

 \mode<presentation>

 {

   \usetheme{Hannover}

   % or ...

   \setbeamercovered{transparent}

   % or whatever (possibly just delete it)

 }

 \usepackage[english]{babel}

 % or whatever

 \usepackage[utf8]{inputenc}

 % or whatever

 \usepackage{times}

 \usepackage[T1]{fontenc}

 % Or whatever. Note that the encoding and the font should match. If T1

 % does not look nice, try deleting the line with the fontenc.

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

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

 \title[\isac: Computation \& Deduction] % (optional, use only with long paper titles)

 {Integrating Computation and Deduction\\

   in the \isac-System}

 \subtitle{Projektpraktikum: Introducing Isabelle's Contexts}

 \author[Lehnfeld, Neuper] % (optional, use only with lots of authors)

 {Mathias~Lehnfeld\inst{1} \and Walther~Neuper\inst{2}}

 % - Give the names in the same order as the appear in the paper.

 % - Use the \inst{?} command only if the authors have different

 %   affiliation.

 \institute % (optional, but mostly needed)

 {

   \inst{1}%

   Vienna University of Technology

   \and

   \inst{2}%

   Institute of Software Technology\\

   Graz University of Technology

 }

 % - Use the \inst command only if there are several affiliations.

 % - Keep it simple, no one is interested in your street address.

 % \date[CFP 2003] % (optional, should be abbreviation of conference name)

 % {Conference on Fabulous Presentations, 2003}

 % - Either use conference name or its abbreviation.

 % - Not really informative to the audience, more for people (including

 %   yourself) who are reading the slides online

 % \subject{Theoretical Computer Science}

 % This is only inserted into the PDF information catalog. Can be left

 % out.

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

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

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

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

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

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

 % the beginning of each subsection:

 \AtBeginSubsection[]

 {

   \begin{frame}<beamer>{Outline}

     \tableofcontents[currentsection,currentsubsection]

   \end{frame}

 }

 % If you wish to uncover everything in a step-wise fashion, uncomment

 % the following command:

 %\beamerdefaultoverlayspecification{<+->}

 \begin{document}

 \begin{frame}

   \titlepage

 \end{frame}

 \begin{frame}{Outline}

   \tableofcontents

   % You might wish to add the option [pausesections]

 \end{frame}

 % Structuring a talk is a difficult task and the following structure

 % may not be suitable. Here are some rules that apply for this

 % solution:

 % - Exactly two or three sections (other than the summary).

 % - At *most* three subsections per section.

 % - Talk about 30s to 2min per frame. So there should be between about

 %   15 and 30 frames, all told.

 % - A conference audience is likely to know very little of what you

 %   are going to talk about. So *simplify*!

 % - In a 20min talk, getting the main ideas across is hard

 %   enough. Leave out details, even if it means being less precise than

 %   you think necessary.

 % - If you omit details that are vital to the proof/implementation,

 %   just say so once. Everybody will be happy with that.

 \section[Deduction - Isabelle]{Deduction - The Theorem Prover Isabelle}

 \subsection[CTP]{Computer Theorem Proving (CTP)}

 \begin{frame}{Computer Theorem Proving (CTP)}

   % - A title should summarize the slide in an understandable fashion

   %   for anyone how does not follow everything on the slide itself.

   \begin{itemize}

   \item USA: ACL, PVS

   \item EU: Isabelle, Coq

   \item history: see 101118-risc.

   \item SW-engineering: program verification, proof obligations proven automatically (ATP), some interactively

   \item interactive provers comprise ATPs

   \end{itemize}

 \end{frame}

 \subsection{Isabelle/Isar}

 \begin{frame}{Isabelle/Isar}

 Wikipedia \href{http://en.wikipedia.org/wiki/Isabelle_(theorem_prover)\\\#Example_proof}{Demo}\\

 lines of code: Pure/  Sequents/ Tools/  Provers/ \\

 in Knowledge/: everything else

 \end{frame}

 \begin{frame}{Contexts}

 	\begin{itemize}

 	\item represent background for composing proofs

 	\item contain declarations, results, ...

 	\item created from theories

 	\item theories are explicitly named data containers

 	\end{itemize}

 \end{frame}

 \section[\isac-System]{Computation - \isac-System}

 \subsection{Features of the \isac-System}

 \begin{frame}{Computation}

 \begin{enumerate}

 \item \alert{guides the user} step by step towards a solution\\

 \uncover<2->{\textit{

 Watching teachers calculate step by step is boring.\\

 Operating on formulas by hand is hard, too.\\

 Software can support {\bf independent learning}.

 }}

 \item \alert{checks user input} as generous and liberal as possible\\

 \uncover<3->{\textit{

 Active learning by {\bf trial and error} is most effective.\\

 Programmers cannot foresee learners' input.\\

 Theorem provers provide most general checking.

 }}

 \item \alert{explains steps} on request by the user\\

 \uncover<4->{\textit{

 Programmers also cannot foresee learners' questions.\\

 A system must be {\bf transparent} for casual questions.\\

 LCF-style provers have human readable knowledge.

 }}

 \end{enumerate}

 \end{frame}

 \subsection{Lucas-Interpretation - Deduction \& Computation}

 \begin{frame}{Lucas-Interpretation - Deduction \& Computation}

 \end{frame}

 \begin{frame}{Title?}

 \includegraphics[width=100mm]{overview.png}

 \end{frame}

 graphics movie

 %\begin{frame}{Make Titles Informative.}

 %\end{frame}

 %\subsection{Introduction of Isabelle's Context to \isac}

 %\begin{frame}{Make Titles Informative.}

 %\end{frame}

 %\begin{frame}{Make Titles Informative.}

 %\end{frame}

 %\begin{frame}{Make Titles Informative.}

 %\end{frame}

 \section*{Summary}

 \begin{frame}{Summary}

   % Keep the summary *very short*.

   \begin{itemize}

   \item

     The \alert{first main message} of your talk in one or two lines.

   \item

     The \alert{second main message} of your talk in one or two lines.

   \item

     Perhaps a \alert{third message}, but not more than that.

   \end{itemize}

   % The following outlook is optional.

   \vskip0pt plus.5fill

   \begin{itemize}

   \item

     Outlook

     \begin{itemize}

     \item

       Something you haven't solved.

     \item

       Something else you haven't solved.

     \end{itemize}

   \end{itemize}

 \end{frame}

 % All of the following is optional and typically not needed.

 \appendix

 \section<presentation>*{\appendixname}

 \subsection<presentation>*{For Further Reading}

 \begin{frame}[allowframebreaks]

   \frametitle<presentation>{For Further Reading}

   \begin{thebibliography}{10}

   \beamertemplatebookbibitems

   % Start with overview books.

   \bibitem{Author1990}

     A.~Author.

     \newblock {\em Handbook of Everything}.

     \newblock Some Press, 1990.

   \beamertemplatearticlebibitems

   % Followed by interesting articles. Keep the list short.

   \bibitem{Someone2000}

     S.~Someone.

     \newblock On this and that.

     \newblock {\em Journal of This and That}, 2(1):50--100,

     2000.

   \end{thebibliography}

 \end{frame}

 \end{document}