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{setspace} %for "\begin{onehalfspace}"
36 \usepackage[english]{babel}
39 \usepackage[utf8]{inputenc}
43 \usepackage[T1]{fontenc}
44 % Or whatever. Note that the encoding and the font should match. If T1
45 % does not look nice, try deleting the line with the fontenc.
47 \def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
48 \def\sisac{{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}}
50 \title[\isac: Computation \& Deduction] % (optional, use only with long paper titles)
51 {Integrating Computation and Deduction\\
54 \subtitle{Projektpraktikum: Introducing Isabelle's Contexts}
56 \author[Lehnfeld, Neuper] % (optional, use only with lots of authors)
57 {Mathias~Lehnfeld\inst{1} \and Walther~Neuper\inst{2}}
58 % - Give the names in the same order as the appear in the paper.
59 % - Use the \inst{?} command only if the authors have different
62 \institute % (optional, but mostly needed)
65 Vienna University of Technology
68 Institute of Software Technology\\
69 Graz University of Technology
71 % - Use the \inst command only if there are several affiliations.
72 % - Keep it simple, no one is interested in your street address.
74 % \date[CFP 2003] % (optional, should be abbreviation of conference name)
75 % {Conference on Fabulous Presentations, 2003}
76 % - Either use conference name or its abbreviation.
77 % - Not really informative to the audience, more for people (including
78 % yourself) who are reading the slides online
80 % \subject{Theoretical Computer Science}
81 % This is only inserted into the PDF information catalog. Can be left
86 % If you have a file called "university-logo-filename.xxx", where xxx
87 % is a graphic format that can be processed by latex or pdflatex,
88 % resp., then you can add a logo as follows:
90 % \pgfdeclareimage[height=0.5cm]{university-logo}{university-logo-filename}
91 % \logo{\pgfuseimage{university-logo}}
95 % Delete this, if you do not want the table of contents to pop up at
96 % the beginning of each subsection:
99 \begin{frame}<beamer>{Outline}
100 \tableofcontents[currentsection,currentsubsection]
105 % If you wish to uncover everything in a step-wise fashion, uncomment
106 % the following command:
108 %\beamerdefaultoverlayspecification{<+->}
117 \begin{frame}{Outline}
119 % You might wish to add the option [pausesections]
123 % Structuring a talk is a difficult task and the following structure
124 % may not be suitable. Here are some rules that apply for this
127 % - Exactly two or three sections (other than the summary).
128 % - At *most* three subsections per section.
129 % - Talk about 30s to 2min per frame. So there should be between about
130 % 15 and 30 frames, all told.
132 % - A conference audience is likely to know very little of what you
133 % are going to talk about. So *simplify*!
134 % - In a 20min talk, getting the main ideas across is hard
135 % enough. Leave out details, even if it means being less precise than
136 % you think necessary.
137 % - If you omit details that are vital to the proof/implementation,
138 % just say so once. Everybody will be happy with that.
140 \section[Introduction]{Introduction}
141 \subsection[TODO]{Isabelle and \isac}
143 \frametitle{Isabelle and \isac}
147 \subsection[TODO]{Computation and deduction in a Lucas-Interpreter}
149 \frametitle{Computation and deduction in a Lucas-Interpreter}
153 \section[Contributions]{Contributions of the project}
154 \subsection[TODO]{Introduction of Isabelle Contexts}
160 \subsection[TODO]{Redesign of type inference in \isac}
166 \subsection[TODO]{Improvement of functional code}
168 \frametitle{Drop \textit{Check\_Elementwise} !}
170 %solve (x / (x ^ 2 - 6 * x + 9) - 1 / (x ^ 2 - 3 * x) = 1 / x, x)
171 % x / (x ^ 2 - 6 * x + 9) - 1 / (x ^ 2 - 3 * x) = 1 / x
172 % x / (x ^ 2 + -1 * (6 * x) + 9) + -1 * 1 / (x ^ 2 + -1 * (3 * x)) = 1 / x
173 % (3 + -1 * x + x ^ 2) / (9 * x + -6 * x ^ 2 + x ^ 3) = 1 / x
174 % (3 + -1 * x + x ^ 2) * x = 1 * (9 * x + -6 * x ^ 2 + x ^ 3)
175 % solve ((3 + -1 * x + x ^ 2) * x = 1 * (9 * x + -6 * x ^ 2 + x ^ 3), x)
176 % (3 + -1 * x + x ^ 2) * x = 1 * (9 * x + -6 * x ^ 2 + x ^ 3)
177 % (3 + -1 * x + x ^ 2) * x - 1 * (9 * x + -6 * x ^ 2 + x ^ 3) = 0
178 % (3 + -1 * x + x ^ 2) * x - (9 * x + -6 * x ^ 2 + x ^ 3) = 0
179 % -6 * x + 5 * x ^ 2 = 0
180 % solve (-6 * x + 5 * x ^ 2 = 0, x)
188 %\begin{onehalfspace}
191 $\mathit{solve}\;(\frac{x}{x ^ 2 - 6 * x + 9} - \frac{1}{x ^ 2 - 3 * x} = \frac{1}{x}, x)$\\ \\
192 \>$\frac{x}{x ^ 2 - 6 * x + 9} - \frac{1}{x ^ 2 - 3 * x} = \frac{1}{x}$ \\ \\
193 \>$\frac{x}{x ^ 2 + -1 * (6 * x) + 9} + \frac{-1 * 1}{x ^ 2 + -1 * (3 * x)} = \frac{1}{x}$ \\ \\
194 %\>$\frac{3 + -1 * x + x ^ 2}{9 * x + -6 * x ^ 2 + x ^ 3} = \frac{1}{x}$ \\ \\
195 \>$(3 + -1 * x + x ^ 2) * x = 1 * (9 * x + -6 * x ^ 2 + x ^ 3)$ \\
196 \>$\mathit{solve}\;((3 + -1 * x + x ^ 2) * x = 1 * (9 * x + -6 * x ^ 2 + x ^ 3), x)$ \\
197 \>\>$(3 + -1 * x + x ^ 2) * x = 1 * (9 * x + -6 * x ^ 2 + x ^ 3)$ \\
198 %\>\>$(3 + -1 * x + x ^ 2) * x - 1 * (9 * x + -6 * x ^ 2 + x ^ 3) = 0$ \\
199 \>\>$(3 + -1 * x + x ^ 2) * x - (9 * x + -6 * x ^ 2 + x ^ 3) = 0$ \\
200 \>\>$-6 * x + 5 * x ^ 2 = 0$ \\
201 \>\>$\mathit{solve}\;(-6 * x + 5 * x ^ 2 = 0, x)$ \\
202 \>\>$[x = 0, x = \frac{6}{5}]$ \\
203 \>$[x = 0, x = \frac{6}{5}]$ \\
204 \`\alert{$\mathit{Check\_Elementwise}\;\mathit{Assumptions}$}\\
205 \>$[x = \frac{6}{5}]$ \\
213 \subsection[TODO]{Preparation of future development}
219 \section[Problems]{Problems encountered in the project}
220 %\subsection[TODO]{TODO}
224 \item Publication of new Isabelle release
225 \item Amount of code in Isabelle and \isac
226 \item Changes scattered throughout the code