wneuper/isa: doc-src/isac/msteger/bakk-presentation.tex@6a67bd03b71c

     1 % /usr/share/doc/latex-beamer/solutions/conference-talks/conference-ornate-20min.en.tex

     3 \documentclass{beamer}

     4 \mode<presentation>

5 {

     6   \usetheme{Hannover}

     7   \setbeamercovered{transparent}

8 }

     9 \usepackage[english]{babel}

    10 \usepackage[latin1]{inputenc}

    11 \usepackage{times}

    12 \usepackage[T1]{fontenc}

    13 %\usepackage{graphicx}

    15 \def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}

    16 \def\sisac{{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}}

    18 \title[Isabelle Frontend]

    19 {Userinterfaces \\f\"ur Computer Theorem Prover,\\

    20 	Machbarkeits-Studie im Isac-Projekt

    21 }

    22 \subtitle{Bachelorarbeit Telematik}

    24 \author{Marco Steger}

    25 \institute{Institut f\"ur Software Technologie\\

    26   Technische Universit\"at Graz}

    28 \date{TODO}

    29 %\subject{Formal specification of math assistants}

    30 % This is only inserted into the PDF information catalog

    32 % Delete this, if you do not want the table of contents to pop up at

    33 % the beginning of each subsection:

    34 \AtBeginSubsection[]

    35 {

    36   \begin{frame}<beamer>

    37     \frametitle{Outline}

    38     \tableofcontents[currentsection,currentsubsection]

    39   \end{frame}

    40 }

    43 % If you wish to uncover everything in a step-wise fashion, uncomment

    44 % the following command:

    45 %\beamerdefaultoverlayspecification{<+->}

    48 \begin{document}

    49 \begin{frame}

    50   \titlepage

    51 \end{frame}

    53 \begin{frame}

    54   \frametitle{Outline}

    55   \tableofcontents

    56   % You might wish to add the option [pausesections]

    57 \end{frame}

    59 \section[Isabelle]{Der Theoremprover Isabelle}

    60 %\begin{frame}

    61 %  \frametitle{The ideal math assistant \dots}

    62 %\begin{enumerate}

    63 %\item \alert{guides the user} step by step towards a solution\\

    64 %\uncover<2->{\textit{

    65 %Watching teachers calculate step by step is boring.\\

    66 %Operating on formulas by hand is hard, too.\\

    67 %Software can support {\bf independent learning}.

    68 %}}

    69 %\item \alert{checks user input} as generous and liberal as possible\\

    70 %\uncover<3->{\textit{

    71 %Active learning by {\bf trial and error} ist most effective.\\

    72 %Programmers cannot foresee learners' input.\\

    73 %Theorem provers provide most general checking.

    74 %}}

    75 %\item \alert{explains steps} on request by the user\\

    76 %\uncover<4->{\textit{

    77 %Programmers also cannot foresee learners' questions.\\

    78 %A system must be {\bf transparent} for casual questions.\\

    79 %LCF-style provers have knowledge human readable.

    80 %}}

    81 %\end{enumerate}

    82 %\end{frame}

    84 \begin{frame}

    85   \frametitle{Der Theoremprover Isabelle}

    86 \begin{itemize}

    87 \item Anwendungen von Isabelle

    88   \begin{itemize}

    89   \item Mechanisieren von Mathematik Theorien

    90     \begin{itemize}

    91     \item nat\"urliche, reelle, komplexe Zahlen, Listen, Lattices, \dots

    92     \item Gr\"obner Basen, Integral/Differential, Taylorreihen, \dots

    93     \item High Order Logics, Logic of Computable Functions, \dots

    94     \end{itemize}

    95   \item Math.Grundlagen f\"ur Softwaretechnologie

    96     \begin{itemize}

    97     \item Hoare Logic, Temporal Logic of Actions, Hoare for Java

    98     \item Theory for Unix file-system security, for state spaces, \dots

    99     \item Archive of Formal Proofs {\tiny\tt http://afp.sourceforge.net}

   100     \end{itemize}

   101   \end{itemize}

   102 \item Integration von Isabelle in Entwicklungstools

   103   \begin{itemize}

   104   \item Boogie --- Verification Condition Generator

   105   \item ? Test Case Generators (TUG) ?

   106   \item \dots ???

   107   \end{itemize}

   108 \item Isar, die Beweissprache von Isabelle

   109 \pause

   110   \begin{itemize}

   111   \item Demo

   112   \end{itemize}

   113 \end{itemize}

   114 \end{frame}

   116 \section[Komponenten]{Komponenten des kommenden Isabelle Frontends}

   117 \subsection[Scala]{Scala und ``Actors''}

   118 \subsection[jEdit]{jEdit und ``Plugins''}

   119 \subsection[Integration]{Integration von Scala und ML}

   121 \section[NetBeans]{Installation der Komponenten in NetBeans}

   122 \subsection[TODO]{TODO}

   124 \section[NetBeans]{Vorbereitung f\"ur ``structured derivations''}

   125 \subsection[Parsen]{Parsen von Isar-Texten}

   127 \section*{Summary}

   128 \begin{frame}

   129   \frametitle<presentation>{Summary}

   131   Summary TODO

   132 \end{frame}

   134 \end{document}

author	Walther Neuper <neuper@ist.tugraz.at>
	Fri, 29 Apr 2011 13:00:34 +0200
branch	decompose-isar
changeset 41966	6a67bd03b71c
parent 41965	c5eaff65fd72
child 42042	4112de132b63
permissions	-rw-r--r--