1 % $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 $
5 % This file is a solution template for:
7 % - Talk at a conference/colloquium.
8 % - Talk length is about 20min.
13 % Copyright 2004 by Till Tantau <tantau@users.sourceforge.net>.
15 % In principle, this file can be redistributed and/or modified under
16 % the terms of the GNU Public License, version 2.
18 % However, this file is supposed to be a template to be modified
19 % for your own needs. For this reason, if you use this file as a
20 % template and not specifically distribute it as part of a another
21 % package/program, I grant the extra permission to freely copy and
22 % modify this file as you see fit and even to delete this copyright
31 \setbeamercovered{transparent}
32 % or whatever (possibly just delete it)
35 \usepackage[english]{babel}
38 \usepackage[utf8]{inputenc}
42 \usepackage[T1]{fontenc}
43 % Or whatever. Note that the encoding and the font should match. If T1
44 % does not look nice, try deleting the line with the fontenc.
46 \def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
47 \def\sisac{{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}}
49 \title[\isac: Computation \& Deduction] % (optional, use only with long paper titles)
50 {Integrating Computation and Deduction\\
53 \subtitle{Projektpraktikum: Introducing Isabelle's Contexts}
55 \author[Lehnfeld, Neuper] % (optional, use only with lots of authors)
56 {Mathias~Lehnfeld\inst{1} \and Walther~Neuper\inst{2}}
57 % - Give the names in the same order as the appear in the paper.
58 % - Use the \inst{?} command only if the authors have different
61 \institute % (optional, but mostly needed)
64 Vienna University of Technology
67 Institute of Software Technology\\
68 Graz University of Technology
70 % - Use the \inst command only if there are several affiliations.
71 % - Keep it simple, no one is interested in your street address.
73 % \date[CFP 2003] % (optional, should be abbreviation of conference name)
74 % {Conference on Fabulous Presentations, 2003}
75 % - Either use conference name or its abbreviation.
76 % - Not really informative to the audience, more for people (including
77 % yourself) who are reading the slides online
79 % \subject{Theoretical Computer Science}
80 % This is only inserted into the PDF information catalog. Can be left
85 % If you have a file called "university-logo-filename.xxx", where xxx
86 % is a graphic format that can be processed by latex or pdflatex,
87 % resp., then you can add a logo as follows:
89 % \pgfdeclareimage[height=0.5cm]{university-logo}{university-logo-filename}
90 % \logo{\pgfuseimage{university-logo}}
94 % Delete this, if you do not want the table of contents to pop up at
95 % the beginning of each subsection:
98 \begin{frame}<beamer>{Outline}
99 \tableofcontents[currentsection,currentsubsection]
104 % If you wish to uncover everything in a step-wise fashion, uncomment
105 % the following command:
107 %\beamerdefaultoverlayspecification{<+->}
116 \begin{frame}{Outline}
118 % You might wish to add the option [pausesections]
122 % Structuring a talk is a difficult task and the following structure
123 % may not be suitable. Here are some rules that apply for this
126 % - Exactly two or three sections (other than the summary).
127 % - At *most* three subsections per section.
128 % - Talk about 30s to 2min per frame. So there should be between about
129 % 15 and 30 frames, all told.
131 % - A conference audience is likely to know very little of what you
132 % are going to talk about. So *simplify*!
133 % - In a 20min talk, getting the main ideas across is hard
134 % enough. Leave out details, even if it means being less precise than
135 % you think necessary.
136 % - If you omit details that are vital to the proof/implementation,
137 % just say so once. Everybody will be happy with that.
139 \section[Deduction - Isabelle]{Deduction - The Theorem Prover Isabelle}
141 \subsection[CTP]{Computer Theorem Proving (CTP)}
143 \begin{frame}{Computer Theorem Proving (CTP)}
144 % - A title should summarize the slide in an understandable fashion
145 % for anyone how does not follow everything on the slide itself.
149 \item EU: Isabelle, Coq
150 \item history: see 101118-risc.
151 \item SW-engineering: program verification, proof obligations proven automatically (ATP), some interactively
152 \item interactive provers comprise ATPs
157 \subsection{Isabelle/Isar}
159 \begin{frame}{Isabelle/Isar}
160 Wikipedia \href{http://en.wikipedia.org/wiki/Isabelle_(theorem_prover)\\\#Example_proof}{Demo}\\
161 lines of code: Pure/ Sequents/ Tools/ Provers/ \\
162 in Knowledge/: everything else
165 \begin{frame}{Contexts}
167 \item represent background for composing proofs
168 \item contain declarations, results, ...
169 \item created from theories
170 \item theories are explicitly named data containers
174 \section[\isac-System]{Computation - \isac-System}
176 \subsection{Features of the \isac-System}
178 \begin{frame}{Computation}
180 \item \alert{guides the user} step by step towards a solution\\
181 \uncover<2->{\textit{
182 Watching teachers calculate step by step is boring.\\
183 Operating on formulas by hand is hard, too.\\
184 Software can support {\bf independent learning}.
186 \item \alert{checks user input} as generous and liberal as possible\\
187 \uncover<3->{\textit{
188 Active learning by {\bf trial and error} is most effective.\\
189 Programmers cannot foresee learners' input.\\
190 Theorem provers provide most general checking.
192 \item \alert{explains steps} on request by the user\\
193 \uncover<4->{\textit{
194 Programmers also cannot foresee learners' questions.\\
195 A system must be {\bf transparent} for casual questions.\\
196 LCF-style provers have human readable knowledge.
201 \subsection{Lucas-Interpretation - Deduction \& Computation}
202 \begin{frame}{Lucas-Interpretation - Deduction \& Computation}
207 \begin{frame}{Title?}
208 \includegraphics[width=100mm]{overview.png}
214 %\begin{frame}{Make Titles Informative.}
218 %\subsection{Introduction of Isabelle's Context to \isac}
220 %\begin{frame}{Make Titles Informative.}
223 %\begin{frame}{Make Titles Informative.}
226 %\begin{frame}{Make Titles Informative.}
233 \begin{frame}{Summary}
235 % Keep the summary *very short*.
238 The \alert{first main message} of your talk in one or two lines.
240 The \alert{second main message} of your talk in one or two lines.
242 Perhaps a \alert{third message}, but not more than that.
245 % The following outlook is optional.
252 Something you haven't solved.
254 Something else you haven't solved.
261 % All of the following is optional and typically not needed.
263 \section<presentation>*{\appendixname}
264 \subsection<presentation>*{For Further Reading}
266 \begin{frame}[allowframebreaks]
267 \frametitle<presentation>{For Further Reading}
269 \begin{thebibliography}{10}
271 \beamertemplatebookbibitems
272 % Start with overview books.
276 \newblock {\em Handbook of Everything}.
277 \newblock Some Press, 1990.
280 \beamertemplatearticlebibitems
281 % Followed by interesting articles. Keep the list short.
283 \bibitem{Someone2000}
285 \newblock On this and that.
286 \newblock {\em Journal of This and That}, 2(1):50--100,
288 \end{thebibliography}