1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/doc-src/isac/msteger/bakk-presentation.tex	Fri Apr 29 12:53:46 2011 +0200
     1.3 @@ -0,0 +1,134 @@
     1.4 +% /usr/share/doc/latex-beamer/solutions/conference-talks/conference-ornate-20min.en.tex
     1.5 +
     1.6 +\documentclass{beamer}
     1.7 +\mode<presentation>
     1.8 +{
     1.9 +  \usetheme{Hannover}
    1.10 +  \setbeamercovered{transparent}
    1.11 +}
    1.12 +\usepackage[english]{babel}
    1.13 +\usepackage[latin1]{inputenc}
    1.14 +\usepackage{times}
    1.15 +\usepackage[T1]{fontenc}
    1.16 +%\usepackage{graphicx}
    1.17 +
    1.18 +\def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
    1.19 +\def\sisac{{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}}
    1.20 +
    1.21 +\title[Isabelle Frontend]
    1.22 +{Userinterfaces \\f\"ur Computer Theorem Prover,\\
    1.23 +	Machbarkeits-Studie im Isac-Projekt
    1.24 +}
    1.25 +\subtitle{Bachelorarbeit Telematik}
    1.26 +
    1.27 +\author{Marco Steger}
    1.28 +\institute{Institut f\"ur Software Technologie\\
    1.29 +  Technische Universit\"at Graz}
    1.30 +
    1.31 +\date{TODO}
    1.32 +%\subject{Formal specification of math assistants}
    1.33 +% This is only inserted into the PDF information catalog
    1.34 +
    1.35 +% Delete this, if you do not want the table of contents to pop up at
    1.36 +% the beginning of each subsection:
    1.37 +\AtBeginSubsection[]
    1.38 +{
    1.39 +  \begin{frame}<beamer>
    1.40 +    \frametitle{Outline}
    1.41 +    \tableofcontents[currentsection,currentsubsection]
    1.42 +  \end{frame}
    1.43 +}
    1.44 +
    1.45 +
    1.46 +% If you wish to uncover everything in a step-wise fashion, uncomment
    1.47 +% the following command: 
    1.48 +%\beamerdefaultoverlayspecification{<+->}
    1.49 +
    1.50 +
    1.51 +\begin{document}
    1.52 +\begin{frame}
    1.53 +  \titlepage
    1.54 +\end{frame}
    1.55 +
    1.56 +\begin{frame}
    1.57 +  \frametitle{Outline}
    1.58 +  \tableofcontents
    1.59 +  % You might wish to add the option [pausesections]
    1.60 +\end{frame}
    1.61 +
    1.62 +\section[Isabelle]{Der Theoremprover Isabelle}
    1.63 +%\begin{frame}
    1.64 +%  \frametitle{The ideal math assistant \dots}
    1.65 +%\begin{enumerate}
    1.66 +%\item \alert{guides the user} step by step towards a solution\\
    1.67 +%\uncover<2->{\textit{
    1.68 +%Watching teachers calculate step by step is boring.\\
    1.69 +%Operating on formulas by hand is hard, too.\\
    1.70 +%Software can support {\bf independent learning}.
    1.71 +%}}
    1.72 +%\item \alert{checks user input} as generous and liberal as possible\\
    1.73 +%\uncover<3->{\textit{
    1.74 +%Active learning by {\bf trial and error} ist most effective.\\
    1.75 +%Programmers cannot foresee learners' input.\\
    1.76 +%Theorem provers provide most general checking.
    1.77 +%}}
    1.78 +%\item \alert{explains steps} on request by the user\\
    1.79 +%\uncover<4->{\textit{
    1.80 +%Programmers also cannot foresee learners' questions.\\
    1.81 +%A system must be {\bf transparent} for casual questions.\\
    1.82 +%LCF-style provers have knowledge human readable.
    1.83 +%}}
    1.84 +%\end{enumerate}
    1.85 +%\end{frame}
    1.86 +
    1.87 +\begin{frame}
    1.88 +  \frametitle{Der Theoremprover Isabelle}
    1.89 +\begin{itemize}
    1.90 +\item Anwendungen von Isabelle
    1.91 +  \begin{itemize}
    1.92 +  \item Mechanisieren von Mathematik Theorien
    1.93 +    \begin{itemize}
    1.94 +    \item nat\"urliche, reelle, komplexe Zahlen, Listen, Lattices, \dots
    1.95 +    \item Gr\"obner Basen, Integral/Differential, Taylorreihen, \dots          
    1.96 +    \item High Order Logics, Logic of Computable Functions, \dots
    1.97 +    \end{itemize}
    1.98 +  \item Math.Grundlagen f\"ur Softwaretechnologie
    1.99 +    \begin{itemize}
   1.100 +    \item Hoare Logic, Temporal Logic of Actions, Hoare for Java
   1.101 +    \item Theory for Unix file-system security, for state spaces, \dots
   1.102 +    \item Archive of Formal Proofs {\tiny\tt http://afp.sourceforge.net}
   1.103 +    \end{itemize}
   1.104 +  \end{itemize}
   1.105 +\item Integration von Isabelle in Entwicklungstools
   1.106 +  \begin{itemize}
   1.107 +  \item Boogie --- Verification Condition Generator
   1.108 +  \item ? Test Case Generators (TUG) ?
   1.109 +  \item \dots ???
   1.110 +  \end{itemize}
   1.111 +\item Isar, die Beweissprache von Isabelle
   1.112 +\pause
   1.113 +  \begin{itemize}
   1.114 +  \item Demo
   1.115 +  \end{itemize}
   1.116 +\end{itemize}
   1.117 +\end{frame}
   1.118 +
   1.119 +\section[Komponenten]{Komponenten des kommenden Isabelle Frontends}
   1.120 +\subsection[Scala]{Scala und ``Actors''}
   1.121 +\subsection[jEdit]{jEdit und ``Plugins''}
   1.122 +\subsection[Integration]{Integration von Scala und ML}
   1.123 +\subsection[Parsen]{Parsen von Isar-Texten}
   1.124 +
   1.125 +\section[NetBeans]{Installation der Komponenten in NetBeans}
   1.126 +\subsection[TODO]{TODO}
   1.127 +
   1.128 +\section*{Summary}
   1.129 +\begin{frame}
   1.130 +  \frametitle<presentation>{Summary}
   1.131 +
   1.132 +  Summary TODO
   1.133 +\end{frame}
   1.134 +
   1.135 +\end{document}
   1.136 +
   1.137 +