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