134 % enough. Leave out details, even if it means being less precise than |
134 % enough. Leave out details, even if it means being less precise than |
135 % you think necessary. |
135 % you think necessary. |
136 % - If you omit details that are vital to the proof/implementation, |
136 % - If you omit details that are vital to the proof/implementation, |
137 % just say so once. Everybody will be happy with that. |
137 % just say so once. Everybody will be happy with that. |
138 |
138 |
139 \section[Deduction - Isabelle]{Deduction - The Theorem Prover Isabelle} |
139 \section[Introduction]{Introduction} |
140 |
140 \subsection[TODO]{Isabelle and \isac} |
141 \subsection[CTP]{Computer Theorem Proving (CTP)} |
141 \begin{frame} |
142 |
142 \frametitle{Isabelle and \isac} |
143 \begin{frame}{Computer Theorem Proving (CTP)} |
143 TODO |
144 % - A title should summarize the slide in an understandable fashion |
|
145 % for anyone how does not follow everything on the slide itself. |
|
146 |
|
147 \begin{itemize} |
|
148 \item USA: ACL, PVS |
|
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 |
|
153 \end{itemize} |
|
154 \end{frame} |
144 \end{frame} |
155 |
145 |
156 |
146 \subsection[TODO]{Computation and deduction in a Lucas-Interpreter} |
157 \subsection{Isabelle/Isar} |
147 \begin{frame} |
158 |
148 \frametitle{Computation and deduction in a Lucas-Interpreter} |
159 \begin{frame}{Isabelle/Isar} |
149 TODO |
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 |
|
163 \end{frame} |
150 \end{frame} |
164 |
151 |
165 \begin{frame}{Contexts} |
152 \section[Contributions]{Contributions of the project} |
166 \begin{itemize} |
153 \subsection[TODO]{Introduction of Isabelle Contexts} |
167 \item represent background for composing proofs |
154 \begin{frame} |
168 \item contain declarations, results, ... |
155 \frametitle{TODO} |
169 \item created from theories |
156 TODO |
170 \item theories are explicitly named data containers |
|
171 \end{itemize} |
|
172 \end{frame} |
157 \end{frame} |
173 |
158 |
174 \section[\isac-System]{Computation - \isac-System} |
159 \subsection[TODO]{Redesign of type inference in \isac} |
175 |
160 \begin{frame} |
176 \subsection{Features of the \isac-System} |
161 \frametitle{TODO} |
177 |
162 TODO |
178 \begin{frame}{Computation} |
|
179 \begin{enumerate} |
|
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}. |
|
185 }} |
|
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. |
|
191 }} |
|
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. |
|
197 }} |
|
198 \end{enumerate} |
|
199 \end{frame} |
163 \end{frame} |
200 |
164 |
201 \subsection{Lucas-Interpretation - Deduction \& Computation} |
165 \subsection[TODO]{Improvement of functional code} |
202 \begin{frame}{Lucas-Interpretation - Deduction \& Computation} |
166 \begin{frame} |
203 |
167 \frametitle{TODO} |
|
168 Demo |
204 \end{frame} |
169 \end{frame} |
205 |
170 |
206 |
171 \subsection[TODO]{Preparation of future development} |
207 \begin{frame}{Title?} |
172 \begin{frame} |
208 \includegraphics[width=100mm]{overview.png} |
173 \frametitle{TODO} |
|
174 TODO |
209 \end{frame} |
175 \end{frame} |
210 |
176 |
211 |
177 \section[Problems]{Problems encountered in the project} |
212 graphics movie |
178 %\subsection[TODO]{TODO} |
213 |
179 \begin{frame} |
214 %\begin{frame}{Make Titles Informative.} |
180 \frametitle{TODO} |
215 %\end{frame} |
181 \begin{itemize} |
216 |
182 \item Publication of new Isabelle release |
217 |
183 \item Amount of code in Isabelle and \isac |
218 %\subsection{Introduction of Isabelle's Context to \isac} |
184 \item Changes scattered throughout the code |
219 |
185 \end{itemize} |
220 %\begin{frame}{Make Titles Informative.} |
|
221 %\end{frame} |
|
222 |
|
223 %\begin{frame}{Make Titles Informative.} |
|
224 %\end{frame} |
|
225 |
|
226 %\begin{frame}{Make Titles Informative.} |
|
227 %\end{frame} |
|
228 |
|
229 |
|
230 |
|
231 \section*{Summary} |
|
232 |
|
233 \begin{frame}{Summary} |
|
234 |
|
235 % Keep the summary *very short*. |
|
236 \begin{itemize} |
|
237 \item |
|
238 The \alert{first main message} of your talk in one or two lines. |
|
239 \item |
|
240 The \alert{second main message} of your talk in one or two lines. |
|
241 \item |
|
242 Perhaps a \alert{third message}, but not more than that. |
|
243 \end{itemize} |
|
244 |
|
245 % The following outlook is optional. |
|
246 \vskip0pt plus.5fill |
|
247 \begin{itemize} |
|
248 \item |
|
249 Outlook |
|
250 \begin{itemize} |
|
251 \item |
|
252 Something you haven't solved. |
|
253 \item |
|
254 Something else you haven't solved. |
|
255 \end{itemize} |
|
256 \end{itemize} |
|
257 \end{frame} |
186 \end{frame} |
258 |
187 |
259 |
188 \section{Summary} |
260 |
189 \begin{frame} |
261 % All of the following is optional and typically not needed. |
190 \frametitle{TODO} |
262 \appendix |
191 TODO |
263 \section<presentation>*{\appendixname} |
|
264 \subsection<presentation>*{For Further Reading} |
|
265 |
|
266 \begin{frame}[allowframebreaks] |
|
267 \frametitle<presentation>{For Further Reading} |
|
268 |
|
269 \begin{thebibliography}{10} |
|
270 |
|
271 \beamertemplatebookbibitems |
|
272 % Start with overview books. |
|
273 |
|
274 \bibitem{Author1990} |
|
275 A.~Author. |
|
276 \newblock {\em Handbook of Everything}. |
|
277 \newblock Some Press, 1990. |
|
278 |
|
279 |
|
280 \beamertemplatearticlebibitems |
|
281 % Followed by interesting articles. Keep the list short. |
|
282 |
|
283 \bibitem{Someone2000} |
|
284 S.~Someone. |
|
285 \newblock On this and that. |
|
286 \newblock {\em Journal of This and That}, 2(1):50--100, |
|
287 2000. |
|
288 \end{thebibliography} |
|
289 \end{frame} |
192 \end{frame} |
290 |
193 |
291 \end{document} |
194 \end{document} |
292 |
195 |
293 |
196 |