1.1 --- a/doc-src/isac/mlehnfeld/presentation.tex Fri May 27 12:04:21 2011 +0200
1.2 +++ b/doc-src/isac/mlehnfeld/presentation.tex Fri May 27 13:07:46 2011 +0200
1.3 @@ -136,156 +136,59 @@
1.4 % - If you omit details that are vital to the proof/implementation,
1.5 % just say so once. Everybody will be happy with that.
1.6
1.7 -\section[Deduction - Isabelle]{Deduction - The Theorem Prover Isabelle}
1.8 -
1.9 -\subsection[CTP]{Computer Theorem Proving (CTP)}
1.10 -
1.11 -\begin{frame}{Computer Theorem Proving (CTP)}
1.12 - % - A title should summarize the slide in an understandable fashion
1.13 - % for anyone how does not follow everything on the slide itself.
1.14 -
1.15 - \begin{itemize}
1.16 - \item USA: ACL, PVS
1.17 - \item EU: Isabelle, Coq
1.18 - \item history: see 101118-risc.
1.19 - \item SW-engineering: program verification, proof obligations proven automatically (ATP), some interactively
1.20 - \item interactive provers comprise ATPs
1.21 - \end{itemize}
1.22 +\section[Introduction]{Introduction}
1.23 +\subsection[TODO]{Isabelle and \isac}
1.24 +\begin{frame}
1.25 + \frametitle{Isabelle and \isac}
1.26 +TODO
1.27 \end{frame}
1.28
1.29 -
1.30 -\subsection{Isabelle/Isar}
1.31 -
1.32 -\begin{frame}{Isabelle/Isar}
1.33 -Wikipedia \href{http://en.wikipedia.org/wiki/Isabelle_(theorem_prover)\\\#Example_proof}{Demo}\\
1.34 -lines of code: Pure/ Sequents/ Tools/ Provers/ \\
1.35 -in Knowledge/: everything else
1.36 +\subsection[TODO]{Computation and deduction in a Lucas-Interpreter}
1.37 +\begin{frame}
1.38 + \frametitle{Computation and deduction in a Lucas-Interpreter}
1.39 +TODO
1.40 \end{frame}
1.41
1.42 -\begin{frame}{Contexts}
1.43 - \begin{itemize}
1.44 - \item represent background for composing proofs
1.45 - \item contain declarations, results, ...
1.46 - \item created from theories
1.47 - \item theories are explicitly named data containers
1.48 - \end{itemize}
1.49 +\section[Contributions]{Contributions of the project}
1.50 +\subsection[TODO]{Introduction of Isabelle Contexts}
1.51 +\begin{frame}
1.52 + \frametitle{TODO}
1.53 +TODO
1.54 \end{frame}
1.55
1.56 -\section[\isac-System]{Computation - \isac-System}
1.57 -
1.58 -\subsection{Features of the \isac-System}
1.59 -
1.60 -\begin{frame}{Computation}
1.61 -\begin{enumerate}
1.62 -\item \alert{guides the user} step by step towards a solution\\
1.63 -\uncover<2->{\textit{
1.64 -Watching teachers calculate step by step is boring.\\
1.65 -Operating on formulas by hand is hard, too.\\
1.66 -Software can support {\bf independent learning}.
1.67 -}}
1.68 -\item \alert{checks user input} as generous and liberal as possible\\
1.69 -\uncover<3->{\textit{
1.70 -Active learning by {\bf trial and error} is most effective.\\
1.71 -Programmers cannot foresee learners' input.\\
1.72 -Theorem provers provide most general checking.
1.73 -}}
1.74 -\item \alert{explains steps} on request by the user\\
1.75 -\uncover<4->{\textit{
1.76 -Programmers also cannot foresee learners' questions.\\
1.77 -A system must be {\bf transparent} for casual questions.\\
1.78 -LCF-style provers have human readable knowledge.
1.79 -}}
1.80 -\end{enumerate}
1.81 +\subsection[TODO]{Redesign of type inference in \isac}
1.82 +\begin{frame}
1.83 + \frametitle{TODO}
1.84 +TODO
1.85 \end{frame}
1.86
1.87 -\subsection{Lucas-Interpretation - Deduction \& Computation}
1.88 -\begin{frame}{Lucas-Interpretation - Deduction \& Computation}
1.89 -
1.90 +\subsection[TODO]{Improvement of functional code}
1.91 +\begin{frame}
1.92 + \frametitle{TODO}
1.93 +Demo
1.94 \end{frame}
1.95
1.96 -
1.97 -\begin{frame}{Title?}
1.98 -\includegraphics[width=100mm]{overview.png}
1.99 +\subsection[TODO]{Preparation of future development}
1.100 +\begin{frame}
1.101 + \frametitle{TODO}
1.102 +TODO
1.103 \end{frame}
1.104
1.105 -
1.106 -graphics movie
1.107 -
1.108 -%\begin{frame}{Make Titles Informative.}
1.109 -%\end{frame}
1.110 -
1.111 -
1.112 -%\subsection{Introduction of Isabelle's Context to \isac}
1.113 -
1.114 -%\begin{frame}{Make Titles Informative.}
1.115 -%\end{frame}
1.116 -
1.117 -%\begin{frame}{Make Titles Informative.}
1.118 -%\end{frame}
1.119 -
1.120 -%\begin{frame}{Make Titles Informative.}
1.121 -%\end{frame}
1.122 -
1.123 -
1.124 -
1.125 -\section*{Summary}
1.126 -
1.127 -\begin{frame}{Summary}
1.128 -
1.129 - % Keep the summary *very short*.
1.130 - \begin{itemize}
1.131 - \item
1.132 - The \alert{first main message} of your talk in one or two lines.
1.133 - \item
1.134 - The \alert{second main message} of your talk in one or two lines.
1.135 - \item
1.136 - Perhaps a \alert{third message}, but not more than that.
1.137 - \end{itemize}
1.138 -
1.139 - % The following outlook is optional.
1.140 - \vskip0pt plus.5fill
1.141 - \begin{itemize}
1.142 - \item
1.143 - Outlook
1.144 - \begin{itemize}
1.145 - \item
1.146 - Something you haven't solved.
1.147 - \item
1.148 - Something else you haven't solved.
1.149 - \end{itemize}
1.150 - \end{itemize}
1.151 +\section[Problems]{Problems encountered in the project}
1.152 +%\subsection[TODO]{TODO}
1.153 +\begin{frame}
1.154 + \frametitle{TODO}
1.155 +\begin{itemize}
1.156 +\item Publication of new Isabelle release
1.157 +\item Amount of code in Isabelle and \isac
1.158 +\item Changes scattered throughout the code
1.159 +\end{itemize}
1.160 \end{frame}
1.161
1.162 -
1.163 -
1.164 -% All of the following is optional and typically not needed.
1.165 -\appendix
1.166 -\section<presentation>*{\appendixname}
1.167 -\subsection<presentation>*{For Further Reading}
1.168 -
1.169 -\begin{frame}[allowframebreaks]
1.170 - \frametitle<presentation>{For Further Reading}
1.171 -
1.172 - \begin{thebibliography}{10}
1.173 -
1.174 - \beamertemplatebookbibitems
1.175 - % Start with overview books.
1.176 -
1.177 - \bibitem{Author1990}
1.178 - A.~Author.
1.179 - \newblock {\em Handbook of Everything}.
1.180 - \newblock Some Press, 1990.
1.181 -
1.182 -
1.183 - \beamertemplatearticlebibitems
1.184 - % Followed by interesting articles. Keep the list short.
1.185 -
1.186 - \bibitem{Someone2000}
1.187 - S.~Someone.
1.188 - \newblock On this and that.
1.189 - \newblock {\em Journal of This and That}, 2(1):50--100,
1.190 - 2000.
1.191 - \end{thebibliography}
1.192 +\section{Summary}
1.193 +\begin{frame}
1.194 + \frametitle{TODO}
1.195 +TODO
1.196 \end{frame}
1.197
1.198 \end{document}